diff options
Diffstat (limited to 'theories/MSets/MSetFacts.v')
| -rw-r--r-- | theories/MSets/MSetFacts.v | 528 |
1 files changed, 528 insertions, 0 deletions
diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v new file mode 100644 index 00000000..6d38b696 --- /dev/null +++ b/theories/MSets/MSetFacts.v @@ -0,0 +1,528 @@ +(***********************************************************************) +(* 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$ *) + +(** * Finite sets library *) + +(** This functor derives additional facts from [MSetInterface.S]. These + facts are mainly the specifications of [MSetInterface.S] written using + different styles: equivalence and boolean equalities. + Moreover, we prove that [E.Eq] and [Equal] are setoid equalities. +*) + +Require Import DecidableTypeEx. +Require Export MSetInterface. +Set Implicit Arguments. +Unset Strict Implicit. + +(** First, a functor for Weak Sets in functorial version. *) + +Module WFactsOn (Import E : DecidableType)(Import M : WSetsOn E). + +Notation eq_dec := E.eq_dec. +Definition eqb x y := if eq_dec x y then true else false. + +(** * Specifications written using implications : + this used to be the default interface. *) + +Section ImplSpec. +Variable s s' : t. +Variable x y : elt. + +Lemma In_1 : E.eq x y -> In x s -> In y s. +Proof. intros E; rewrite E; auto. Qed. + +Lemma mem_1 : In x s -> mem x s = true. +Proof. intros; apply <- mem_spec; auto. Qed. +Lemma mem_2 : mem x s = true -> In x s. +Proof. intros; apply -> mem_spec; auto. Qed. + +Lemma equal_1 : Equal s s' -> equal s s' = true. +Proof. intros; apply <- equal_spec; auto. Qed. +Lemma equal_2 : equal s s' = true -> Equal s s'. +Proof. intros; apply -> equal_spec; auto. Qed. + +Lemma subset_1 : Subset s s' -> subset s s' = true. +Proof. intros; apply <- subset_spec; auto. Qed. +Lemma subset_2 : subset s s' = true -> Subset s s'. +Proof. intros; apply -> subset_spec; auto. Qed. + +Lemma is_empty_1 : Empty s -> is_empty s = true. +Proof. intros; apply <- is_empty_spec; auto. Qed. +Lemma is_empty_2 : is_empty s = true -> Empty s. +Proof. intros; apply -> is_empty_spec; auto. Qed. + +Lemma add_1 : E.eq x y -> In y (add x s). +Proof. intros; apply <- add_spec. auto with relations. Qed. +Lemma add_2 : In y s -> In y (add x s). +Proof. intros; apply <- add_spec; auto. Qed. +Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. +Proof. rewrite add_spec. intros H [H'|H']; auto. elim H; auto with relations. Qed. + +Lemma remove_1 : E.eq x y -> ~ In y (remove x s). +Proof. intros; rewrite remove_spec; intuition. Qed. +Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). +Proof. intros; apply <- remove_spec; auto with relations. Qed. +Lemma remove_3 : In y (remove x s) -> In y s. +Proof. rewrite remove_spec; intuition. Qed. + +Lemma singleton_1 : In y (singleton x) -> E.eq x y. +Proof. rewrite singleton_spec; auto with relations. Qed. +Lemma singleton_2 : E.eq x y -> In y (singleton x). +Proof. rewrite singleton_spec; auto with relations. Qed. + +Lemma union_1 : In x (union s s') -> In x s \/ In x s'. +Proof. rewrite union_spec; auto. Qed. +Lemma union_2 : In x s -> In x (union s s'). +Proof. rewrite union_spec; auto. Qed. +Lemma union_3 : In x s' -> In x (union s s'). +Proof. rewrite union_spec; auto. Qed. + +Lemma inter_1 : In x (inter s s') -> In x s. +Proof. rewrite inter_spec; intuition. Qed. +Lemma inter_2 : In x (inter s s') -> In x s'. +Proof. rewrite inter_spec; intuition. Qed. +Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). +Proof. rewrite inter_spec; intuition. Qed. + +Lemma diff_1 : In x (diff s s') -> In x s. +Proof. rewrite diff_spec; intuition. Qed. +Lemma diff_2 : In x (diff s s') -> ~ In x s'. +Proof. rewrite diff_spec; intuition. Qed. +Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). +Proof. rewrite diff_spec; auto. Qed. + +Variable f : elt -> bool. +Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing). + +Lemma filter_1 : compatb f -> In x (filter f s) -> In x s. +Proof. intros P; rewrite filter_spec; intuition. Qed. +Lemma filter_2 : compatb f -> In x (filter f s) -> f x = true. +Proof. intros P; rewrite filter_spec; intuition. Qed. +Lemma filter_3 : compatb f -> In x s -> f x = true -> In x (filter f s). +Proof. intros P; rewrite filter_spec; intuition. Qed. + +Lemma for_all_1 : compatb f -> + For_all (fun x => f x = true) s -> for_all f s = true. +Proof. intros; apply <- for_all_spec; auto. Qed. +Lemma for_all_2 : compatb f -> + for_all f s = true -> For_all (fun x => f x = true) s. +Proof. intros; apply -> for_all_spec; auto. Qed. + +Lemma exists_1 : compatb f -> + Exists (fun x => f x = true) s -> exists_ f s = true. +Proof. intros; apply <- exists_spec; auto. Qed. + +Lemma exists_2 : compatb f -> + exists_ f s = true -> Exists (fun x => f x = true) s. +Proof. intros; apply -> exists_spec; auto. Qed. + +Lemma elements_1 : In x s -> InA E.eq x (elements s). +Proof. intros; apply <- elements_spec1; auto. Qed. +Lemma elements_2 : InA E.eq x (elements s) -> In x s. +Proof. intros; apply -> elements_spec1; auto. Qed. + +End ImplSpec. + +Notation empty_1 := empty_spec (only parsing). +Notation fold_1 := fold_spec (only parsing). +Notation cardinal_1 := cardinal_spec (only parsing). +Notation partition_1 := partition_spec1 (only parsing). +Notation partition_2 := partition_spec2 (only parsing). +Notation choose_1 := choose_spec1 (only parsing). +Notation choose_2 := choose_spec2 (only parsing). +Notation elements_3w := elements_spec2w (only parsing). + +Hint Resolve mem_1 equal_1 subset_1 empty_1 + is_empty_1 choose_1 choose_2 add_1 add_2 remove_1 + remove_2 singleton_2 union_1 union_2 union_3 + inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1 + partition_1 partition_2 elements_1 elements_3w + : set. +Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3 + remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2 + filter_1 filter_2 for_all_2 exists_2 elements_2 + : set. + + +(** * Specifications written using equivalences : + this is now provided by the default interface. *) + +Section IffSpec. +Variable s s' s'' : t. +Variable x y z : elt. + +Lemma In_eq_iff : E.eq x y -> (In x s <-> In y s). +Proof. +intros E; rewrite E; intuition. +Qed. + +Lemma mem_iff : In x s <-> mem x s = true. +Proof. apply iff_sym, mem_spec. Qed. + +Lemma not_mem_iff : ~In x s <-> mem x s = false. +Proof. +rewrite <-mem_spec; destruct (mem x s); intuition. +Qed. + +Lemma equal_iff : s[=]s' <-> equal s s' = true. +Proof. apply iff_sym, equal_spec. Qed. + +Lemma subset_iff : s[<=]s' <-> subset s s' = true. +Proof. apply iff_sym, subset_spec. Qed. + +Lemma empty_iff : In x empty <-> False. +Proof. intuition; apply (empty_spec H). Qed. + +Lemma is_empty_iff : Empty s <-> is_empty s = true. +Proof. apply iff_sym, is_empty_spec. Qed. + +Lemma singleton_iff : In y (singleton x) <-> E.eq x y. +Proof. rewrite singleton_spec; intuition. Qed. + +Lemma add_iff : In y (add x s) <-> E.eq x y \/ In y s. +Proof. rewrite add_spec; intuition. Qed. + +Lemma add_neq_iff : ~ E.eq x y -> (In y (add x s) <-> In y s). +Proof. rewrite add_spec; intuition. elim H; auto with relations. Qed. + +Lemma remove_iff : In y (remove x s) <-> In y s /\ ~E.eq x y. +Proof. rewrite remove_spec; intuition. Qed. + +Lemma remove_neq_iff : ~ E.eq x y -> (In y (remove x s) <-> In y s). +Proof. rewrite remove_spec; intuition. Qed. + +Variable f : elt -> bool. + +Lemma for_all_iff : Proper (E.eq==>Logic.eq) f -> + (For_all (fun x => f x = true) s <-> for_all f s = true). +Proof. intros; apply iff_sym, for_all_spec; auto. Qed. + +Lemma exists_iff : Proper (E.eq==>Logic.eq) f -> + (Exists (fun x => f x = true) s <-> exists_ f s = true). +Proof. intros; apply iff_sym, exists_spec; auto. Qed. + +Lemma elements_iff : In x s <-> InA E.eq x (elements s). +Proof. apply iff_sym, elements_spec1. Qed. + +End IffSpec. + +Notation union_iff := union_spec (only parsing). +Notation inter_iff := inter_spec (only parsing). +Notation diff_iff := diff_spec (only parsing). +Notation filter_iff := filter_spec (only parsing). + +(** Useful tactic for simplifying expressions like [In y (add x (union s s'))] *) + +Ltac set_iff := + repeat (progress ( + rewrite add_iff || rewrite remove_iff || rewrite singleton_iff + || rewrite union_iff || rewrite inter_iff || rewrite diff_iff + || rewrite empty_iff)). + +(** * Specifications written using boolean predicates *) + +Section BoolSpec. +Variable s s' s'' : t. +Variable x y z : elt. + +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 empty_b : mem y empty = false. +Proof. +generalize (empty_iff y)(mem_iff empty y). +destruct (mem y empty); intuition. +Qed. + +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. +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). +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. +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. +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'. +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'. +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'). +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). +Proof. +generalize (mem_iff s x)(elements_iff s x)(existsb_exists (eqb x) (elements s)). +rewrite InA_alt. +destruct (mem x s); destruct (existsb (eqb x) (elements s)); auto; intros. +symmetry. +rewrite H1. +destruct H0 as (H0,_). +destruct H0 as (a,(Ha1,Ha2)); [ intuition |]. +exists a; intuition. +unfold eqb; destruct (eq_dec x a); auto. +rewrite <- H. +rewrite H0. +destruct H1 as (H1,_). +destruct H1 as (a,(Ha1,Ha2)); [intuition|]. +exists a; intuition. +unfold eqb in *; destruct (eq_dec x a); auto; discriminate. +Qed. + +Variable f : elt->bool. + +Lemma filter_b : Proper (E.eq==>Logic.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 : Proper (E.eq==>Logic.eq) f -> + for_all f s = forallb f (elements s). +Proof. +intros. +generalize (forallb_forall f (elements s))(for_all_iff s H)(elements_iff s). +unfold For_all. +destruct (forallb f (elements s)); destruct (for_all f s); auto; intros. +rewrite <- H1; intros. +destruct H0 as (H0,_). +rewrite (H2 x0) in H3. +rewrite (InA_alt E.eq x0 (elements s)) in H3. +destruct H3 as (a,(Ha1,Ha2)). +rewrite (H _ _ Ha1). +apply H0; auto. +symmetry. +rewrite H0; intros. +destruct H1 as (_,H1). +apply H1; auto. +rewrite H2. +rewrite InA_alt. exists x0; split; auto with relations. +Qed. + +Lemma exists_b : Proper (E.eq==>Logic.eq) f -> + exists_ f s = existsb f (elements s). +Proof. +intros. +generalize (existsb_exists f (elements s))(exists_iff s H)(elements_iff s). +unfold Exists. +destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros. +rewrite <- H1; intros. +destruct H0 as (H0,_). +destruct H0 as (a,(Ha1,Ha2)); auto. +exists a; split; auto. +rewrite H2; rewrite InA_alt; exists a; auto with relations. +symmetry. +rewrite H0. +destruct H1 as (_,H1). +destruct H1 as (a,(Ha1,Ha2)); auto. +rewrite (H2 a) in Ha1. +rewrite (InA_alt E.eq a (elements s)) in Ha1. +destruct Ha1 as (b,(Hb1,Hb2)). +exists b; auto. +rewrite <- (H _ _ Hb1); auto. +Qed. + +End BoolSpec. + +(** * Declarations of morphisms with respects to [E.eq] and [Equal] *) + +Instance In_m : Proper (E.eq==>Equal==>iff) In. +Proof. +unfold Equal; intros x y H s s' H0. +rewrite (In_eq_iff s H); auto. +Qed. + +Instance Empty_m : Proper (Equal==>iff) Empty. +Proof. +repeat red; unfold Empty; intros s s' E. +setoid_rewrite E; auto. +Qed. + +Instance is_empty_m : Proper (Equal==>Logic.eq) is_empty. +Proof. +intros s s' H. +generalize (is_empty_iff s). rewrite H at 1. rewrite is_empty_iff. +destruct (is_empty s); destruct (is_empty s'); intuition. +Qed. + +Instance mem_m : Proper (E.eq==>Equal==>Logic.eq) mem. +Proof. +intros x x' Hx s s' Hs. +generalize (mem_iff s x). rewrite Hs, Hx at 1; rewrite mem_iff. +destruct (mem x s), (mem x' s'); intuition. +Qed. + +Instance singleton_m : Proper (E.eq==>Equal) singleton. +Proof. +intros x y H a. rewrite !singleton_iff, H; intuition. +Qed. + +Instance add_m : Proper (E.eq==>Equal==>Equal) add. +Proof. +intros x x' Hx s s' Hs a. rewrite !add_iff, Hx, Hs; intuition. +Qed. + +Instance remove_m : Proper (E.eq==>Equal==>Equal) remove. +Proof. +intros x x' Hx s s' Hs a. rewrite !remove_iff, Hx, Hs; intuition. +Qed. + +Instance union_m : Proper (Equal==>Equal==>Equal) union. +Proof. +intros s1 s1' Hs1 s2 s2' Hs2 a. rewrite !union_iff, Hs1, Hs2; intuition. +Qed. + +Instance inter_m : Proper (Equal==>Equal==>Equal) inter. +Proof. +intros s1 s1' Hs1 s2 s2' Hs2 a. rewrite !inter_iff, Hs1, Hs2; intuition. +Qed. + +Instance diff_m : Proper (Equal==>Equal==>Equal) diff. +Proof. +intros s1 s1' Hs1 s2 s2' Hs2 a. rewrite !diff_iff, Hs1, Hs2; intuition. +Qed. + +Instance Subset_m : Proper (Equal==>Equal==>iff) Subset. +Proof. +unfold Equal, Subset; firstorder. +Qed. + +Instance subset_m : Proper (Equal==>Equal==>Logic.eq) subset. +Proof. +intros s1 s1' Hs1 s2 s2' Hs2. +generalize (subset_iff s1 s2). rewrite Hs1, Hs2 at 1. rewrite subset_iff. +destruct (subset s1 s2); destruct (subset s1' s2'); intuition. +Qed. + +Instance equal_m : Proper (Equal==>Equal==>Logic.eq) equal. +Proof. +intros s1 s1' Hs1 s2 s2' Hs2. +generalize (equal_iff s1 s2). rewrite Hs1,Hs2 at 1. rewrite equal_iff. +destruct (equal s1 s2); destruct (equal s1' s2'); intuition. +Qed. + +Instance SubsetSetoid : PreOrder Subset. (* reflexive + transitive *) +Proof. firstorder. Qed. + +Definition Subset_refl := @PreOrder_Reflexive _ _ SubsetSetoid. +Definition Subset_trans := @PreOrder_Transitive _ _ SubsetSetoid. + +Instance In_s_m : Morphisms.Proper (E.eq ==> Subset ++> impl) In | 1. +Proof. + simpl_relation. eauto with set. +Qed. + +Instance Empty_s_m : Proper (Subset-->impl) Empty. +Proof. firstorder. Qed. + +Instance add_s_m : Proper (E.eq==>Subset++>Subset) add. +Proof. +intros x x' Hx s s' Hs a. rewrite !add_iff, Hx; intuition. +Qed. + +Instance remove_s_m : Proper (E.eq==>Subset++>Subset) remove. +Proof. +intros x x' Hx s s' Hs a. rewrite !remove_iff, Hx; intuition. +Qed. + +Instance union_s_m : Proper (Subset++>Subset++>Subset) union. +Proof. +intros s1 s1' Hs1 s2 s2' Hs2 a. rewrite !union_iff, Hs1, Hs2; intuition. +Qed. + +Instance inter_s_m : Proper (Subset++>Subset++>Subset) inter. +Proof. +intros s1 s1' Hs1 s2 s2' Hs2 a. rewrite !inter_iff, Hs1, Hs2; intuition. +Qed. + +Instance diff_s_m : Proper (Subset++>Subset-->Subset) diff. +Proof. +intros s1 s1' Hs1 s2 s2' Hs2 a. rewrite !diff_iff, Hs1, Hs2; intuition. +Qed. + + +(* [fold], [filter], [for_all], [exists_] and [partition] requires + some knowledge on [f] in order to be known as morphisms. *) + +Generalizable Variables f. + +Instance filter_equal : forall `(Proper _ (E.eq==>Logic.eq) f), + Proper (Equal==>Equal) (filter f). +Proof. +intros f Hf s s' Hs a. rewrite !filter_iff, Hs by auto; intuition. +Qed. + +Instance filter_subset : forall `(Proper _ (E.eq==>Logic.eq) f), + Proper (Subset==>Subset) (filter f). +Proof. +intros f Hf s s' Hs a. rewrite !filter_iff, Hs by auto; intuition. +Qed. + +Lemma filter_ext : forall f f', Proper (E.eq==>Logic.eq) f -> (forall x, f x = f' x) -> + forall s s', s[=]s' -> filter f s [=] filter f' s'. +Proof. +intros f f' Hf Hff' s s' Hss' x. rewrite 2 filter_iff; auto. +rewrite Hff', Hss'; intuition. +red; red; intros; rewrite <- 2 Hff'; auto. +Qed. + +(* For [elements], [min_elt], [max_elt] and [choose], we would need setoid + structures on [list elt] and [option elt]. *) + +(* Later: +Add Morphism cardinal ; cardinal_m. +*) + +End WFactsOn. + +(** Now comes variants for self-contained weak sets and for full sets. + For these variants, only one argument is necessary. Thanks to + the subtyping [WS<=S], the [Facts] functor which is meant to be + used on modules [(M:S)] can simply be an alias of [WFacts]. *) + +Module WFacts (M:WSets) := WFactsOn M.E M. +Module Facts := WFacts. |