Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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.
+