* For uniformity, FSetAVL uses Implicit Arguments (a bit)

* Some additionnal properties: 
  - two more induction principles on sets
  - some results about union, filter, etc
  - Subset is declared to be a Setoid Relation



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9882 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 215 insertions, 45 deletions

diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index f12a92e07c..a49887bf09 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -2576,6 +2576,9 @@ Qed.
 
 End Raw.
 
+Set Implicit Arguments. 
+Unset Strict Implicit.
+
 (** * Encapsulation
 
    Now, in order to really provide a functor implementing [S], we 
@@ -2602,21 +2605,21 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  
  Definition mem (x:elt)(s:t) : bool := Raw.mem x s.
 
- Definition empty : t := Bbst _ Raw.empty_bst Raw.empty_avl.
+ Definition empty : t := Bbst Raw.empty_bst Raw.empty_avl.
  Definition is_empty (s:t) : bool := Raw.is_empty s.
- Definition singleton (x:elt) : t := Bbst _ (Raw.singleton_bst x) (Raw.singleton_avl x).
+ Definition singleton (x:elt) : t := Bbst (Raw.singleton_bst x) (Raw.singleton_avl x).
  Definition add (x:elt)(s:t) : t := 
-   Bbst _ (Raw.add_bst s x (is_bst s) (is_avl s)) 
-          (Raw.add_avl s x (is_avl s)). 
+   Bbst (Raw.add_bst s x (is_bst s) (is_avl s)) 
+        (Raw.add_avl s x (is_avl s)). 
  Definition remove (x:elt)(s:t) : t := 
-   Bbst _ (Raw.remove_bst s x (is_bst s) (is_avl s)) 
-          (Raw.remove_avl s x (is_avl s)). 
+   Bbst (Raw.remove_bst s x (is_bst s) (is_avl s)) 
+        (Raw.remove_avl s x (is_avl s)). 
  Definition inter (s s':t) : t := 
-   Bbst _ (Raw.inter_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'))  
-          (Raw.inter_avl _ _ (is_avl s) (is_avl s')).
+   Bbst (Raw.inter_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'))  
+        (Raw.inter_avl _ _ (is_avl s) (is_avl s')).
  Definition diff (s s':t) : t := 
-   Bbst _ (Raw.diff_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'))  
-          (Raw.diff_avl _ _ (is_avl s) (is_avl s')).
+   Bbst (Raw.diff_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'))  
+        (Raw.diff_avl _ _ (is_avl s) (is_avl s')).
  Definition elements (s:t) : list elt := Raw.elements s.
  Definition min_elt (s:t) : option elt := Raw.min_elt s.
  Definition max_elt (s:t) : option elt := Raw.max_elt s.
@@ -2624,26 +2627,26 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s. 
  Definition cardinal (s:t) : nat := Raw.cardinal s.
  Definition filter (f : elt -> bool) (s:t) : t := 
-   Bbst _ (Raw.filter_bst f _ (is_bst s) (is_avl s))
-          (Raw.filter_avl f _ (is_avl s)). 
+   Bbst (Raw.filter_bst f _ (is_bst s) (is_avl s))
+        (Raw.filter_avl f _ (is_avl s)). 
  Definition for_all (f : elt -> bool) (s:t) : bool := Raw.for_all f s.
  Definition exists_ (f : elt -> bool) (s:t) : bool := Raw.exists_ f s.
  Definition partition (f : elt -> bool) (s:t) : t * t :=
    let p := Raw.partition f s in
-   (Bbst (fst p) (Raw.partition_bst_1 f _ (is_bst s) (is_avl s)) 
-                 (Raw.partition_avl_1 f _ (is_avl s)),
-    Bbst (snd p) (Raw.partition_bst_2 f _ (is_bst s) (is_avl s)) 
-                 (Raw.partition_avl_2 f _ (is_avl s))).
+   (Bbst (Raw.partition_bst_1 f _ (is_bst s) (is_avl s)) 
+         (Raw.partition_avl_1 f _ (is_avl s)),
+    Bbst (Raw.partition_bst_2 f _ (is_bst s) (is_avl s)) 
+         (Raw.partition_avl_2 f _ (is_avl s))).
 
  Definition union (s s':t) : t :=
    let (u,p) := Raw.union _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s') in 
    let (b,p) := p in 
    let (a,_) := p in 
-   Bbst u b a.
+   Bbst b a.
 
  Definition union' (s s' : t) : t := 
-   Bbst _ (Raw.union'_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'))  
-          (Raw.union'_avl _ _ (is_avl s) (is_avl s')).
+   Bbst (Raw.union'_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'))  
+        (Raw.union'_avl _ _ (is_avl s) (is_avl s')).
 
  Definition equal (s s': t) : bool := if Raw.equal _ _ (is_bst s) (is_bst s') then true else false. 
  Definition equal' (s s':t) : bool := Raw.equal' s s'.
@@ -2817,7 +2820,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Qed.
  
  Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
-      fold A f s i = fold_left (fun a e => f e a) (elements s) i.
+      fold f s i = fold_left (fun a e => f e a) (elements s) i.
  Proof. 
  unfold fold, elements; intros; apply Raw.fold_1; auto.
  Qed.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 4645a6bbc6..a970c092dc 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -665,6 +665,23 @@ Proof.
 auto.
 Qed.
 
+Lemma filter_add_1 : forall s x, f x = true -> 
+ filter f (add x s) [=] add x (filter f s). 
+Proof.
+red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
+intuition.
+rewrite <- H; apply Comp; auto.
+Qed.
+
+Lemma filter_add_2 : forall s x, f x = false -> 
+ filter f (add x s) [=] filter f s. 
+Proof.
+red; intros; do 2 (rewrite filter_iff; auto); set_iff.
+intuition.
+assert (f x = f a) by (apply Comp; auto).
+rewrite H in H1; rewrite H2 in H1; discriminate.
+Qed.
+
 Lemma add_filter_1 : forall s s' x, 
  f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
 Proof.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 6874ceb33e..4c1c51c497 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -287,19 +287,17 @@ End BoolSpec.
 
 (** * [E.eq] and [Equal] are setoid equalities *)
 
-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.
-Proof. 
-constructor; [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.
@@ -396,6 +394,65 @@ 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. Qed.
+
+Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''.
+Proof. unfold Subset; eauto. Qed.
+
+Add Relation t Subset 
+ reflexivity proved by Subset_refl
+ transitivity proved by Subset_trans
+ as SubsetSetoid.
+
+Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m.
+Proof.
+unfold Subset, impl; intros; eauto.
+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.
+
+Add Morphism Subset with signature Subset --> Subset ++> impl as  Subset_s_m.
+Proof.
+unfold Subset, impl; auto.
+Qed.
+
 (* [fold], [filter], [for_all], [exists_] and [partition] cannot be proved morphism
    without additional hypothesis on [f]. For instance: *)
 
@@ -405,6 +462,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 +475,5 @@ Qed.
 Add Morphism cardinal ; cardinal_m.
 *)
 
+
 End Facts.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 7b25e8d61d..3b8d0d708a 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -51,21 +51,21 @@ Module Properties (M: S).
 
   Lemma equal_refl : forall s, s[=]s.
   Proof.
-  unfold Equal; intuition.
+  exact eq_refl.
   Qed.
 
   Lemma equal_sym : forall s s', s[=]s' -> s'[=]s.
   Proof.
-  unfold Equal; intros.
-  rewrite H; intuition.
+  exact eq_sym.
   Qed.
 
   Lemma equal_trans : forall s1 s2 s3, s1[=]s2 -> s2[=]s3 -> s1[=]s3.
   Proof.
-  unfold Equal; intros.
-  rewrite H; exact (H0 a).
+  exact eq_trans.
   Qed.
 
+  Hint Immediate equal_refl equal_sym : set.
+
   Variable s s' s'' s1 s2 s3 : t.
   Variable x x' : elt.
 
@@ -73,22 +73,24 @@ Module Properties (M: S).
   
   Lemma subset_refl : s[<=]s. 
   Proof.
-  unfold Subset; intuition.
+  apply Subset_refl.
   Qed.
 
-  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
+  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
   Proof.
-  unfold Subset, Equal; intuition.
+  apply Subset_trans.
   Qed.
 
-  Lemma subset_trans : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3.
+  Lemma subset_antisym : s[<=]s' -> s'[<=]s -> s[=]s'.
   Proof.
-  unfold Subset; intuition.
+  unfold Subset, Equal; intuition.
   Qed.
 
+  Hint Immediate subset_refl : set.
+
   Lemma subset_equal : s[=]s' -> s[<=]s'.
   Proof.
-  unfold Subset, Equal; firstorder.
+  unfold Subset, Equal; intros; rewrite <- H; auto.
   Qed.
 
   Lemma subset_empty : empty[<=]s.
@@ -119,7 +121,7 @@ Module Properties (M: S).
 
   Lemma in_subset : In x s1 -> s1[<=]s2 -> In x s2.
   Proof.
-  unfold Subset; intuition.
+  intros; rewrite <- H0; auto.
   Qed.
  
   Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
@@ -223,6 +225,21 @@ Module Properties (M: S).
   unfold Equal; intros; set_iff; tauto.
   Qed.
 
+  Lemma union_remove_add_1 : 
+   union (remove x s) (add x s') [=] union (add x s) (remove x s').
+  Proof.
+  unfold Equal; intros; set_iff.
+  destruct (ME.eq_dec x a); intuition.
+  Qed.
+
+  Lemma union_remove_add_2 : In x s -> 
+   union (remove x s) (add x s') [=] union s s'.
+  Proof.
+  unfold Equal; intros; set_iff.
+  destruct (ME.eq_dec x a); intuition.
+  left; eauto.
+  Qed.
+
   Lemma union_subset_1 : s [<=] union s s'.
   Proof.
   unfold Subset; intuition.
@@ -892,4 +909,73 @@ Module Properties (M: S).
 
   Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
 
+  (** Two other induction principles on sets: we can be more restrictive 
+      on the element we add at each step.  *)
+
+  Definition Above x s := forall y, In y s -> E.lt y x.
+  Definition Below x s := forall y, In y s -> E.lt x y.
+
+  Lemma set_induction_max :
+   forall P : t -> Type,
+   (forall s : t, Empty s -> P s) ->
+   (forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') ->
+   forall s : t, P s.
+  Proof.
+  intros.
+  remember (cardinal s) as n; revert s Heqn; induction n.
+  intros.
+  apply X.
+  apply cardinal_inv_1; auto.
+
+  intros.
+  case_eq (max_elt s); intros.
+  apply X0 with (remove e s) e.
+  apply IHn.
+  assert (S (cardinal (remove e s)) = S n).
+   rewrite Heqn.
+   apply remove_cardinal_1; auto.
+  inversion H0; auto.
+  red; intros.
+  rewrite remove_iff in H0; destruct H0.
+  generalize (@max_elt_2 s e y H H0).
+  intros.
+  destruct (E.compare y e); intuition.
+  elim H1; auto.
+  apply Add_remove; auto.
+
+  rewrite (cardinal_1 (max_elt_3 H)) in Heqn; inversion Heqn.
+  Qed.  
+
+  Lemma set_induction_min :
+   forall P : t -> Type,
+   (forall s : t, Empty s -> P s) ->
+   (forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') ->
+   forall s : t, P s.
+  Proof.
+  intros.
+  remember (cardinal s) as n; revert s Heqn; induction n.
+  intros.
+  apply X.
+  apply cardinal_inv_1; auto.
+
+  intros.
+  case_eq (min_elt s); intros.
+  apply X0 with (remove e s) e.
+  apply IHn.
+  assert (S (cardinal (remove e s)) = S n).
+   rewrite Heqn.
+   apply remove_cardinal_1; auto.
+  inversion H0; auto.
+  red; intros.
+  rewrite remove_iff in H0; destruct H0.
+  generalize (@min_elt_2 s e y H H0).
+  intros.
+  destruct (E.compare y e); intuition.
+  elim H1; auto.
+  apply Add_remove; auto.
+
+  rewrite (cardinal_1 (min_elt_3 H)) in Heqn; inversion Heqn.
+  Qed.  
+
+
 End Properties.