diff options
Diffstat (limited to 'theories/FSets/FSetFacts.v')
| -rw-r--r-- | theories/FSets/FSetFacts.v | 120 |
1 files changed, 105 insertions, 15 deletions
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index aa57f066..b4b834b1 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetFacts.v 8882 2006-05-31 21:55:30Z letouzey $ *) +(* $Id: FSetFacts.v 10765 2008-04-08 16:15:23Z msozeau $ *) (** * Finite sets library *) @@ -16,16 +16,19 @@ Moreover, we prove that [E.Eq] and [Equal] are setoid equalities. *) +Require Import DecidableTypeEx. Require Export FSetInterface. Set Implicit Arguments. Unset Strict Implicit. -Module Facts (M: S). -Module ME := OrderedTypeFacts M.E. -Import ME. -Import M. -Import Logic. (* to unmask [eq] *) -Import Peano. (* to unmask [lt] *) +(** First, a functor for Weak Sets. Since the signature [WS] includes + an EqualityType and not a stronger DecidableType, this functor + should take two arguments in order to compensate this. *) + +Module WFacts (Import E : DecidableType)(Import M : WSfun E). + +Notation eq_dec := E.eq_dec. +Definition eqb x y := if eq_dec x y then true else false. (** * Specifications written using equivalences *) @@ -259,6 +262,8 @@ symmetry. rewrite H0; intros. destruct H1 as (_,H1). apply H1; auto. +rewrite H2. +rewrite InA_alt; eauto. Qed. Lemma exists_b : compat_bool E.eq f -> @@ -271,7 +276,8 @@ 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; auto. +exists a; split; auto. +rewrite H2; rewrite InA_alt; eauto. symmetry. rewrite H0. destruct H1 as (_,H1). @@ -289,17 +295,25 @@ End BoolSpec. Definition E_ST : Setoid_Theory elt E.eq. Proof. -constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans]. +constructor ; red; [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. Proof. -constructor; [apply eq_refl | apply eq_sym | apply eq_trans]. +constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans]. Qed. -Add Setoid t Equal Equal_ST as EqualSetoid. +Add Relation elt E.eq + reflexivity proved by E.eq_refl + symmetry proved by E.eq_sym + transitivity proved by E.eq_trans + as EltSetoid. + +Add Relation t Equal + reflexivity proved by eq_refl + symmetry proved by eq_sym + transitivity proved by eq_trans + as EqualSetoid. Add Morphism In with signature E.eq ==> Equal ==> iff as In_m. Proof. @@ -325,7 +339,7 @@ exact (H1 (refl_equal true) _ Ha). Qed. Add Morphism Empty with signature Equal ==> iff as Empty_m. -Proof. +Proof. intros; do 2 rewrite is_empty_iff; rewrite H; intuition. Qed. @@ -340,7 +354,9 @@ Qed. Add Morphism singleton : singleton_m. Proof. unfold Equal; intros x y H a. -do 2 rewrite singleton_iff; split; order. +do 2 rewrite singleton_iff; split; intros. +apply E.eq_trans with x; auto. +apply E.eq_trans with y; auto. Qed. Add Morphism add : add_m. @@ -396,6 +412,63 @@ rewrite H in H1; rewrite H0 in H1; intuition. rewrite H in H1; rewrite H0 in H1; intuition. Qed. + +(* [Subset] is a setoid order *) + +Lemma Subset_refl : forall s, s[<=]s. +Proof. red; auto. Defined. + +Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''. +Proof. unfold Subset; eauto. Defined. + +Add Relation t Subset + reflexivity proved by Subset_refl + transitivity proved by Subset_trans + as SubsetSetoid. +(* NB: for the moment, it is important to use Defined and not Qed in + the two previous lemmas, in order to allow conversion of + SubsetSetoid coming from separate Facts modules. See bug #1738. *) + +Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1. +Proof. + simpl_relation. eauto with set. +Qed. + +Add Morphism Empty with signature Subset --> impl as Empty_s_m. +Proof. +unfold Subset, Empty, impl; firstorder. +Qed. + +Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m. +Proof. +unfold Subset; intros x y H s s' H0 a. +do 2 rewrite add_iff; rewrite H; intuition. +Qed. + +Add Morphism remove with signature E.eq ==> Subset ++> Subset as remove_s_m. +Proof. +unfold Subset; intros x y H s s' H0 a. +do 2 rewrite remove_iff; rewrite H; intuition. +Qed. + +Add Morphism union with signature Subset ++> Subset ++> Subset as union_s_m. +Proof. +unfold Equal; intros s s' H s'' s''' H0 a. +do 2 rewrite union_iff; intuition. +Qed. + +Add Morphism inter with signature Subset ++> Subset ++> Subset as inter_s_m. +Proof. +unfold Equal; intros s s' H s'' s''' H0 a. +do 2 rewrite inter_iff; intuition. +Qed. + +Add Morphism diff with signature Subset ++> Subset --> Subset as diff_s_m. +Proof. +unfold Subset; intros s s' H s'' s''' H0 a. +do 2 rewrite diff_iff; intuition. +Qed. + (* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism without additional hypothesis on [f]. For instance: *) @@ -405,6 +478,12 @@ Proof. unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto. Qed. +Lemma filter_subset : forall f, compat_bool E.eq f -> + forall s s', s[<=]s' -> filter f s [<=] filter f s'. +Proof. +unfold Subset; intros; rewrite filter_iff in *; intuition. +Qed. + (* For [elements], [min_elt], [max_elt] and [choose], we would need setoid structures on [list elt] and [option elt]. *) @@ -412,4 +491,15 @@ Qed. Add Morphism cardinal ; cardinal_m. *) +End WFacts. + + +(** Now comes a special version dedicated to full sets. For this + one, only one argument [(M:S)] is necessary. *) + +Module Facts (Import M:S). + Module D:=OT_as_DT M.E. + Include WFacts D M. + End Facts. + |