summaryrefslogtreecommitdiff
path: root/theories/FSets/FSetWeakList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetWeakList.v')
-rw-r--r--theories/FSets/FSetWeakList.v873
1 files changed, 873 insertions, 0 deletions
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
new file mode 100644
index 00000000..74c81f37
--- /dev/null
+++ b/theories/FSets/FSetWeakList.v
@@ -0,0 +1,873 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id: FSetWeakList.v 8639 2006-03-16 19:21:55Z letouzey $ *)
+
+(** * Finite sets library *)
+
+(** This file proposes an implementation of the non-dependant
+ interface [FSetWeakInterface.S] using lists without redundancy. *)
+
+Require Import FSetWeakInterface.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Functions over lists
+
+ First, we provide sets as lists which are (morally) without redundancy.
+ The specs are proved under the additional condition of no redundancy.
+ And the functions returning sets are proved to preserve this invariant. *)
+
+Module Raw (X: DecidableType).
+
+ Module E := X.
+
+ Definition elt := X.t.
+ Definition t := list elt.
+
+ Definition empty : t := nil.
+
+ Definition is_empty (l : t) : bool := if l then true else false.
+
+ (** ** The set operations. *)
+
+ Fixpoint mem (x : elt) (s : t) {struct s} : bool :=
+ match s with
+ | nil => false
+ | y :: l =>
+ if X.eq_dec x y then true else mem x l
+ end.
+
+ Fixpoint add (x : elt) (s : t) {struct s} : t :=
+ match s with
+ | nil => x :: nil
+ | y :: l =>
+ if X.eq_dec x y then s else y :: add x l
+ end.
+
+ Definition singleton (x : elt) : t := x :: nil.
+
+ Fixpoint remove (x : elt) (s : t) {struct s} : t :=
+ match s with
+ | nil => nil
+ | y :: l =>
+ if X.eq_dec x y then l else y :: remove x l
+ end.
+
+ Fixpoint fold (B : Set) (f : elt -> B -> B) (s : t) {struct s} :
+ B -> B := fun i => match s with
+ | nil => i
+ | x :: l => fold f l (f x i)
+ end.
+
+ Definition union (s : t) : t -> t := fold add s.
+
+ Definition diff (s s' : t) : t := fold remove s' s.
+
+ Definition inter (s s': t) : t :=
+ fold (fun x s => if mem x s' then add x s else s) s nil.
+
+ Definition subset (s s' : t) : bool := is_empty (diff s s').
+
+ Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s).
+
+ Fixpoint filter (f : elt -> bool) (s : t) {struct s} : t :=
+ match s with
+ | nil => nil
+ | x :: l => if f x then x :: filter f l else filter f l
+ end.
+
+ Fixpoint for_all (f : elt -> bool) (s : t) {struct s} : bool :=
+ match s with
+ | nil => true
+ | x :: l => if f x then for_all f l else false
+ end.
+
+ Fixpoint exists_ (f : elt -> bool) (s : t) {struct s} : bool :=
+ match s with
+ | nil => false
+ | x :: l => if f x then true else exists_ f l
+ end.
+
+ Fixpoint partition (f : elt -> bool) (s : t) {struct s} :
+ t * t :=
+ match s with
+ | nil => (nil, nil)
+ | x :: l =>
+ let (s1, s2) := partition f l in
+ if f x then (x :: s1, s2) else (s1, x :: s2)
+ end.
+
+ Definition cardinal (s : t) : nat := length s.
+
+ Definition elements (s : t) : list elt := s.
+
+ Definition choose (s : t) : option elt :=
+ match s with
+ | nil => None
+ | x::_ => Some x
+ end.
+
+ (** ** Proofs of set operation specifications. *)
+
+ Notation NoDup := (NoDupA X.eq).
+ Notation In := (InA X.eq).
+
+ Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+ Definition Subset s s' := forall a : elt, In a s -> In a s'.
+ Definition Empty s := forall a : elt, ~ In a s.
+ Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+ Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+
+ Lemma In_eq :
+ forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s.
+ Proof.
+ intros s x y; do 2 setoid_rewrite InA_alt; firstorder eauto.
+ Qed.
+ Hint Immediate In_eq.
+
+ Lemma mem_1 :
+ forall (s : t)(x : elt), In x s -> mem x s = true.
+ Proof.
+ induction s; intros.
+ inversion H.
+ simpl; destruct (X.eq_dec x a); trivial.
+ inversion_clear H; auto.
+ Qed.
+
+ Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s.
+ Proof.
+ induction s.
+ intros; inversion H.
+ intros x; simpl.
+ destruct (X.eq_dec x a); firstorder; discriminate.
+ Qed.
+
+ Lemma add_1 :
+ forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> In y (add x s).
+ Proof.
+ induction s.
+ simpl; intuition.
+ simpl; intros; case (X.eq_dec x a); intuition; inversion_clear Hs;
+ firstorder.
+ eauto.
+ Qed.
+
+ Lemma add_2 :
+ forall (s : t) (Hs : NoDup s) (x y : elt), In y s -> In y (add x s).
+ Proof.
+ induction s.
+ simpl; intuition.
+ simpl; intros; case (X.eq_dec x a); intuition.
+ inversion_clear Hs; eauto; inversion_clear H; intuition.
+ Qed.
+
+ Lemma add_3 :
+ forall (s : t) (Hs : NoDup s) (x y : elt),
+ ~ X.eq x y -> In y (add x s) -> In y s.
+ Proof.
+ induction s.
+ simpl; intuition.
+ inversion_clear H0; firstorder; absurd (X.eq x y); auto.
+ simpl; intros Hs x y; case (X.eq_dec x a); intros;
+ inversion_clear H0; inversion_clear Hs; firstorder;
+ absurd (X.eq x y); auto.
+ Qed.
+
+ Lemma add_unique :
+ forall (s : t) (Hs : NoDup s)(x:elt), NoDup (add x s).
+ Proof.
+ induction s.
+ simpl; intuition.
+ constructor; auto.
+ intro H0; inversion H0.
+ intros.
+ inversion_clear Hs.
+ simpl.
+ destruct (X.eq_dec x a).
+ constructor; auto.
+ constructor; auto.
+ intro H1; apply H.
+ eapply add_3; eauto.
+ Qed.
+
+ Lemma remove_1 :
+ forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> ~ In y (remove x s).
+ Proof.
+ simple induction s.
+ simpl; red; intros; inversion H0.
+ simpl; intros; case (X.eq_dec x a); intuition; inversion_clear Hs.
+ elim H2.
+ apply In_eq with y; eauto.
+ inversion_clear H1; eauto.
+ Qed.
+
+ Lemma remove_2 :
+ forall (s : t) (Hs : NoDup s) (x y : elt),
+ ~ X.eq x y -> In y s -> In y (remove x s).
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros; case (X.eq_dec x a); intuition; inversion_clear Hs;
+ inversion_clear H1; auto.
+ absurd (X.eq x y); eauto.
+ Qed.
+
+ Lemma remove_3 :
+ forall (s : t) (Hs : NoDup s) (x y : elt), In y (remove x s) -> In y s.
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros a l Hrec Hs x y; case (X.eq_dec x a); intuition.
+ inversion_clear Hs; inversion_clear H; firstorder.
+ Qed.
+
+ Lemma remove_unique :
+ forall (s : t) (Hs : NoDup s) (x : elt), NoDup (remove x s).
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros; case (X.eq_dec x a); intuition; inversion_clear Hs;
+ auto.
+ constructor; auto.
+ intro H2; elim H0.
+ eapply remove_3; eauto.
+ Qed.
+
+ Lemma singleton_unique : forall x : elt, NoDup (singleton x).
+ Proof.
+ unfold singleton; simpl; constructor; auto; intro H; inversion H.
+ Qed.
+
+ Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y.
+ Proof.
+ unfold singleton; simpl; intuition.
+ inversion_clear H; auto; inversion H0.
+ Qed.
+
+ Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x).
+ Proof.
+ unfold singleton; simpl; intuition.
+ Qed.
+
+ Lemma empty_unique : NoDup empty.
+ Proof.
+ unfold empty; constructor.
+ Qed.
+
+ Lemma empty_1 : Empty empty.
+ Proof.
+ unfold Empty, empty; intuition; inversion H.
+ Qed.
+
+ Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.
+ Proof.
+ unfold Empty; intro s; case s; simpl; intuition.
+ elim (H e); auto.
+ Qed.
+
+ Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s.
+ Proof.
+ unfold Empty; intro s; case s; simpl; intuition;
+ inversion H0.
+ Qed.
+
+ Lemma elements_1 : forall (s : t) (x : elt), In x s -> In x (elements s).
+ Proof.
+ unfold elements; auto.
+ Qed.
+
+ Lemma elements_2 : forall (s : t) (x : elt), In x (elements s) -> In x s.
+ Proof.
+ unfold elements; auto.
+ Qed.
+
+ Lemma elements_3 : forall (s : t) (Hs : NoDup s), NoDup (elements s).
+ Proof.
+ unfold elements; auto.
+ Qed.
+
+ Lemma fold_1 :
+ forall (s : t) (Hs : NoDup s) (A : Set) (i : A) (f : elt -> A -> A),
+ fold f s i = fold_left (fun a e => f e a) (elements s) i.
+ Proof.
+ induction s; simpl; auto; intros.
+ inversion_clear Hs; auto.
+ Qed.
+
+ Lemma union_unique :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (union s s').
+ Proof.
+ unfold union; induction s; simpl; auto; intros.
+ inversion_clear Hs.
+ apply IHs; auto.
+ apply add_unique; auto.
+ Qed.
+
+ Lemma union_1 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x (union s s') -> In x s \/ In x s'.
+ Proof.
+ unfold union; induction s; simpl; auto; intros.
+ inversion_clear Hs.
+ destruct (X.eq_dec x a).
+ left; auto.
+ destruct (IHs (add a s') H1 (add_unique Hs' a) x); intuition.
+ right; eapply add_3; eauto.
+ Qed.
+
+ Lemma union_0 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x s \/ In x s' -> In x (union s s').
+ Proof.
+ unfold union; induction s; simpl; auto; intros.
+ inversion_clear H; auto.
+ inversion_clear H0.
+ inversion_clear Hs.
+ apply IHs; auto.
+ apply add_unique; auto.
+ destruct H.
+ inversion_clear H; auto.
+ right; apply add_1; auto.
+ right; apply add_2; auto.
+ Qed.
+
+ Lemma union_2 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x s -> In x (union s s').
+ Proof.
+ intros; apply union_0; auto.
+ Qed.
+
+ Lemma union_3 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x s' -> In x (union s s').
+ Proof.
+ intros; apply union_0; auto.
+ Qed.
+
+ Lemma inter_unique :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (inter s s').
+ Proof.
+ unfold inter; intros s.
+ set (acc := nil (A:=elt)).
+ assert (NoDup acc) by (unfold acc; auto).
+ clearbody acc; generalize H; clear H; generalize acc; clear acc.
+ induction s; simpl; auto; intros.
+ inversion_clear Hs.
+ apply IHs; auto.
+ destruct (mem a s'); intros; auto.
+ apply add_unique; auto.
+ Qed.
+
+ Lemma inter_0 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x (inter s s') -> In x s /\ In x s'.
+ Proof.
+ unfold inter; intros.
+ set (acc := nil (A:=elt)) in *.
+ assert (NoDup acc) by (unfold acc; auto).
+ cut ((In x s /\ In x s') \/ In x acc).
+ destruct 1; auto.
+ inversion H1.
+ clearbody acc.
+ generalize H0 H Hs' Hs; clear H0 H Hs Hs'.
+ generalize acc x s'; clear acc x s'.
+ induction s; simpl; auto; intros.
+ inversion_clear Hs.
+ case_eq (mem a s'); intros H3; rewrite H3 in H; simpl in H.
+ destruct (IHs _ _ _ (add_unique H0 a) H); auto.
+ left; intuition.
+ destruct (X.eq_dec x a); auto.
+ left; intuition.
+ apply In_eq with a; eauto.
+ apply mem_2; auto.
+ right; eapply add_3; eauto.
+ destruct (IHs _ _ _ H0 H); auto.
+ left; intuition.
+ Qed.
+
+ Lemma inter_1 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x (inter s s') -> In x s.
+ Proof.
+ intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ].
+ Qed.
+
+ Lemma inter_2 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x (inter s s') -> In x s'.
+ Proof.
+ intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ].
+ Qed.
+
+ Lemma inter_3 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x s -> In x s' -> In x (inter s s').
+ Proof.
+ intros s s' Hs Hs' x.
+ cut (((In x s /\ In x s')\/ In x (nil (A:=elt))) -> In x (inter s s')).
+ intuition.
+ unfold inter.
+ set (acc := nil (A:=elt)) in *.
+ assert (NoDup acc) by (unfold acc; auto).
+ clearbody acc.
+ generalize H Hs' Hs; clear H Hs Hs'.
+ generalize acc x s'; clear acc x s'.
+ induction s; simpl; auto; intros.
+ destruct H0; auto.
+ destruct H0; inversion H0.
+ inversion_clear Hs.
+ case_eq (mem a s'); intros H3; apply IHs; auto.
+ apply add_unique; auto.
+ destruct H0.
+ destruct H0.
+ inversion_clear H0.
+ right; apply add_1; auto.
+ left; auto.
+ right; apply add_2; auto.
+ destruct H0; auto.
+ destruct H0.
+ inversion_clear H0; auto.
+ absurd (In x s'); auto.
+ red; intros.
+ rewrite (mem_1 (In_eq H5 H0)) in H3.
+ discriminate.
+ Qed.
+
+ Lemma diff_unique :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (diff s s').
+ Proof.
+ unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
+ induction s'; simpl; auto; intros.
+ inversion_clear Hs'.
+ apply IHs'; auto.
+ apply remove_unique; auto.
+ Qed.
+
+ Lemma diff_0 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x (diff s s') -> In x s /\ ~ In x s'.
+ Proof.
+ unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
+ induction s'; simpl; auto; intros.
+ inversion_clear Hs'.
+ split; auto; intro H1; inversion H1.
+ inversion_clear Hs'.
+ destruct (IHs' (remove a s) (remove_unique Hs a) H1 x H).
+ split.
+ eapply remove_3; eauto.
+ red; intros.
+ inversion_clear H4; auto.
+ destruct (remove_1 Hs (X.eq_sym H5) H2).
+ Qed.
+
+ Lemma diff_1 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x (diff s s') -> In x s.
+ Proof.
+ intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto].
+ Qed.
+
+ Lemma diff_2 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x (diff s s') -> ~ In x s'.
+ Proof.
+ intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto].
+ Qed.
+
+ Lemma diff_3 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
+ In x s -> ~ In x s' -> In x (diff s s').
+ Proof.
+ unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
+ induction s'; simpl; auto; intros.
+ inversion_clear Hs'.
+ apply IHs'; auto.
+ apply remove_unique; auto.
+ apply remove_2; auto.
+ Qed.
+
+ Lemma subset_1 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
+ Subset s s' -> subset s s' = true.
+ Proof.
+ unfold subset, Subset; intros.
+ apply is_empty_1.
+ unfold Empty; intros.
+ intro.
+ destruct (diff_2 Hs Hs' H0).
+ apply H.
+ eapply diff_1; eauto.
+ Qed.
+
+ Lemma subset_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'),
+ subset s s' = true -> Subset s s'.
+ Proof.
+ unfold subset, Subset; intros.
+ generalize (is_empty_2 H); clear H; unfold Empty; intros.
+ generalize (@mem_1 s' a) (@mem_2 s' a); destruct (mem a s').
+ intuition.
+ intros.
+ destruct (H a).
+ apply diff_3; intuition.
+ Qed.
+
+ Lemma equal_1 :
+ forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
+ Equal s s' -> equal s s' = true.
+ Proof.
+ unfold Equal, equal; intros.
+ apply andb_true_intro; split; apply subset_1; firstorder.
+ Qed.
+
+ Lemma equal_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'),
+ equal s s' = true -> Equal s s'.
+ Proof.
+ unfold Equal, equal; intros.
+ destruct (andb_prop _ _ H); clear H.
+ split; apply subset_2; auto.
+ Qed.
+
+ Definition choose_1 :
+ forall (s : t) (x : elt), choose s = Some x -> In x s.
+ Proof.
+ destruct s; simpl; intros; inversion H; auto.
+ Qed.
+
+ Definition choose_2 : forall s : t, choose s = None -> Empty s.
+ Proof.
+ destruct s; simpl; intros.
+ intros x H0; inversion H0.
+ inversion H.
+ Qed.
+
+ Lemma cardinal_1 :
+ forall (s : t) (Hs : NoDup s), cardinal s = length (elements s).
+ Proof.
+ auto.
+ Qed.
+
+ Lemma filter_1 :
+ forall (s : t) (x : elt) (f : elt -> bool),
+ In x (filter f s) -> In x s.
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H.
+ intros x l Hrec a f.
+ case (f x); simpl.
+ inversion_clear 1.
+ constructor; auto.
+ constructor 2; apply (Hrec a f); trivial.
+ constructor 2; apply (Hrec a f); trivial.
+ Qed.
+
+ Lemma filter_2 :
+ forall (s : t) (x : elt) (f : elt -> bool),
+ compat_bool X.eq f -> In x (filter f s) -> f x = true.
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H0.
+ intros x l Hrec a f Hf.
+ generalize (Hf x); case (f x); simpl; auto.
+ inversion_clear 2; auto.
+ symmetry; auto.
+ Qed.
+
+ Lemma filter_3 :
+ forall (s : t) (x : elt) (f : elt -> bool),
+ compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H0.
+ intros x l Hrec a f Hf.
+ generalize (Hf x); case (f x); simpl.
+ inversion_clear 2; auto.
+ inversion_clear 2; auto.
+ rewrite <- (H a (X.eq_sym H1)); intros; discriminate.
+ Qed.
+
+ Lemma filter_unique :
+ forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (filter f s).
+ Proof.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec Hs f; inversion_clear Hs.
+ case (f x); auto.
+ constructor; auto.
+ intro H1; apply H.
+ eapply filter_1; eauto.
+ Qed.
+
+
+ Lemma for_all_1 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f ->
+ For_all (fun x => f x = true) s -> for_all f s = true.
+ Proof.
+ simple induction s; simpl; auto; unfold For_all.
+ intros x l Hrec f Hf.
+ generalize (Hf x); case (f x); simpl.
+ auto.
+ intros; rewrite (H x); auto.
+ Qed.
+
+ Lemma for_all_2 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f ->
+ for_all f s = true -> For_all (fun x => f x = true) s.
+ Proof.
+ simple induction s; simpl; auto; unfold For_all.
+ intros; inversion H1.
+ intros x l Hrec f Hf.
+ intros A a; intros.
+ assert (f x = true).
+ generalize A; case (f x); auto.
+ rewrite H0 in A; simpl in A.
+ inversion_clear H; auto.
+ rewrite (Hf a x); auto.
+ Qed.
+
+ Lemma exists_1 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
+ Proof.
+ simple induction s; simpl; auto; unfold Exists.
+ intros.
+ elim H0; intuition.
+ inversion H2.
+ intros x l Hrec f Hf.
+ generalize (Hf x); case (f x); simpl.
+ auto.
+ destruct 2 as [a (A1,A2)].
+ inversion_clear A1.
+ rewrite <- (H a (X.eq_sym H0)) in A2; discriminate.
+ apply Hrec; auto.
+ exists a; auto.
+ Qed.
+
+ Lemma exists_2 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
+ Proof.
+ simple induction s; simpl; auto; unfold Exists.
+ intros; discriminate.
+ intros x l Hrec f Hf.
+ case_eq (f x); intros.
+ exists x; auto.
+ destruct (Hrec f Hf H0) as [a (A1,A2)].
+ exists a; auto.
+ Qed.
+
+ Lemma partition_1 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).
+ Proof.
+ simple induction s; simpl; auto; unfold Equal.
+ firstorder.
+ intros x l Hrec f Hf.
+ generalize (Hrec f Hf); clear Hrec.
+ case (partition f l); intros s1 s2; simpl; intros.
+ case (f x); simpl; firstorder; inversion H0; intros; firstorder.
+ Qed.
+
+ Lemma partition_2 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f ->
+ Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+ Proof.
+ simple induction s; simpl; auto; unfold Equal.
+ firstorder.
+ intros x l Hrec f Hf.
+ generalize (Hrec f Hf); clear Hrec.
+ case (partition f l); intros s1 s2; simpl; intros.
+ case (f x); simpl; firstorder; inversion H0; intros; firstorder.
+ Qed.
+
+ Lemma partition_aux_1 :
+ forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt),
+ In x (fst (partition f s)) -> In x s.
+ Proof.
+ induction s; simpl; auto; intros.
+ inversion_clear Hs.
+ generalize (IHs H1 f x).
+ destruct (f a); destruct (partition f s); simpl in *; auto.
+ inversion_clear H; auto.
+ Qed.
+
+ Lemma partition_aux_2 :
+ forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt),
+ In x (snd (partition f s)) -> In x s.
+ Proof.
+ induction s; simpl; auto; intros.
+ inversion_clear Hs.
+ generalize (IHs H1 f x).
+ destruct (f a); destruct (partition f s); simpl in *; auto.
+ inversion_clear H; auto.
+ Qed.
+
+ Lemma partition_unique_1 :
+ forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (fst (partition f s)).
+ Proof.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec Hs f; inversion_clear Hs.
+ generalize (@partition_aux_1 _ H0 f x).
+ generalize (Hrec H0 f).
+ case (f x); case (partition f l); simpl; auto.
+ Qed.
+
+ Lemma partition_unique_2 :
+ forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (snd (partition f s)).
+ Proof.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec Hs f; inversion_clear Hs.
+ generalize (@partition_aux_2 _ H0 f x).
+ generalize (Hrec H0 f).
+ case (f x); case (partition f l); simpl; auto.
+ Qed.
+
+ Definition eq : t -> t -> Prop := Equal.
+
+ Lemma eq_refl : forall s : t, eq s s.
+ Proof.
+ unfold eq, Equal; intuition.
+ Qed.
+
+ Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s.
+ Proof.
+ unfold eq, Equal; firstorder.
+ Qed.
+
+ Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
+ Proof.
+ unfold eq, Equal; firstorder.
+ Qed.
+
+End Raw.
+
+(** * Encapsulation
+
+ Now, in order to really provide a functor implementing [S], we
+ need to encapsulate everything into a type of lists without redundancy. *)
+
+Module Make (X: DecidableType) <: S with Module E := X.
+
+ Module E := X.
+ Module Raw := Raw X.
+
+ Record slist : Set := {this :> Raw.t; unique : NoDupA X.eq this}.
+ Definition t := slist.
+ Definition elt := X.t.
+
+ Definition In (x : elt) (s : t) := InA X.eq x s.(this).
+ Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+ Definition Subset s s' := forall a : elt, In a s -> In a s'.
+ Definition Empty s := forall a : elt, ~ In a s.
+ Definition For_all (P : elt -> Prop) (s : t) :=
+ forall x : elt, In x s -> P x.
+ Definition Exists (P : elt -> Prop) (s : t) := exists x : elt, In x s /\ P x.
+
+ Definition In_1 (s : t) := Raw.In_eq (s:=s).
+
+ Definition mem (x : elt) (s : t) := Raw.mem x s.
+ Definition mem_1 (s : t) := Raw.mem_1 (s:=s).
+ Definition mem_2 (s : t) := Raw.mem_2 (s:=s).
+
+ Definition add x s := Build_slist (Raw.add_unique (unique s) x).
+ Definition add_1 (s : t) := Raw.add_1 (unique s).
+ Definition add_2 (s : t) := Raw.add_2 (unique s).
+ Definition add_3 (s : t) := Raw.add_3 (unique s).
+
+ Definition remove x s := Build_slist (Raw.remove_unique (unique s) x).
+ Definition remove_1 (s : t) := Raw.remove_1 (unique s).
+ Definition remove_2 (s : t) := Raw.remove_2 (unique s).
+ Definition remove_3 (s : t) := Raw.remove_3 (unique s).
+
+ Definition singleton x := Build_slist (Raw.singleton_unique x).
+ Definition singleton_1 := Raw.singleton_1.
+ Definition singleton_2 := Raw.singleton_2.
+
+ Definition union (s s' : t) :=
+ Build_slist (Raw.union_unique (unique s) (unique s')).
+ Definition union_1 (s s' : t) := Raw.union_1 (unique s) (unique s').
+ Definition union_2 (s s' : t) := Raw.union_2 (unique s) (unique s').
+ Definition union_3 (s s' : t) := Raw.union_3 (unique s) (unique s').
+
+ Definition inter (s s' : t) :=
+ Build_slist (Raw.inter_unique (unique s) (unique s')).
+ Definition inter_1 (s s' : t) := Raw.inter_1 (unique s) (unique s').
+ Definition inter_2 (s s' : t) := Raw.inter_2 (unique s) (unique s').
+ Definition inter_3 (s s' : t) := Raw.inter_3 (unique s) (unique s').
+
+ Definition diff (s s' : t) :=
+ Build_slist (Raw.diff_unique (unique s) (unique s')).
+ Definition diff_1 (s s' : t) := Raw.diff_1 (unique s) (unique s').
+ Definition diff_2 (s s' : t) := Raw.diff_2 (unique s) (unique s').
+ Definition diff_3 (s s' : t) := Raw.diff_3 (unique s) (unique s').
+
+ Definition equal (s s' : t) := Raw.equal s s'.
+ Definition equal_1 (s s' : t) := Raw.equal_1 (unique s) (unique s').
+ Definition equal_2 (s s' : t) := Raw.equal_2 (unique s) (unique s').
+
+ Definition subset (s s' : t) := Raw.subset s s'.
+ Definition subset_1 (s s' : t) := Raw.subset_1 (unique s) (unique s').
+ Definition subset_2 (s s' : t) := Raw.subset_2 (unique s) (unique s').
+
+ Definition empty := Build_slist Raw.empty_unique.
+ Definition empty_1 := Raw.empty_1.
+
+ Definition is_empty (s : t) := Raw.is_empty s.
+ Definition is_empty_1 (s : t) := Raw.is_empty_1 (s:=s).
+ Definition is_empty_2 (s : t) := Raw.is_empty_2 (s:=s).
+
+ Definition elements (s : t) := Raw.elements s.
+ Definition elements_1 (s : t) := Raw.elements_1 (s:=s).
+ Definition elements_2 (s : t) := Raw.elements_2 (s:=s).
+ Definition elements_3 (s : t) := Raw.elements_3 (unique s).
+
+ Definition choose (s:t) := Raw.choose s.
+ Definition choose_1 (s : t) := Raw.choose_1 (s:=s).
+ Definition choose_2 (s : t) := Raw.choose_2 (s:=s).
+
+ Definition fold (B : Set) (f : elt -> B -> B) (s : t) := Raw.fold (B:=B) f s.
+ Definition fold_1 (s : t) := Raw.fold_1 (unique s).
+
+ Definition cardinal (s : t) := Raw.cardinal s.
+ Definition cardinal_1 (s : t) := Raw.cardinal_1 (unique s).
+
+ Definition filter (f : elt -> bool) (s : t) :=
+ Build_slist (Raw.filter_unique (unique s) f).
+ Definition filter_1 (s : t)(x:elt)(f: elt -> bool)(H:compat_bool X.eq f) :=
+ @Raw.filter_1 s x f.
+ Definition filter_2 (s : t) := Raw.filter_2 (s:=s).
+ Definition filter_3 (s : t) := Raw.filter_3 (s:=s).
+
+ Definition for_all (f : elt -> bool) (s : t) := Raw.for_all f s.
+ Definition for_all_1 (s : t) := Raw.for_all_1 (s:=s).
+ Definition for_all_2 (s : t) := Raw.for_all_2 (s:=s).
+
+ Definition exists_ (f : elt -> bool) (s : t) := Raw.exists_ f s.
+ Definition exists_1 (s : t) := Raw.exists_1 (s:=s).
+ Definition exists_2 (s : t) := Raw.exists_2 (s:=s).
+
+ Definition partition (f : elt -> bool) (s : t) :=
+ let p := Raw.partition f s in
+ (Build_slist (this:=fst p) (Raw.partition_unique_1 (unique s) f),
+ Build_slist (this:=snd p) (Raw.partition_unique_2 (unique s) f)).
+ Definition partition_1 (s : t) := Raw.partition_1 s.
+ Definition partition_2 (s : t) := Raw.partition_2 s.
+
+ Definition eq (s s' : t) := Raw.eq s s'.
+ Definition eq_refl (s : t) := Raw.eq_refl s.
+ Definition eq_sym (s s' : t) := Raw.eq_sym (s:=s) (s':=s').
+ Definition eq_trans (s s' s'' : t) :=
+ Raw.eq_trans (s:=s) (s':=s') (s'':=s'').
+
+End Make.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 18:43:35 +0000