Le Mon, 5 Dec 2011 14:02:56 +0100,
Post by f***@franckbarbier.comHi,
I'm trying an implementation of the Object Constraint Language in
Coq. I look for simplified and/or canonical *usages* of FSet (or
another more suitable Coq component?). Didn't find much matter either
in archives or on the Web. Thanks about any provided examples. Cheers.
PS: please avoid theoretical considerations bout implementing set
theory in Coq!
FSet is now "deprecated", since there is a new module called MSet.
Here is an example, with WeakList of string and AVL of string.
As you can see here:
http://coq.inria.fr/stdlib/Coq.MSets.MSets.html
there are also a simple list implementation, and a specific set for
positives.
Note that if you want to have a set of positive, I already have done
another one on the same idea, but for which you have:
"∀ S₁ S₂, (∀ x, x∈S₁ <-> x∈S₂) → S₁ = S₂", which is not the case for
the provided one.
To know the allowed operations, see the S module type in MSetInterface.v
or "Require MSet. Print MSetInterface." (but it won't print the types).
===============================
Require Import String.
Open Scope string_scope.
Require Import MSets.
(** * First example, using WeakList *)
(** → First, create a decidable type module *)
(** for example using MiniDecidableType *)
Module MDT_String.
Definition t := string.
Definition eq_dec := string_dec.
End MDT_String.
Module StringDec := Make_UDT(MDT_String).
(** → Then build the MSet module *)
Module StringWL := MSetWeakList.Make StringDec.
Example string_wl :=
StringWL.union (StringWL.add "Hello" StringWL.empty)
(StringWL.singleton "World").
Eval compute in string_wl.
Print DecStrOrder.
(** * Second example, using AVL *)
(** → First, create a decidable type module *)
(** for example using MiniDecidableType *)
Module MOT_String.
Definition t := string.
Definition compare_bit : bool -> bool -> comparison -> comparison.
intros [] [] c; [exact c|exact Gt|exact Lt|exact c].
Defined.
Definition compare_ascii :
Ascii.ascii -> Ascii.ascii -> comparison -> comparison.
intros [a10 a11 a12 a13 a14 a15 a16 a17]
[a20 a21 a22 a23 a24 a25 a26 a27] c.
apply (compare_bit a10 a20).
apply (compare_bit a11 a21).
apply (compare_bit a12 a22).
apply (compare_bit a13 a23).
apply (compare_bit a14 a24).
apply (compare_bit a15 a25).
apply (compare_bit a16 a26).
apply (compare_bit a17 a27).
exact c.
Defined.
Definition compare : string -> string -> comparison.
fix 1; intros [|a1 s1] [|a2 s2].
exact Eq.
exact Lt.
exact Gt.
exact (compare_ascii a1 a2 (compare s1 s2)).
Defined.
Definition flip c := match c with Lt => Gt | Eq => Eq | Gt => Lt end.
Definition lt s1 s2 := compare s1 s2 = Lt.
Definition eq s1 s2 := compare s1 s2 = Eq.
Lemma bit_refl : forall b c, compare_bit b b c = c.
Proof. intros []; auto. Qed.
Lemma bit_sym b c d : compare_bit b c (flip d) = flip (compare_bit c
b d). Proof. destruct b; destruct c; auto. Qed.
Lemma bit_trans:forall s t u c d e cmp,
(c = cmp -> d = cmp -> e = cmp) ->
compare_bit s t c = cmp ->
compare_bit t u d = cmp ->
compare_bit s u e = cmp.
Proof. intros [] [] []; simpl; auto; intros; subst; discriminate. Qed.
Lemma bit_inv : forall b c d, compare_bit b c d = Eq -> b = c /\ d =
Eq. Proof. intros [] [] d; simpl; try discriminate; split; auto. Qed.
Lemma ascii_refl : forall b c, compare_ascii b b c = c.
Proof. intros []; simpl; intros; repeat rewrite bit_refl; auto. Qed.
Lemma ascii_sym b c d:
compare_ascii b c (flip d) = flip (compare_ascii c b d).
Proof. now destruct b; destruct c; simpl; repeat rewrite bit_sym. Qed.
Lemma ascii_trans:forall s t u c d e cmp,
(c = cmp -> d = cmp -> e = cmp) ->
compare_ascii s t c = cmp ->
compare_ascii t u d = cmp ->
compare_ascii s u e = cmp.
Proof. now intros [] [] [] c d e cmp K; repeat apply bit_trans. Qed.
Lemma ascii_inv:forall b c d, compare_ascii b c d = Eq -> b = c /\ d
= Eq. Proof.
intros [] [] d H; simpl in *.
repeat (destruct (bit_inv _ _ _ H) as [R L];
rewrite R in *; clear R H; rename L into H).
now split.
Qed.
Lemma string_sym : forall s t, compare s t = flip (compare t s).
Proof.
intros s; induction s; intros t; destruct t; simpl; auto.
rewrite IHs; apply ascii_sym.
Qed.
Lemma string_trans : forall s t u cmp, compare s t = cmp ->
compare t u = cmp -> compare s u = cmp.
Proof.
intros s; induction s; intros t u; destruct t; destruct u; simpl;
auto; try congruence.
intros cmp; apply ascii_trans; eauto.
Qed.
Lemma string_inv : forall s t, compare s t = Eq -> s = t.
Proof.
intros s; induction s; intros t; destruct t; auto; try discriminate.
simpl; intros H; destruct (ascii_inv _ _ _ H).
erewrite IHs; eauto; rewrite H0; split.
Qed.
Instance eq_equiv : Equivalence eq.
split; unfold eq.
intros s; induction s; simpl; auto; rewrite IHs; apply ascii_refl.
intros s1 s2 H; rewrite string_sym; rewrite H; auto.
intros s t u; apply string_trans.
Qed.
Instance lt_strorder : StrictOrder lt.
split; unfold lt.
intros s t; rewrite (@Equivalence_Reflexive _ _ eq_equiv) in t;
congruence. intros s t u; apply string_trans.
Qed.
Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
unfold Proper, eq, lt; split; simpl in *;
rewrite (string_inv _ _ H); rewrite (string_inv _ _ H0); auto.
Qed.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Proof.
intros x y; case_eq (compare x y); constructor; auto.
unfold lt. rewrite string_sym. rewrite H. split.
Qed.
End MOT_String.
Module StringOrd := DSO_to_OT(MOT_String).
(** → Then build the MSet module *)
Module StringAVL := MSetAVL.Make StringOrd.
Example string_avl :=
StringAVL.union (StringAVL.add "Hello" StringAVL.empty)
(StringAVL.singleton "World").
Eval compute in string_avl.