diff options
Diffstat (limited to 'theories/FSets/FSetWeakList.v')
-rw-r--r-- | theories/FSets/FSetWeakList.v | 492 |
1 files changed, 246 insertions, 246 deletions
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 0a13ee78e..bcd966f9a 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetWeakList.v,v 1.8 2006/03/09 18:34:51 letouzey Exp $ *) (** * Finite sets library *) @@ -23,116 +23,116 @@ Unset Strict Implicit. 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 Raw (X: DecidableType). - Module E = X. + Module E := X. - Definition elt = X.t. - Definition t = list elt. + Definition elt := X.t. + Definition t := list elt. - Definition empty t := nil. + Definition empty : t := nil. - Definition is_empty (l t) : bool := if l then true else false. + Definition is_empty (l : t) : bool := if l then true else false. (** ** The set operations. *) - Fixpoint mem (x elt) (s : t) {struct s} : bool := + Fixpoint mem (x : elt) (s : t) {struct s} : bool := match s with | nil => false - | y : l => + | y :: l => if X.eq_dec x y then true else mem x l end. - Fixpoint add (x elt) (s : t) {struct s} : t := + 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 + | 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. + Definition singleton (x : elt) : t := x :: nil. - Fixpoint remove (x elt) (s : t) {struct s} : t := + 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 + | 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 + 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) + | x :: l => fold f l (f x i) end. - Definition union (s t) : t -> t := fold add s. + Definition union (s : t) : t -> t := fold add s. - Definition diff (s s' t) : t := fold remove s' s. + Definition diff (s s' : t) : t := fold remove s' s. - Definition inter (s s' t) : t := + 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 subset (s s' : t) : bool := is_empty (diff s s'). - Definition equal (s s' t) : bool := andb (subset s s') (subset 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 := + 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 + | 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 := + 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 + | x :: l => if f x then for_all f l else false end. - Fixpoint exists_ (f elt -> bool) (s : t) {struct s} : bool := + 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 + | x :: l => if f x then true else exists_ f l end. - Fixpoint partition (f elt -> bool) (s : t) {struct s} : - t * t = + 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) + | 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 cardinal (s : t) : nat := length s. - Definition elements (s t) : list elt := s. + Definition elements (s : t) : list elt := s. - Definition choose (s t) : option elt := + Definition choose (s : t) : option elt := match s with | nil => None - | x:_ => Some x + | x::_ => Some x end. (** ** Proofs of set operation specifications. *) - Notation NoRedun = (noredunA X.eq). - Notation In = (InA X.eq). + Notation NoRedun := (noredunA 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. + 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. + 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. + Lemma mem_1 : + forall (s : t)(x : elt), In x s -> mem x s = true. Proof. induction s; intros. inversion H. @@ -140,7 +140,7 @@ Module Raw (X DecidableType). inversion_clear H; auto. Qed. - Lemma mem_2 forall (s : t) (x : elt), mem x s = true -> In x s. + Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s. Proof. induction s. intros; inversion H. @@ -148,8 +148,8 @@ Module Raw (X DecidableType). destruct (X.eq_dec x a); firstorder; discriminate. Qed. - Lemma add_1 - forall (s t) (Hs : NoRedun s) (x y : elt), X.eq x y -> In y (add x s). + Lemma add_1 : + forall (s : t) (Hs : NoRedun s) (x y : elt), X.eq x y -> In y (add x s). Proof. induction s. simpl; intuition. @@ -158,8 +158,8 @@ Module Raw (X DecidableType). eauto. Qed. - Lemma add_2 - forall (s t) (Hs : NoRedun s) (x y : elt), In y s -> In y (add x s). + Lemma add_2 : + forall (s : t) (Hs : NoRedun s) (x y : elt), In y s -> In y (add x s). Proof. induction s. simpl; intuition. @@ -167,8 +167,8 @@ Module Raw (X DecidableType). inversion_clear Hs; eauto; inversion_clear H; intuition. Qed. - Lemma add_3 - forall (s t) (Hs : NoRedun s) (x y : elt), + Lemma add_3 : + forall (s : t) (Hs : NoRedun s) (x y : elt), ~ X.eq x y -> In y (add x s) -> In y s. Proof. induction s. @@ -179,8 +179,8 @@ Module Raw (X DecidableType). absurd (X.eq x y); auto. Qed. - Lemma add_unique - forall (s t) (Hs : NoRedun s)(x:elt), NoRedun (add x s). + Lemma add_unique : + forall (s : t) (Hs : NoRedun s)(x:elt), NoRedun (add x s). Proof. induction s. simpl; intuition. @@ -196,8 +196,8 @@ Module Raw (X DecidableType). eapply add_3; eauto. Qed. - Lemma remove_1 - forall (s t) (Hs : NoRedun s) (x y : elt), X.eq x y -> ~ In y (remove x s). + Lemma remove_1 : + forall (s : t) (Hs : NoRedun s) (x y : elt), X.eq x y -> ~ In y (remove x s). Proof. simple induction s. simpl; red; intros; inversion H0. @@ -207,8 +207,8 @@ Module Raw (X DecidableType). inversion_clear H1; eauto. Qed. - Lemma remove_2 - forall (s t) (Hs : NoRedun s) (x y : elt), + Lemma remove_2 : + forall (s : t) (Hs : NoRedun s) (x y : elt), ~ X.eq x y -> In y s -> In y (remove x s). Proof. simple induction s. @@ -218,8 +218,8 @@ Module Raw (X DecidableType). absurd (X.eq x y); eauto. Qed. - Lemma remove_3 - forall (s t) (Hs : NoRedun s) (x y : elt), In y (remove x s) -> In y s. + Lemma remove_3 : + forall (s : t) (Hs : NoRedun s) (x y : elt), In y (remove x s) -> In y s. Proof. simple induction s. simpl; intuition. @@ -227,8 +227,8 @@ Module Raw (X DecidableType). inversion_clear Hs; inversion_clear H; firstorder. Qed. - Lemma remove_unique - forall (s t) (Hs : NoRedun s) (x : elt), NoRedun (remove x s). + Lemma remove_unique : + forall (s : t) (Hs : NoRedun s) (x : elt), NoRedun (remove x s). Proof. simple induction s. simpl; intuition. @@ -239,69 +239,69 @@ Module Raw (X DecidableType). eapply remove_3; eauto. Qed. - Lemma singleton_unique forall x : elt, NoRedun (singleton x). + Lemma singleton_unique : forall x : elt, NoRedun (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. + 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). + Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x). Proof. unfold singleton; simpl; intuition. Qed. - Lemma empty_unique NoRedun empty. + Lemma empty_unique : NoRedun empty. Proof. unfold empty; constructor. Qed. - Lemma empty_1 Empty empty. + 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. + 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. + 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). + 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. + 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 : NoRedun s), NoRedun (elements s). + Lemma elements_3 : forall (s : t) (Hs : NoRedun s), NoRedun (elements s). Proof. unfold elements; auto. Qed. - Lemma fold_1 - forall (s t) (Hs : NoRedun s) (A : Set) (i : A) (f : elt -> A -> A), + Lemma fold_1 : + forall (s : t) (Hs : NoRedun 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 : NoRedun s) (Hs' : NoRedun s'), NoRedun (union s s'). + Lemma union_unique : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (union s s'). Proof. unfold union; induction s; simpl; auto; intros. inversion_clear Hs. @@ -309,8 +309,8 @@ Module Raw (X DecidableType). apply add_unique; auto. Qed. - Lemma union_1 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma union_1 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), In x (union s s') -> In x s \/ In x s'. Proof. unfold union; induction s; simpl; auto; intros. @@ -321,8 +321,8 @@ Module Raw (X DecidableType). right; eapply add_3; eauto. Qed. - Lemma union_0 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma union_0 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), In x s \/ In x s' -> In x (union s s'). Proof. unfold union; induction s; simpl; auto; intros. @@ -337,25 +337,25 @@ Module Raw (X DecidableType). right; apply add_2; auto. Qed. - Lemma union_2 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma union_2 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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 : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma union_3 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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 : NoRedun s) (Hs' : NoRedun s'), NoRedun (inter s s'). + Lemma inter_unique : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (inter s s'). Proof. unfold inter; intros s. - set (acc = nil (A:=elt)). + set (acc := nil (A:=elt)). assert (NoRedun acc) by (unfold acc; auto). clearbody acc; generalize H; clear H; generalize acc; clear acc. induction s; simpl; auto; intros. @@ -365,12 +365,12 @@ Module Raw (X DecidableType). apply add_unique; auto. Qed. - Lemma inter_0 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma inter_0 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), In x (inter s s') -> In x s /\ In x s'. Proof. unfold inter; intros. - set (acc = nil (A:=elt)) in *. + set (acc := nil (A:=elt)) in *. assert (NoRedun acc) by (unfold acc; auto). cut ((In x s /\ In x s') \/ In x acc). destruct 1; auto. @@ -392,29 +392,29 @@ Module Raw (X DecidableType). left; intuition. Qed. - Lemma inter_1 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma inter_1 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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 : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma inter_2 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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 : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma inter_3 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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')). + 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 *. + set (acc := nil (A:=elt)) in *. assert (NoRedun acc) by (unfold acc; auto). clearbody acc. generalize H Hs' Hs; clear H Hs Hs'. @@ -440,8 +440,8 @@ Module Raw (X DecidableType). discriminate. Qed. - Lemma diff_unique - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (diff s s'). + Lemma diff_unique : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (diff s s'). Proof. unfold diff; intros s s' Hs; generalize s Hs; clear Hs s. induction s'; simpl; auto; intros. @@ -450,8 +450,8 @@ Module Raw (X DecidableType). apply remove_unique; auto. Qed. - Lemma diff_0 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma diff_0 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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. @@ -467,22 +467,22 @@ Module Raw (X DecidableType). destruct (remove_1 Hs (X.eq_sym H5) H2). Qed. - Lemma diff_1 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma diff_1 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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 : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma diff_2 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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 : NoRedun s) (Hs' : NoRedun s') (x : elt), + Lemma diff_3 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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. @@ -493,8 +493,8 @@ Module Raw (X DecidableType). apply remove_2; auto. Qed. - Lemma subset_1 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s'), + Lemma subset_1 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), Subset s s' -> subset s s' = true. Proof. unfold subset, Subset; intros. @@ -506,7 +506,7 @@ Module Raw (X DecidableType). eapply diff_1; eauto. Qed. - Lemma subset_2 forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'), + Lemma subset_2 : forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'), subset s s' = true -> Subset s s'. Proof. unfold subset, Subset; intros. @@ -518,15 +518,15 @@ Module Raw (X DecidableType). apply diff_3; intuition. Qed. - Lemma equal_1 - forall (s s' t) (Hs : NoRedun s) (Hs' : NoRedun s'), + Lemma equal_1 : + forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun 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 : NoRedun s) (Hs' : NoRedun s'), + Lemma equal_2 : forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'), equal s s' = true -> Equal s s'. Proof. unfold Equal, equal; intros. @@ -534,27 +534,27 @@ Module Raw (X DecidableType). split; apply subset_2; auto. Qed. - Definition choose_1 - forall (s t) (x : elt), choose s = Some x -> In x s. + 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. + 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 : NoRedun s), cardinal s = length (elements s). + Lemma cardinal_1 : + forall (s : t) (Hs : NoRedun s), cardinal s = length (elements s). Proof. auto. Qed. - Lemma filter_1 - forall (s t) (x : elt) (f : elt -> bool), + Lemma filter_1 : + forall (s : t) (x : elt) (f : elt -> bool), In x (filter f s) -> In x s. Proof. simple induction s; simpl. @@ -567,8 +567,8 @@ Module Raw (X DecidableType). constructor 2; apply (Hrec a f); trivial. Qed. - Lemma filter_2 - forall (s t) (x : elt) (f : elt -> bool), + 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. @@ -579,8 +579,8 @@ Module Raw (X DecidableType). symmetry; auto. Qed. - Lemma filter_3 - forall (s t) (x : elt) (f : elt -> bool), + 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. @@ -592,8 +592,8 @@ Module Raw (X DecidableType). rewrite <- (H a (X.eq_sym H1)); intros; discriminate. Qed. - Lemma filter_unique - forall (s t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (filter f s). + Lemma filter_unique : + forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (filter f s). Proof. simple induction s; simpl. auto. @@ -605,8 +605,8 @@ Module Raw (X DecidableType). Qed. - Lemma for_all_1 - forall (s t) (f : elt -> bool), + 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. @@ -617,8 +617,8 @@ Module Raw (X DecidableType). intros; rewrite (H x); auto. Qed. - Lemma for_all_2 - forall (s t) (f : elt -> bool), + 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. @@ -633,8 +633,8 @@ Module Raw (X DecidableType). rewrite (Hf a x); auto. Qed. - Lemma exists_1 - forall (s t) (f : elt -> bool), + 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. @@ -651,8 +651,8 @@ Module Raw (X DecidableType). exists a; auto. Qed. - Lemma exists_2 - forall (s t) (f : elt -> bool), + 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. @@ -664,8 +664,8 @@ Module Raw (X DecidableType). exists a; auto. Qed. - Lemma partition_1 - forall (s t) (f : elt -> bool), + 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. @@ -676,8 +676,8 @@ Module Raw (X DecidableType). case (f x); simpl; firstorder; inversion H0; intros; firstorder. Qed. - Lemma partition_2 - forall (s t) (f : elt -> bool), + 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. @@ -689,8 +689,8 @@ Module Raw (X DecidableType). case (f x); simpl; firstorder; inversion H0; intros; firstorder. Qed. - Lemma partition_aux_1 - forall (s t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), + Lemma partition_aux_1 : + forall (s : t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), In x (fst (partition f s)) -> In x s. Proof. induction s; simpl; auto; intros. @@ -700,8 +700,8 @@ Module Raw (X DecidableType). inversion_clear H; auto. Qed. - Lemma partition_aux_2 - forall (s t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), + Lemma partition_aux_2 : + forall (s : t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), In x (snd (partition f s)) -> In x s. Proof. induction s; simpl; auto; intros. @@ -711,8 +711,8 @@ Module Raw (X DecidableType). inversion_clear H; auto. Qed. - Lemma partition_unique_1 - forall (s t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (fst (partition f s)). + Lemma partition_unique_1 : + forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (fst (partition f s)). Proof. simple induction s; simpl. auto. @@ -722,8 +722,8 @@ Module Raw (X DecidableType). case (f x); case (partition f l); simpl; auto. Qed. - Lemma partition_unique_2 - forall (s t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (snd (partition f s)). + Lemma partition_unique_2 : + forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (snd (partition f s)). Proof. simple induction s; simpl. auto. @@ -733,19 +733,19 @@ Module Raw (X DecidableType). case (f x); case (partition f l); simpl; auto. Qed. - Definition eq t -> t -> Prop := Equal. + Definition eq : t -> t -> Prop := Equal. - Lemma eq_refl forall s : t, eq s s. + 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. + 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''. + Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''. Proof. unfold eq, Equal; firstorder. Qed. @@ -757,117 +757,117 @@ End Raw. 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 Make (X: DecidableType) <: S with Module E := X. - Module E = X. - Module Raw = Raw X. + Module E := X. + Module Raw := Raw X. - Record slist Set := {this :> Raw.t; unique : noredunA X.eq this}. - Definition t = slist. - Definition elt = X.t. + Record slist : Set := {this :> Raw.t; unique : noredunA 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 (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 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 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 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) := + 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 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) := + 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 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) := + 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 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 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 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 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 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 (st) := Raw.choose s. - Definition choose_1 (s t) := Raw.choose_1 (s:=s). - Definition choose_2 (s t) := Raw.choose_2 (s:=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 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 cardinal (s : t) := Raw.cardinal s. + Definition cardinal_1 (s : t) := Raw.cardinal_1 (unique s). - Definition filter (f elt -> bool) (s : t) := + 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) := + 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 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''). + 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. |