The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Mon, 5 Dec 2011 14:02:56 +0100,
franck.barbier AT franckbarbier.com
 a écrit :

> Hi,
> 
> 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.