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.v945
1 files changed, 9 insertions, 936 deletions
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 309016ce..711cbd9a 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -6,952 +6,25 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetWeakList.v 11866 2009-01-28 19:10:15Z letouzey $ *)
+(* $Id$ *)
(** * Finite sets library *)
-(** This file proposes an implementation of the non-dependant
- interface [FSetWeakInterface.S] using lists without redundancy. *)
+(** This file proposes an implementation of the non-dependant
+ interface [FSetInterface.WS] using lists without redundancy. *)
Require Import FSetInterface.
Set Implicit Arguments.
Unset Strict Implicit.
-(** * Functions over lists
+(** This is just a compatibility layer, the real implementation
+ is now in [MSetWeakList] *)
- 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).
-
- 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 : Type) (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. *)
- Section ForNotations.
- 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; 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_3w : forall (s : t) (Hs : NoDup s), NoDup (elements s).
- Proof.
- unfold elements; auto.
- Qed.
-
- Lemma fold_1 :
- forall (s : t) (Hs : NoDup s) (A : Type) (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, eq s s.
- Proof. firstorder. Qed.
-
- Lemma eq_sym : forall s s', eq s s' -> eq s' s.
- Proof. firstorder. Qed.
-
- Lemma eq_trans :
- forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
- Proof. firstorder. Qed.
-
- Definition eq_dec : forall (s s':t)(Hs:NoDup s)(Hs':NoDup s'),
- { eq s s' }+{ ~eq s s' }.
- Proof.
- intros.
- change eq with Equal.
- case_eq (equal s s'); intro H; [left | right].
- apply equal_2; auto.
- intro H'; rewrite equal_1 in H; auto; discriminate.
- Defined.
-
- End ForNotations.
-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. *)
+Require Equalities FSetCompat MSetWeakList.
Module Make (X: DecidableType) <: WS with Module E := X.
-
- Module Raw := Raw X.
Module E := X.
-
- Record slist := {this :> Raw.t; unique : NoDupA E.eq this}.
- Definition t := slist.
- Definition elt := E.t.
-
- Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this).
- Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
- Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
- Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
- Definition For_all (P : elt -> Prop) (s : t) : Prop :=
- forall x : elt, In x s -> P x.
- Definition Exists (P : elt -> Prop) (s : t) : Prop := exists x : elt, In x s /\ P x.
-
- Definition mem (x : elt) (s : t) : bool := Raw.mem x s.
- Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_unique (unique s) x).
- Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_unique (unique s) x).
- Definition singleton (x : elt) : t := Build_slist (Raw.singleton_unique x).
- Definition union (s s' : t) : t :=
- Build_slist (Raw.union_unique (unique s) (unique s')).
- Definition inter (s s' : t) : t :=
- Build_slist (Raw.inter_unique (unique s) (unique s')).
- Definition diff (s s' : t) : t :=
- Build_slist (Raw.diff_unique (unique s) (unique s')).
- Definition equal (s s' : t) : bool := Raw.equal s s'.
- Definition subset (s s' : t) : bool := Raw.subset s s'.
- Definition empty : t := Build_slist Raw.empty_unique.
- Definition is_empty (s : t) : bool := Raw.is_empty s.
- Definition elements (s : t) : list elt := Raw.elements s.
- Definition choose (s:t) : option elt := Raw.choose s.
- Definition fold (B : Type) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s.
- Definition cardinal (s : t) : nat := Raw.cardinal s.
- Definition filter (f : elt -> bool) (s : t) : t :=
- Build_slist (Raw.filter_unique (unique s) f).
- Definition for_all (f : elt -> bool) (s : t) : bool := Raw.for_all f s.
- Definition exists_ (f : elt -> bool) (s : t) : bool := Raw.exists_ f s.
- Definition partition (f : elt -> bool) (s : t) : t * 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)).
-
- Section Spec.
- Variable s s' : t.
- Variable x y : elt.
-
- Lemma In_1 : E.eq x y -> In x s -> In y s.
- Proof. exact (fun H H' => Raw.In_eq H H'). Qed.
-
- Lemma mem_1 : In x s -> mem x s = true.
- Proof. exact (fun H => Raw.mem_1 H). Qed.
- Lemma mem_2 : mem x s = true -> In x s.
- Proof. exact (fun H => Raw.mem_2 H). Qed.
-
- Lemma equal_1 : Equal s s' -> equal s s' = true.
- Proof. exact (Raw.equal_1 s.(unique) s'.(unique)). Qed.
- Lemma equal_2 : equal s s' = true -> Equal s s'.
- Proof. exact (Raw.equal_2 s.(unique) s'.(unique)). Qed.
-
- Lemma subset_1 : Subset s s' -> subset s s' = true.
- Proof. exact (Raw.subset_1 s.(unique) s'.(unique)). Qed.
- Lemma subset_2 : subset s s' = true -> Subset s s'.
- Proof. exact (Raw.subset_2 s.(unique) s'.(unique)). Qed.
-
- Lemma empty_1 : Empty empty.
- Proof. exact Raw.empty_1. Qed.
-
- Lemma is_empty_1 : Empty s -> is_empty s = true.
- Proof. exact (fun H => Raw.is_empty_1 H). Qed.
- Lemma is_empty_2 : is_empty s = true -> Empty s.
- Proof. exact (fun H => Raw.is_empty_2 H). Qed.
-
- Lemma add_1 : E.eq x y -> In y (add x s).
- Proof. exact (fun H => Raw.add_1 s.(unique) H). Qed.
- Lemma add_2 : In y s -> In y (add x s).
- Proof. exact (fun H => Raw.add_2 s.(unique) x H). Qed.
- Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s.
- Proof. exact (fun H => Raw.add_3 s.(unique) H). Qed.
-
- Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
- Proof. exact (fun H => Raw.remove_1 s.(unique) H). Qed.
- Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
- Proof. exact (fun H H' => Raw.remove_2 s.(unique) H H'). Qed.
- Lemma remove_3 : In y (remove x s) -> In y s.
- Proof. exact (fun H => Raw.remove_3 s.(unique) H). Qed.
-
- Lemma singleton_1 : In y (singleton x) -> E.eq x y.
- Proof. exact (fun H => Raw.singleton_1 H). Qed.
- Lemma singleton_2 : E.eq x y -> In y (singleton x).
- Proof. exact (fun H => Raw.singleton_2 H). Qed.
-
- Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
- Proof. exact (fun H => Raw.union_1 s.(unique) s'.(unique) H). Qed.
- Lemma union_2 : In x s -> In x (union s s').
- Proof. exact (fun H => Raw.union_2 s.(unique) s'.(unique) H). Qed.
- Lemma union_3 : In x s' -> In x (union s s').
- Proof. exact (fun H => Raw.union_3 s.(unique) s'.(unique) H). Qed.
-
- Lemma inter_1 : In x (inter s s') -> In x s.
- Proof. exact (fun H => Raw.inter_1 s.(unique) s'.(unique) H). Qed.
- Lemma inter_2 : In x (inter s s') -> In x s'.
- Proof. exact (fun H => Raw.inter_2 s.(unique) s'.(unique) H). Qed.
- Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
- Proof. exact (fun H => Raw.inter_3 s.(unique) s'.(unique) H). Qed.
-
- Lemma diff_1 : In x (diff s s') -> In x s.
- Proof. exact (fun H => Raw.diff_1 s.(unique) s'.(unique) H). Qed.
- Lemma diff_2 : In x (diff s s') -> ~ In x s'.
- Proof. exact (fun H => Raw.diff_2 s.(unique) s'.(unique) H). Qed.
- Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
- Proof. exact (fun H => Raw.diff_3 s.(unique) s'.(unique) H). Qed.
-
- Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
- fold f s i = fold_left (fun a e => f e a) (elements s) i.
- Proof. exact (Raw.fold_1 s.(unique)). Qed.
-
- Lemma cardinal_1 : cardinal s = length (elements s).
- Proof. exact (Raw.cardinal_1 s.(unique)). Qed.
-
- Section Filter.
-
- Variable f : elt -> bool.
-
- Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s.
- Proof. exact (fun H => @Raw.filter_1 s x f). Qed.
- Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true.
- Proof. exact (@Raw.filter_2 s x f). Qed.
- Lemma filter_3 :
- compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
- Proof. exact (@Raw.filter_3 s x f). Qed.
-
- Lemma for_all_1 :
- compat_bool E.eq f ->
- For_all (fun x => f x = true) s -> for_all f s = true.
- Proof. exact (@Raw.for_all_1 s f). Qed.
- Lemma for_all_2 :
- compat_bool E.eq f ->
- for_all f s = true -> For_all (fun x => f x = true) s.
- Proof. exact (@Raw.for_all_2 s f). Qed.
-
- Lemma exists_1 :
- compat_bool E.eq f ->
- Exists (fun x => f x = true) s -> exists_ f s = true.
- Proof. exact (@Raw.exists_1 s f). Qed.
- Lemma exists_2 :
- compat_bool E.eq f ->
- exists_ f s = true -> Exists (fun x => f x = true) s.
- Proof. exact (@Raw.exists_2 s f). Qed.
-
- Lemma partition_1 :
- compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
- Proof. exact (@Raw.partition_1 s f). Qed.
- Lemma partition_2 :
- compat_bool E.eq f ->
- Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
- Proof. exact (@Raw.partition_2 s f). Qed.
-
- End Filter.
-
- Lemma elements_1 : In x s -> InA E.eq x (elements s).
- Proof. exact (fun H => Raw.elements_1 H). Qed.
- Lemma elements_2 : InA E.eq x (elements s) -> In x s.
- Proof. exact (fun H => Raw.elements_2 H). Qed.
- Lemma elements_3w : NoDupA E.eq (elements s).
- Proof. exact (Raw.elements_3w s.(unique)). Qed.
-
- Lemma choose_1 : choose s = Some x -> In x s.
- Proof. exact (fun H => Raw.choose_1 H). Qed.
- Lemma choose_2 : choose s = None -> Empty s.
- Proof. exact (fun H => Raw.choose_2 H). Qed.
-
- End Spec.
-
- Definition eq : t -> t -> Prop := Equal.
-
- Lemma eq_refl : forall s, eq s s.
- Proof. firstorder. Qed.
-
- Lemma eq_sym : forall s s', eq s s' -> eq s' s.
- Proof. firstorder. Qed.
-
- Lemma eq_trans :
- forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
- Proof. firstorder. Qed.
-
- Definition eq_dec : forall (s s':t),
- { eq s s' }+{ ~eq s s' }.
- Proof.
- intros s s'; exact (Raw.eq_dec s.(unique) s'.(unique)).
- Defined.
-
+ Module X' := Equalities.Update_DT X.
+ Module MSet := MSetWeakList.Make X'.
+ Include FSetCompat.Backport_WSets X MSet.
End Make.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 06:53:12 +0000