Nicer third spec of choose.

The old version is now a properties in FSetProperties.OrdProperties



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

6 files changed, 71 insertions, 114 deletions

diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index db2c94c2c6..5c701c0055 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1088,6 +1088,20 @@ Proof.
  exact min_elt_3.
 Qed.
 
+Lemma choose_3 : forall s s', bst s -> avl s -> bst s' -> avl s' -> 
+ forall x x', choose s = Some x -> choose s' = Some x' -> 
+  Equal s s' -> X.eq x x'.
+Proof.
+ unfold choose, Equal; intros s s' Hb Ha Hb' Ha' x x' Hx Hx' H.
+ assert (~X.lt x x').
+  apply min_elt_2 with s'; auto.
+  rewrite <-H; auto using min_elt_1.
+ assert (~X.lt x' x).
+  apply min_elt_2 with s; auto.
+  rewrite H; auto using min_elt_1.
+ destruct (X.compare x x'); intuition.
+Qed.
+
 
 
 (** * Concatenation
@@ -2332,37 +2346,6 @@ generalize (compare_Eq B1 B2);
  destruct compare; auto; discriminate.
 Qed.
 
-Lemma choose_equal: forall s s', bst s -> avl s -> bst s' -> avl s' -> 
-  Equal s s' -> 
-  match choose s, choose s' with  
-   | Some x, Some x' => X.eq x x'
-   | None, None => True
-   | _, _ => False
-  end.
-Proof.
- unfold choose; intros s s' Hb Ha Hb' Ha' H.
- generalize (@min_elt_1 s) (@min_elt_2 s) (@min_elt_3 s).
- generalize (@min_elt_1 s') (@min_elt_2 s') (@min_elt_3 s').
- destruct (min_elt s) as [x|]; destruct (min_elt s') as [x'|]; auto.
- 
- intros H1 H2 _ H1' H2' _.
- destruct (X.compare x x'); auto.
- assert (In x s) by auto.
- rewrite (H x) in H0.
- destruct (H2 x' x); auto.
- assert (In x' s') by auto.
- rewrite <- (H x') in H0.
- destruct (H2' x x'); auto.
-
- intros _ _ H3 H1' _ _.
- destruct (H3 (refl_equal _) x).
- rewrite <- (H x); auto.
-   
- intros H1 _ _ _ _ H3'.
- destruct (H3' (refl_equal _) x').
- rewrite (H x'); auto.
-Qed.
-
 End Raw.
 
 
@@ -2657,18 +2640,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. exact (@Raw.choose_1 s x). Qed.
  Lemma choose_2 : choose s = None -> Empty s.
  Proof. exact (@Raw.choose_2 s). Qed.
-
- Lemma  choose_equal: (equal s s')=true -> 
-     match choose s, choose s' with  
-      | Some x, Some x' => E.eq x x'
-      | None, None => True
-      | _, _ => False
-     end.
- Proof.
-  intros.
-  unfold choose.  
-  apply Raw.choose_equal; auto.
-  exact (equal_2 H).
+ Lemma choose_3 : choose s = Some x -> choose s' = Some y -> 
+  Equal s s' -> E.eq x y.
+ Proof. 
+  exact (@Raw.choose_3 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s') x y).
  Qed.
 
  Lemma eq_refl : eq s s. 
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 993475757b..0fb41931c4 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -294,23 +294,17 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
        | _, _                        => False
      end.
   Proof.
-    intros.
-    generalize (M.choose_equal (M.equal_1 H)); clear H; intros Heq.
-    generalize (choose_ok1 s) (choose_ok2 s) (choose_ok1 s') (choose_ok2 s').
-    destruct (choose s) as [(x,Hx)|Hx]; destruct (choose s') as [(x',Hx')|Hx']; auto.
- 
-   intros H _ H' _; generalize (H x) (H' x'); clear H H'; intros H H'.
-   destruct H as (_,H); rewrite H in Heq; simpl in Heq; [|exists Hx]; auto.
-   destruct H' as (_,H'); rewrite H' in Heq; simpl in Heq; [|exists Hx']; auto.
-   
-   intros H _ _ H'; generalize (H x); clear H; intros H.
-   destruct H as (_,H); rewrite H in Heq; simpl in Heq; [|exists Hx]; auto.
-   destruct H' as (_,H'); rewrite H' in Heq; simpl in Heq;[|exists Hx']; auto.
-
-   intros _ H H' _; generalize (H' x'); clear H'; intros H'.
-   destruct H as (_,H); rewrite H in Heq; simpl in Heq; [|exists Hx]; auto.
-   destruct H' as (_,H'); rewrite H' in Heq; simpl in Heq; [|exists Hx']; auto.
-  Qed. 
+   intros.
+   generalize (@M.choose_1 s)(@M.choose_2 s)
+              (@M.choose_1 s')(@M.choose_2 s')(@M.choose_3 s s')
+              (choose_ok1 s)(choose_ok2 s)(choose_ok1 s')(choose_ok2 s').
+   destruct (choose s) as [(x,Hx)|Hx]; destruct (choose s') as [(x',Hx')|Hx']; auto; intros.
+   apply H4; auto.
+   rewrite H5; exists Hx; auto.
+   rewrite H7; exists Hx'; auto.
+   apply Hx' with x; unfold Equal in H; rewrite <-H; auto.
+   apply Hx with x'; unfold Equal in H; rewrite H; auto.
+  Qed.
 
   Definition min_elt :
     forall s : t,
@@ -449,17 +443,13 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
     simple destruct s0; intros; discriminate H.
   Qed.
  
-  Lemma choose_equal: forall s s', (equal s s')=true -> 
-     match choose s, choose s' with  
-      | Some x, Some x' => E.eq x x'
-      | None, None => True
-      | _, _ => False
-     end.
+  Lemma choose_3 : forall s s' x x', 
+   choose s = Some x -> choose s' = Some x' -> Equal s s' -> E.eq x x'.
   Proof.
   unfold choose; intros.
-  generalize (M.choose_equal (equal_2 H)); clear H.
-  destruct (M.choose s) as [(x,Hx)|Hx]; destruct (M.choose s') as [(x',Hx')|Hx']; 
-   simpl; auto.
+  generalize (M.choose_equal H1); clear H1.
+  destruct (M.choose s) as [(?,?)|?]; destruct (M.choose s') as [(?,?)|?]; 
+   simpl; auto; congruence.
   Qed.
 
   Definition elements (s : t) : list elt := let (l, _) := elements s in l. 
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 2bf0c1cae4..8ee74649e6 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -497,8 +497,9 @@ End WFacts.
 (** Now comes a special version dedicated to full sets. For this 
     one, only one argument [(M:S)] is necessary. *)
 
-Module Facts (M:S).
+Module Facts (Import M:S).
   Module D:=OT_as_DT M.E.
   Include WFacts D M.
+
 End Facts.
 
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index c113a7d242..eb2a730868 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -338,12 +338,8 @@ Module Type Sfun (E : OrderedType).
   Parameter max_elt_3 : max_elt s = None -> Empty s.
 
   (** Additional specification of [choose] *)
-  Parameter choose_equal: (equal s s')=true -> 
-     match choose s, choose s' with  
-      | Some x, Some x' => E.eq x x'
-      | None, None => True
-      | _, _ => False
-     end.
+  Parameter choose_3 : choose s = Some x -> choose s' = Some y -> 
+    Equal s s' -> E.eq x y.
 
   End Spec.
 
@@ -507,7 +503,7 @@ Module Type Sdep.
 
   Parameter choose : forall s : t, {x : elt | In x s} + {Empty s}.
 
-  (** The [choose_equal] specification of [S] cannot be packed 
+  (** The [choose_3] specification of [S] cannot be packed 
         in the dependent version of [choose], so we leave it separate. *)
   Parameter choose_equal : forall s s', Equal s s' -> 
      match choose s, choose s' with 
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 322e970cfc..01060eccee 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -722,36 +722,18 @@ Module Raw (X: OrderedType).
 
   Definition choose_2 : forall s : t, choose s = None -> Empty s := min_elt_3.
 
-  Lemma choose_equal: forall s s', Sort s -> Sort s' -> (equal s s')=true -> 
-     match choose s, choose s' with  
-      | Some x, Some x' => X.eq x x'
-      | None, None => True
-      | _, _ => False
-     end.
+  Lemma choose_3: forall s s', Sort s -> Sort s' -> forall x x',
+   choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'.
   Proof.
-   unfold choose; intros s s' Hs Hs' H.
-   generalize (equal_2 H); clear H; intros.
-   generalize (@min_elt_1 s) (@min_elt_2 _ Hs) (@min_elt_3 s).
-   generalize (@min_elt_1 s') (@min_elt_2 _ Hs') (@min_elt_3 s').
-   destruct (min_elt s) as [x|]; destruct (min_elt s') as [x'|]; auto.
-   
-   intros H1 H2 _ H1' H2' _.
-   destruct (X.compare x x'); auto.
-   assert (In x s) by auto.
-   rewrite (H x) in H0.
-   destruct (H2 x' x); auto.
-   assert (In x' s') by auto.
-   rewrite <- (H x') in H0.
-   destruct (H2' x x'); auto.
-
-   intros _ _ H3 H1' _ _.
-   destruct (H3 (refl_equal _) x).
-   rewrite <- (H x); auto.
-   
-   intros H1 _ _ _ _ H3'.
-   destruct (H3' (refl_equal _) x').
-   rewrite (H x'); auto.
-  Qed.   
+   unfold choose, Equal; intros s s' Hs Hs' x x' Hx Hx' H.
+   assert (~X.lt x x').
+    apply min_elt_2 with s'; auto.
+    rewrite <-H; auto using min_elt_1.
+   assert (~X.lt x' x).
+    apply min_elt_2 with s; auto.
+    rewrite H; auto using min_elt_1.
+   destruct (X.compare x x'); intuition.
+  Qed.
    
   Lemma fold_1 :
    forall (s : t) (Hs : Sort s) (A : Type) (i : A) (f : elt -> A -> A),
@@ -1258,13 +1240,9 @@ Module Make (X: OrderedType) <: S with Module E := X.
   Proof. exact (fun H => Raw.choose_1 H). Qed.
   Lemma choose_2 : choose s = None -> Empty s.
   Proof. exact (fun H => Raw.choose_2 H). Qed.
-  Lemma choose_equal : (equal s s')=true -> 
-     match choose s, choose s' with  
-      | Some x, Some x' => E.eq x x'
-      | None, None => True
-      | _, _ => False
-     end. 
-  Proof. exact (Raw.choose_equal s.(sorted) s'.(sorted)). Qed.
+  Lemma choose_3 : choose s = Some x -> choose s' = Some y -> 
+   Equal s s' -> E.eq x y.
+  Proof. exact (@Raw.choose_3 _ _ s.(sorted) s'.(sorted) x y). Qed.
 
   Lemma eq_refl : eq s s.
   Proof. exact (Raw.eq_refl s). Qed.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 5525c3ecce..f9bce013c5 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -789,7 +789,7 @@ Module OrdProperties (M:S).
   Import M.E.
   Import M.
 
-  (* First, a specialized version of SortA_equivlistA_eqlistA: *)
+  (** First, a specialized version of SortA_equivlistA_eqlistA: *)
   Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
    sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
   Proof.
@@ -1042,4 +1042,21 @@ Module OrdProperties (M:S).
 
   End FoldOpt.
 
+  (** An alternative version of [choose_3] *)
+
+  Lemma choose_equal : forall s s', Equal s s' -> 
+    match choose s, choose s' with  
+      | Some x, Some x' => E.eq x x'
+      | None, None => True
+      | _, _ => False
+     end.
+  Proof.
+  intros s s' H; 
+  generalize (@choose_1 s)(@choose_2 s)
+             (@choose_1 s')(@choose_2 s')(@choose_3 s s'); 
+  destruct (choose s); destruct (choose s'); simpl; intuition.
+  apply H5 with e; rewrite <-H; auto.
+  apply H5 with e; rewrite H; auto.
+  Qed.
+
 End OrdProperties.