* 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

1 files changed, 98 insertions, 12 deletions

diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 7b25e8d61..3b8d0d708 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.