Making those proofs which depend on names generated for the arguments

in Prop of constructors of inductive types independent of these names.

Incidentally upgraded/simplified a couple of proofs, mainly in Reals.

This prepares to the next commit about using names based on H for such
hypotheses in Prop.

6 files changed, 38 insertions, 37 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index bee922c6f..7f5853494 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1270,10 +1270,10 @@ Proof.
 
  inv bst.
  rewrite H2, join_find; auto; clear H2.
- simpl; destruct X.compare; simpl; auto.
+ simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto.
  destruct (find y m2'); auto.
  symmetry; rewrite not_find_iff; auto; intro.
- apply (MX.lt_not_gt l); apply H1; auto; rewrite H3; auto.
+ apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto.
 
  intros z Hz; apply H1; auto; rewrite H3; auto.
 Qed.
@@ -1622,8 +1622,8 @@ Lemma map_option_find : forall (m:t elt)(x:key),
 Proof.
 intros m; functional induction (map_option f m); simpl; auto; intros;
  inv bst; rewrite join_find || rewrite concat_find; auto; simpl;
- try destruct X.compare; simpl; auto.
-rewrite (f_compat d e); auto.
+ try destruct X.compare as [Hlt|Heq|Hlt]; simpl; auto.
+rewrite (f_compat d Heq); auto.
 intros y H;
  destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In.
 intros y H;
@@ -1631,7 +1631,7 @@ intros y H;
 
 rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto.
 rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto.
-rewrite (f_compat d e); auto.
+rewrite (f_compat d Heq); auto.
 rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto.
  destruct (find x0 (map_option f r)); auto.
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 0e3b5cef1..083965cb7 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -702,18 +702,18 @@ Add Parametric Morphism elt : (@add elt)
  with signature E.eq ==> eq ==> Equal ==> Equal as add_m.
 Proof.
 intros k k' Hk e m m' Hm y.
-rewrite add_o, add_o; do 2 destruct eq_dec; auto.
-elim n; rewrite <-Hk; auto.
-elim n; rewrite Hk; auto.
+rewrite add_o, add_o; do 2 destruct eq_dec as [|?Hnot]; auto.
+elim Hnot; rewrite <-Hk; auto.
+elim Hnot; rewrite Hk; auto.
 Qed.
 
 Add Parametric Morphism elt : (@remove elt)
  with signature E.eq ==> Equal ==> Equal as remove_m.
 Proof.
 intros k k' Hk m m' Hm y.
-rewrite remove_o, remove_o; do 2 destruct eq_dec; auto.
-elim n; rewrite <-Hk; auto.
-elim n; rewrite Hk; auto.
+rewrite remove_o, remove_o; do 2 destruct eq_dec as [|?Hnot]; auto.
+elim Hnot; rewrite <-Hk; auto.
+elim Hnot; rewrite Hk; auto.
 Qed.
 
 Add Parametric Morphism elt elt' : (@map elt elt')
