diff options
Diffstat (limited to 'theories/FSets/FSetFacts.v')
-rw-r--r-- | theories/FSets/FSetFacts.v | 122 |
1 files changed, 61 insertions, 61 deletions
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index b7756592f..5cf2808c5 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetFacts.v,v 1.6 2006/03/13 04:59:24 letouzey Exp $ *) (** * Finite sets library *) (** This functor derives additional facts from [FSetInterface.S]. These facts are mainly the specifications of [FSetInterface.S] written using - different styles equivalence and boolean equalities. + different styles: equivalence and boolean equalities. Moreover, we prove that [E.Eq] and [Equal] are setoid equalities. *) @@ -20,8 +20,8 @@ Require Export FSetInterface. Set Implicit Arguments. Unset Strict Implicit. -Module Facts (M S). -Module ME = OrderedTypeFacts M.E. +Module Facts (M: S). +Module ME := OrderedTypeFacts M.E. Import ME. Import M. Import Logic. (* to unmask [eq] *) @@ -30,108 +30,108 @@ Import Peano. (* to unmask [lt] *) (** * Specifications written using equivalences *) Section IffSpec. -Variable s s' s'' t. -Variable x y z elt. +Variable s s' s'' : t. +Variable x y z : elt. -Lemma In_eq_iff E.eq x y -> (In x s <-> In y s). +Lemma In_eq_iff : E.eq x y -> (In x s <-> In y s). Proof. split; apply In_1; auto. Qed. -Lemma mem_iff In x s <-> mem x s = true. +Lemma mem_iff : In x s <-> mem x s = true. Proof. split; [apply mem_1|apply mem_2]. Qed. -Lemma not_mem_iff ~In x s <-> mem x s = false. +Lemma not_mem_iff : ~In x s <-> mem x s = false. Proof. rewrite mem_iff; destruct (mem x s); intuition. Qed. -Lemma equal_iff s[=]s' <-> equal s s' = true. +Lemma equal_iff : s[=]s' <-> equal s s' = true. Proof. split; [apply equal_1|apply equal_2]. Qed. -Lemma subset_iff s[<=]s' <-> subset s s' = true. +Lemma subset_iff : s[<=]s' <-> subset s s' = true. Proof. split; [apply subset_1|apply subset_2]. Qed. -Lemma empty_iff In x empty <-> False. +Lemma empty_iff : In x empty <-> False. Proof. intuition; apply (empty_1 H). Qed. -Lemma is_empty_iff Empty s <-> is_empty s = true. +Lemma is_empty_iff : Empty s <-> is_empty s = true. Proof. split; [apply is_empty_1|apply is_empty_2]. Qed. -Lemma singleton_iff In y (singleton x) <-> E.eq x y. +Lemma singleton_iff : In y (singleton x) <-> E.eq x y. Proof. split; [apply singleton_1|apply singleton_2]. Qed. -Lemma add_iff In y (add x s) <-> E.eq x y \/ In y s. +Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s. Proof. split; [ | destruct 1; [apply add_1|apply add_2]]; auto. destruct (eq_dec x y) as [E|E]; auto. intro H; right; exact (add_3 E H). Qed. -Lemma add_neq_iff ~ E.eq x y -> (In y (add x s) <-> In y s). +Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s) <-> In y s). Proof. split; [apply add_3|apply add_2]; auto. Qed. -Lemma remove_iff In y (remove x s) <-> In y s /\ ~E.eq x y. +Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y. Proof. split; [split; [apply remove_3 with x |] | destruct 1; apply remove_2]; auto. intro. apply (remove_1 H0 H). Qed. -Lemma remove_neq_iff ~ E.eq x y -> (In y (remove x s) <-> In y s). +Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s). Proof. split; [apply remove_3|apply remove_2]; auto. Qed. -Lemma union_iff In x (union s s') <-> In x s \/ In x s'. +Lemma union_iff : In x (union s s') <-> In x s \/ In x s'. Proof. split; [apply union_1 | destruct 1; [apply union_2|apply union_3]]; auto. Qed. -Lemma inter_iff In x (inter s s') <-> In x s /\ In x s'. +Lemma inter_iff : In x (inter s s') <-> In x s /\ In x s'. Proof. split; [split; [apply inter_1 with s' | apply inter_2 with s] | destruct 1; apply inter_3]; auto. Qed. -Lemma diff_iff In x (diff s s') <-> In x s /\ ~ In x s'. +Lemma diff_iff : In x (diff s s') <-> In x s /\ ~ In x s'. Proof. split; [split; [apply diff_1 with s' | apply diff_2 with s] | destruct 1; apply diff_3]; auto. Qed. -Variable f elt->bool. +Variable f : elt->bool. -Lemma filter_iff compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true). +Lemma filter_iff : compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true). Proof. split; [split; [apply filter_1 with f | apply filter_2 with s] | destruct 1; apply filter_3]; auto. Qed. -Lemma for_all_iff compat_bool E.eq f -> +Lemma for_all_iff : compat_bool E.eq f -> (For_all (fun x => f x = true) s <-> for_all f s = true). Proof. split; [apply for_all_1 | apply for_all_2]; auto. Qed. -Lemma exists_iff compat_bool E.eq f -> +Lemma exists_iff : compat_bool E.eq f -> (Exists (fun x => f x = true) s <-> exists_ f s = true). Proof. split; [apply exists_1 | apply exists_2]; auto. Qed. -Lemma elements_iff In x s <-> ME.In x (elements s). +Lemma elements_iff : In x s <-> ME.In x (elements s). Proof. split; [apply elements_1 | apply elements_2]. Qed. @@ -140,7 +140,7 @@ End IffSpec. (** Useful tactic for simplifying expressions like [In y (add x (union s s'))] *) -Ltac set_iff = +Ltac set_iff := repeat (progress ( rewrite add_iff || rewrite remove_iff || rewrite singleton_iff || rewrite union_iff || rewrite inter_iff || rewrite diff_iff @@ -149,65 +149,65 @@ Ltac set_iff = (** * Specifications written using boolean predicates *) Section BoolSpec. -Variable s s' s'' t. -Variable x y z elt. +Variable s s' s'' : t. +Variable x y z : elt. -Lemma mem_b E.eq x y -> mem x s = mem y s. +Lemma mem_b : E.eq x y -> mem x s = mem y s. Proof. intros. generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H). destruct (mem x s); destruct (mem y s); intuition. Qed. -Lemma add_b mem y (add x s) = eqb x y || mem y s. +Lemma add_b : mem y (add x s) = eqb x y || mem y s. Proof. generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb. destruct (eq_dec x y); destruct (mem y s); destruct (mem y (add x s)); intuition. Qed. -Lemma add_neq_b ~ E.eq x y -> mem y (add x s) = mem y s. +Lemma add_neq_b : ~ E.eq x y -> mem y (add x s) = mem y s. Proof. intros; generalize (mem_iff (add x s) y)(mem_iff s y)(add_neq_iff s H). destruct (mem y s); destruct (mem y (add x s)); intuition. Qed. -Lemma remove_b mem y (remove x s) = mem y s && negb (eqb x y). +Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y). Proof. generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_iff s x y); unfold eqb. destruct (eq_dec x y); destruct (mem y s); destruct (mem y (remove x s)); simpl; intuition. Qed. -Lemma remove_neq_b ~ E.eq x y -> mem y (remove x s) = mem y s. +Lemma remove_neq_b : ~ E.eq x y -> mem y (remove x s) = mem y s. Proof. intros; generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_neq_iff s H). destruct (mem y s); destruct (mem y (remove x s)); intuition. Qed. -Lemma singleton_b mem y (singleton x) = eqb x y. +Lemma singleton_b : mem y (singleton x) = eqb x y. Proof. generalize (mem_iff (singleton x) y)(singleton_iff x y); unfold eqb. destruct (eq_dec x y); destruct (mem y (singleton x)); intuition. Qed. -Lemma union_b mem x (union s s') = mem x s || mem x s'. +Lemma union_b : mem x (union s s') = mem x s || mem x s'. Proof. generalize (mem_iff (union s s') x)(mem_iff s x)(mem_iff s' x)(union_iff s s' x). destruct (mem x s); destruct (mem x s'); destruct (mem x (union s s')); intuition. Qed. -Lemma inter_b mem x (inter s s') = mem x s && mem x s'. +Lemma inter_b : mem x (inter s s') = mem x s && mem x s'. Proof. generalize (mem_iff (inter s s') x)(mem_iff s x)(mem_iff s' x)(inter_iff s s' x). destruct (mem x s); destruct (mem x s'); destruct (mem x (inter s s')); intuition. Qed. -Lemma diff_b mem x (diff s s') = mem x s && negb (mem x s'). +Lemma diff_b : mem x (diff s s') = mem x s && negb (mem x s'). Proof. generalize (mem_iff (diff s s') x)(mem_iff s x)(mem_iff s' x)(diff_iff s s' x). destruct (mem x s); destruct (mem x s'); destruct (mem x (diff s s')); simpl; intuition. Qed. -Lemma elements_b mem x s = existsb (eqb x) (elements s). +Lemma elements_b : mem x s = existsb (eqb x) (elements s). Proof. generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)). rewrite InA_alt. @@ -226,16 +226,16 @@ exists a; intuition. unfold eqb in *; destruct (eq_dec x a); auto; discriminate. Qed. -Variable f elt->bool. +Variable f : elt->bool. -Lemma filter_b compat_bool E.eq f -> mem x (filter f s) = mem x s && f x. +Lemma filter_b : compat_bool E.eq f -> mem x (filter f s) = mem x s && f x. Proof. intros. generalize (mem_iff (filter f s) x)(mem_iff s x)(filter_iff s x H). destruct (mem x s); destruct (mem x (filter f s)); destruct (f x); simpl; intuition. Qed. -Lemma for_all_b compat_bool E.eq f -> +Lemma for_all_b : compat_bool E.eq f -> for_all f s = forallb f (elements s). Proof. intros. @@ -255,7 +255,7 @@ destruct H1 as (_,H1). apply H1; auto. Qed. -Lemma exists_b compat_bool E.eq f -> +Lemma exists_b : compat_bool E.eq f -> exists_ f s = existsb f (elements s). Proof. intros. @@ -281,27 +281,27 @@ End BoolSpec. (** * [E.eq] and [Equal] are setoid equalities *) -Definition E_ST Setoid_Theory elt E.eq. +Definition E_ST : Setoid_Theory elt E.eq. Proof. constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. Qed. Add Setoid elt E.eq E_ST as EltSetoid. -Definition Equal_ST Setoid_Theory t Equal. +Definition Equal_ST : Setoid_Theory t Equal. Proof. constructor; [apply eq_refl | apply eq_sym | apply eq_trans]. Qed. Add Setoid t Equal Equal_ST as EqualSetoid. -Add Morphism In In_m. +Add Morphism In : In_m. Proof. unfold Equal; intros x y H s s' H0. rewrite (In_eq_iff s H); auto. Qed. -Add Morphism is_empty is_empty_m. +Add Morphism is_empty : is_empty_m. Proof. unfold Equal; intros s s' H. generalize (is_empty_iff s)(is_empty_iff s'). @@ -318,12 +318,12 @@ destruct H1 as (_,H1). exact (H1 (refl_equal true) _ Ha). Qed. -Add Morphism Empty Empty_m. +Add Morphism Empty : Empty_m. Proof. intros; do 2 rewrite is_empty_iff; rewrite H; intuition. Qed. -Add Morphism mem mem_m. +Add Morphism mem : mem_m. Proof. unfold Equal; intros x y H s s' H0. generalize (H0 x); clear H0; rewrite (In_eq_iff s' H). @@ -331,48 +331,48 @@ generalize (mem_iff s x)(mem_iff s' y). destruct (mem x s); destruct (mem y s'); intuition. Qed. -Add Morphism singleton singleton_m. +Add Morphism singleton : singleton_m. Proof. unfold Equal; intros x y H a. do 2 rewrite singleton_iff; split; order. Qed. -Add Morphism add add_m. +Add Morphism add : add_m. Proof. unfold Equal; intros x y H s s' H0 a. do 2 rewrite add_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism remove remove_m. +Add Morphism remove : remove_m. Proof. unfold Equal; intros x y H s s' H0 a. do 2 rewrite remove_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism union union_m. +Add Morphism union : union_m. Proof. unfold Equal; intros s s' H s'' s''' H0 a. do 2 rewrite union_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism inter inter_m. +Add Morphism inter : inter_m. Proof. unfold Equal; intros s s' H s'' s''' H0 a. do 2 rewrite inter_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism diff diff_m. +Add Morphism diff : diff_m. Proof. unfold Equal; intros s s' H s'' s''' H0 a. do 2 rewrite diff_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism Subset Subset_m. +Add Morphism Subset : Subset_m. Proof. unfold Equal, Subset; firstorder. Qed. -Add Morphism subset subset_m. +Add Morphism subset : subset_m. Proof. intros s s' H s'' s''' H0. generalize (subset_iff s s'') (subset_iff s' s'''). @@ -381,7 +381,7 @@ rewrite H in H1; rewrite H0 in H1; intuition. rewrite H in H1; rewrite H0 in H1; intuition. Qed. -Add Morphism equal equal_m. +Add Morphism equal : equal_m. Proof. intros s s' H s'' s''' H0. generalize (equal_iff s s'') (equal_iff s' s'''). @@ -391,9 +391,9 @@ rewrite H in H1; rewrite H0 in H1; intuition. Qed. (* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism - without additional hypothesis on [f]. For instance *) + without additional hypothesis on [f]. For instance: *) -Lemma filter_equal forall f, compat_bool E.eq f -> +Lemma filter_equal : forall f, compat_bool E.eq f -> forall s s', s[=]s' -> filter f s [=] filter f s'. Proof. unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto. @@ -402,7 +402,7 @@ Qed. (* For [elements], [min_elt], [max_elt] and [choose], we would need setoid structures on [list elt] and [option elt]. *) -(* Later +(* Later: Add Morphism cardinal ; cardinal_m. *) |