@@ -861,7 +861,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
   specialize (IH k Hnodup'); clear Hnodup'.
   rewrite add_o, IH.
-  unfold eqb; do 2 destruct eq_dec; auto; elim n; eauto.
+  unfold eqb; do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto.
   Qed.
 
   Lemma of_list_2 : forall l, NoDupA eqk l ->
@@ -928,7 +928,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
    apply InA_eqke_eqk with k e'; auto.
    rewrite <- of_list_1; auto.
    intro k'. rewrite Hsame, add_o, of_list_1b. simpl.
-   unfold eqb. do 2 destruct eq_dec; auto; elim n; eauto.
+   unfold eqb. do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto.
    inversion_clear Hdup; auto.
   apply IHl.
    intros; eapply Hstep'; eauto.
@@ -1890,7 +1890,7 @@ Module OrdProperties (M:S).
    find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
    add_mapsto_iff by (auto with *).
   unfold O.eqke; simpl. intuition.
-  destruct (E.eq_dec x t0); auto.
+  destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.
   exfalso.
   assert (In t0 m).
    exists e0; auto.
@@ -1919,7 +1919,7 @@ Module OrdProperties (M:S).
     find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
     add_mapsto_iff by (auto with *).
   unfold O.eqke; simpl. intuition.
-  destruct (E.eq_dec x t0); auto.
+  destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.
   exfalso.
   assert (In t0 m).
    exists e0; auto.
@@ -1975,7 +1975,7 @@ Module OrdProperties (M:S).
   inversion_clear H1; [ | inversion_clear H2; eauto ].
   red in H3; simpl in H3; destruct H3.
   destruct p as (p1,p2).
-  destruct (E.eq_dec p1 x).
+  destruct (E.eq_dec p1 x) as [Heq|Hneq].
   apply ME.lt_eq with p1; auto.
    inversion_clear H2.
    inversion_clear H5.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 64d5b1c9a..a6f9ae902 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -867,8 +867,8 @@ Proof.
  induction m'.
  (* m' = nil *)
  intros; destruct a; simpl.
- destruct (X.compare x t0); simpl; auto.
- inversion_clear Hm; clear H0 l Hm' IHm t0.
+ destruct (X.compare x t0) as [Hlt| |Hlt]; simpl; auto.
+ inversion_clear Hm; clear H0 Hlt Hm' IHm t0.
  induction m; simpl; auto.
  inversion_clear H.
  destruct a.
@@ -1244,16 +1244,16 @@ Lemma eq_refl : forall m : t, eq m m.
 Proof.
  intros (m,Hm); induction m; unfold eq; simpl; auto.
  destruct a.
- destruct (X.compare t0 t0); auto.
- apply (MapS.Raw.MX.lt_antirefl l); auto.
+ destruct (X.compare t0 t0) as [Hlt| |Hlt]; auto.
+ apply (MapS.Raw.MX.lt_antirefl Hlt); auto.
  split.
  apply D.eq_refl.
  inversion_clear Hm.
  apply (IHm H).
- apply (MapS.Raw.MX.lt_antirefl l); auto.
+ apply (MapS.Raw.MX.lt_antirefl Hlt); auto.
 Qed.
 
-Lemma  eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
+Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
 Proof.
  intros (m,Hm); induction m;
  intros (m', Hm'); destruct m'; unfold eq; simpl;
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 253800a45..a0ecdb756 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -1074,7 +1074,7 @@ Module PositiveMapAdditionalFacts.
     find i (add j x m) = if E.eq_dec i j then Some x else find i m.
   Proof.
     intros.
-    destruct (E.eq_dec i j); [ rewrite e; apply gss | apply gso; auto ].
+    destruct (E.eq_dec i j) as [ ->|]; [ apply gss | apply gso; auto ].
   Qed.
 
    (* Not derivable from the Map interface *)
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index e3f84723f..0f11dd7a5 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -146,9 +146,10 @@ Proof.
  induction m; simpl; auto; destruct a; intros.
  inversion_clear Hm.
  rewrite (IHm H1 x x'); auto.
- destruct (X.eq_dec x t0); destruct (X.eq_dec x' t0); trivial.
- elim n; apply X.eq_trans with x; auto.
- elim n; apply X.eq_trans with x'; auto.
+ destruct (X.eq_dec x t0) as [|Hneq]; destruct (X.eq_dec x' t0) as [|?Hneq'];
+   trivial.
+ elim Hneq'; apply X.eq_trans with x; auto.
+ elim Hneq; apply X.eq_trans with x'; auto.
 Qed.
 
 (** * [add] *)
@@ -787,14 +788,14 @@ Proof.
  destruct o; destruct o'; simpl in *; try discriminate; auto.
  destruct a as (k,(oo,oo')); simpl in *.
  inversion_clear H2.
- destruct (X.eq_dec x k); simpl in *.
+ destruct (X.eq_dec x k) as [|Hneq]; simpl in *.
  (* x = k *)
  assert (at_least_one_then_f o o' = f oo oo').
   destruct o; destruct o'; simpl in *; inversion_clear H; auto.
  rewrite H2.
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); try contradict n; auto.
+ destruct (X.eq_dec x k) as [|Hneq]; try contradict Hneq; auto.
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
  case_eq (find x m0); intros; auto.
  elim H0.
@@ -804,7 +805,7 @@ Proof.
  (* k < x *)
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); [ contradict n; auto | auto].
+ destruct (X.eq_dec x k); [ contradict Hneq; auto | auto].
  destruct (IHm0 H1) as (H3,_); apply H3; auto.
  destruct (IHm0 H1) as (H3,_); apply H3; auto.
 
@@ -812,13 +813,13 @@ Proof.
  destruct a as (k,(oo,oo')).
  simpl.
  inversion_clear H2.
- destruct (X.eq_dec x k).
+ destruct (X.eq_dec x k) as [|Hneq].
  (* x = k *)
  discriminate.
  (* k < x *)
  unfold f'; simpl.
  destruct (f oo oo'); simpl.
- destruct (X.eq_dec x k); [ contradict n; auto | auto].
+ destruct (X.eq_dec x k); [ contradict Hneq; auto | auto].
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
  destruct (IHm0 H1) as (_,H4); apply H4; auto.
 Qed.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 6aebcf501..97f140b39 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -673,24 +673,24 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
    forall (s : t) (x : elt) (f : elt -> bool),
    compat_bool E.eq f -> In x (filter f s) -> In x s.
   Proof.
-    intros s x f; unfold filter; case M.filter; intuition.
-    generalize (i (compat_P_aux H)); firstorder.
+    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.
+    generalize (Hiff (compat_P_aux H)); firstorder.
   Qed.
 
   Lemma filter_2 :
    forall (s : t) (x : elt) (f : elt -> bool),
    compat_bool E.eq f -> In x (filter f s) -> f x = true.
   Proof.
-    intros s x f; unfold filter; case M.filter; intuition.
-    generalize (i (compat_P_aux H)); firstorder.
+    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.
+    generalize (Hiff (compat_P_aux H)); firstorder.
   Qed.
 
   Lemma filter_3 :
    forall (s : t) (x : elt) (f : elt -> bool),
    compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
   Proof.
-    intros s x f; unfold filter; case M.filter; intuition.
-    generalize (i (compat_P_aux H)); firstorder.
+    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.
+    generalize (Hiff (compat_P_aux H)); firstorder.
   Qed.
 
   Definition for_all (f : elt -> bool) (s : t) : bool :=