+ ameliorating the tactic "functional induction"

+ bug correction in proof of structural principles
+ up do to date test-suite/success/Funind.v


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

4 files changed, 86 insertions, 86 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index af5cee4fa..a94f40637 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -512,7 +512,7 @@ Proof.
  (* LT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt H2); intuition_in.
+ rewrite (IHt H1); intuition_in.
  (* EQ *)  
  inv avl.
  firstorder_in.
@@ -520,7 +520,7 @@ Proof.
  (* GT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt H3); intuition_in.
+ rewrite (IHt H2); intuition_in.
 Qed.
 
 Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m).
@@ -528,15 +528,15 @@ Proof.
  intros elt m x e; functional induction (add x e m); 
    intros; inv bst; inv avl; auto; apply bal_bst; auto.
  (* lt_tree -> lt_tree (add ...) *)
- red; red in H5.
+ red; red in H4.
  intros.
- rewrite (add_in x y0 e H1) in H2.
+ rewrite (add_in x y0 e H) in H1.
  intuition.
  eauto.
  (* gt_tree -> gt_tree (add ...) *)
  red; red in H5.
  intros.
- rewrite (add_in x y0 e H7) in H2.
+ rewrite (add_in x y0 e H6) in H1.
  intuition.
  apply lt_eq with x; auto.
 Qed.
@@ -588,7 +588,7 @@ Proof.
  inv avl; simpl in *; split; auto.
  avl_nns; omega_max.
  (* l = Node *)
- inversion_clear H1.
+ inversion_clear H.
  destruct (IHp lh); auto.
  split; simpl in *. 
  rewrite_all H0. simpl in *.
@@ -609,14 +609,14 @@ Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in.
  (* l = Node *)
- inversion_clear H1.
- generalize (remove_min_avl H2).
+ inversion_clear H.
+ generalize (remove_min_avl H1).
  
  rewrite_all H0; simpl; intros.
  rewrite bal_in; auto.
- generalize (IHp lh y H2).
+ generalize (IHp lh y H1).
  intuition.
- inversion_clear H9; intuition.
+ inversion_clear H8; intuition.
 Qed.
 
 Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> 
@@ -627,15 +627,15 @@ Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in; subst; auto.
  (* l = Node *)
- inversion_clear H1.
- generalize (remove_min_avl H2).
+ inversion_clear H.
+ generalize (remove_min_avl H1).
  rewrite_all H0; simpl; intros.
  rewrite bal_mapsto; auto; unfold create.
  simpl in *;destruct (IHp lh y e').
  auto.
  intuition.
- inversion_clear H4; intuition.
- inversion_clear H11; intuition.
+ inversion_clear H3; intuition.
+ inversion_clear H10; intuition.
 Qed.
 
 Lemma remove_min_bst : forall elt (l:t elt) x e r h, 
@@ -643,14 +643,14 @@ Lemma remove_min_bst : forall elt (l:t elt) x e r h,
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H1; inversion_clear H2.
+ inversion_clear H; inversion_clear H1.
  apply bal_bst; auto.
  rewrite_all H0;simpl in *;firstorder.
  intro; intros.
- generalize (remove_min_in y H1).
+ generalize (remove_min_in y H).
  rewrite_all H0; simpl in *.
  destruct 1.
- apply H5; intuition.
+ apply H4; intuition.
 Qed.
 
 Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, 
@@ -659,15 +659,15 @@ Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h,
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H1; inversion_clear H2.
+ inversion_clear H; inversion_clear H1.
  intro; intro.
  rewrite_all H0;simpl in *.
- generalize (IHp lh H3 H1); clear H9 H8 IHp.
- generalize (remove_min_avl H1).
- generalize (remove_min_in (fst m) H1).
+ generalize (IHp lh H2 H); clear H7 H8 IHp.
+ generalize (remove_min_avl H).
+ generalize (remove_min_in (fst m) H).
  rewrite H0; simpl; intros.
- rewrite (bal_in x e y H9 H7) in H2.
- destruct H8.
+ rewrite (bal_in x e y H8 H6) in H1.
+ destruct H7.
  firstorder.
  apply lt_eq with x; auto.
  apply X.lt_trans with x; auto.
@@ -694,13 +694,13 @@ Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 ->
  avl (merge s1 s2) /\ 
  0<= height (merge s1 s2) - max (height s1) (height s2) <=1.
 Proof.
- intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros;subst.
+ intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros.
  split; auto; avl_nns; omega_max.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  split; auto; avl_nns; simpl in *; omega_max.
- destruct _x;try contradiction;clear H1.
- generalize (remove_min_avl_1 H4).
-rewrite H2; simpl;destruct 1.
+ destruct s1;try contradiction;clear H1.
+ generalize (remove_min_avl_1 H0).
+ rewrite H2; simpl;destruct 1.
  split.
  apply bal_avl; auto.
  simpl; omega_max.
@@ -716,10 +716,10 @@ Qed.
 Lemma merge_in : forall elt (s1 s2:t elt) y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
  (In y (merge s1 s2) <-> In y s1 \/ In y s2).
 Proof. 
- intros elt s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
+ intros elt s1 s2; functional induction (merge s1 s2);intros.
  intuition_in.
  intuition_in.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
 (*  rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *)
  replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto].
  rewrite bal_in; auto.
@@ -731,10 +731,10 @@ Qed.
 Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
   (MapsTo y e (merge s1 s2) <-> MapsTo y e s1 \/ MapsTo y e s2).
 Proof.
- intros elt s1 s2; functional induction (@merge elt s1 s2); subst; simpl in *; intros.
+ intros elt s1 s2; functional induction (@merge elt s1 s2); intros.
  intuition_in.
  intuition_in.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto].
  rewrite bal_mapsto; auto; unfold create.
  generalize (remove_min_avl H4); rewrite H2; simpl; auto.
@@ -747,16 +747,16 @@ Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2
  (forall y1 y2 : key, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  bst (merge s1 s2). 
 Proof.
- intros elt s1 s2; functional induction (@merge elt s1 s2); subst;simpl in *; intros; auto.
+ intros elt s1 s2; functional induction (@merge elt s1 s2); intros; auto.
 
  apply bal_bst; auto.
- destruct _x;try contradiction.
+ destruct s1;try contradiction.
  generalize (remove_min_bst H3); rewrite H2; simpl in *; auto.
- destruct _x;try contradiction.
+ destruct s1;try contradiction.
  intro; intro.
  apply H5; auto.
  generalize (remove_min_in x H4); rewrite H2; simpl; intuition.
- destruct _x;try contradiction.
+ destruct s1;try contradiction.
  generalize (remove_min_gt_tree H3); rewrite H2; simpl; auto.
 Qed. 
 
@@ -775,7 +775,7 @@ Function remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with
 Lemma remove_avl_1 : forall elt (s:t elt) x, avl s -> 
  avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
 Proof.
- intros elt s x; functional induction (@remove elt x s); subst;simpl; intros.
+ intros elt s x; functional induction (@remove elt x s); intros.
  split; auto; omega_max.
  (* LT *)
  inv avl.
@@ -811,20 +811,20 @@ Proof.
  (* LT *)
  inv avl; inv bst; clear H0.
  rewrite bal_in; auto.
- generalize (IHt y0 H2); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H1); intuition; [ order | order | intuition_in ].
  (* EQ *)
  inv avl; inv bst; clear H0.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
- elim H10; eauto.
+ elim H9; eauto.
  (* GT *)
  inv avl; inv bst; clear H0.
  rewrite bal_in; auto.
- generalize (IHt y0 H7); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H6); intuition; [ order | order | intuition_in ].
 Qed.
 
 Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s).
 Proof. 
- intros elt s x; functional induction (@remove elt x s); subst;simpl; intros.
+ intros elt s x; functional induction (@remove elt x s); simpl; intros.
  auto.
  (* LT *)
  inv avl; inv bst.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 128ed45d2..5564b174b 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -112,7 +112,7 @@ Proof.
  intros m Hm x; generalize Hm; clear Hm.      
  functional induction (mem x m);intros sorted belong1;trivial.
  
- inversion belong1. inversion H0.
+ inversion belong1. inversion H.
  
  absurd (In x ((k', _x) :: l));try assumption.
  apply Sort_Inf_NotIn with _x;auto.
@@ -200,7 +200,7 @@ Proof.
  functional induction (add x e' m) ;simpl;auto;  clear H0.
  subst;auto.
 
- intros y' e'' eqky';  inversion_clear 1; destruct H1; simpl in *.
+ intros y' e'' eqky';  inversion_clear 1;  destruct H0; simpl in *.
  order.
  auto.
  auto.
@@ -213,10 +213,10 @@ Lemma add_3 : forall m x y e e',
 Proof.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl; intros.
+ apply (In_inv_3 H0); compute; auto.
  apply (In_inv_3 H1); compute; auto.
- subst s;apply (In_inv_3 H2); compute; auto.
- constructor 2; apply (In_inv_3 H2); compute; auto. 
- inversion_clear H2; auto.
+ constructor 2; apply (In_inv_3 H1); compute; auto. 
+ inversion_clear H1; auto.
 Qed.
 
 
@@ -441,8 +441,8 @@ Proof.
   apply Inf_lt with (x,e); auto.
  elim (Sort_Inf_NotIn H5 H7 H4).
 
- destruct _x;
- destruct _x0;try contradiction.
+ destruct m;
+ destruct m';try contradiction.
  
  clear H1;destruct p as (k,e).
  destruct (H0 k).
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 415e0c113..53485a67c 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -101,12 +101,12 @@ Lemma mem_1 : forall m (Hm:NoDupA m) x, In x m -> mem x m = true.
 Proof.
  intros m Hm x; generalize Hm; clear Hm.      
  functional induction (mem x m);intros NoDup belong1;trivial.
- inversion belong1. inversion H0.
+ inversion belong1. inversion H.
  inversion_clear NoDup.
  inversion_clear belong1.
- inversion_clear H3.
- compute in H4; destruct H4.
- elim H; auto.
+ inversion_clear H2.
+ compute in H3; destruct H3.
+ contradiction.
  apply IHb; auto.
  exists x0; auto.
 Qed. 
@@ -184,7 +184,7 @@ Proof.
  intros m x  y e e'; generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl;auto.
  intros y' e'' eqky';  inversion_clear 1.
- destruct H2; simpl in *.
+ destruct H1; simpl in *.
  elim eqky'; apply X.eq_trans with k'; auto.
  auto.
  intros y' e'' eqky'; inversion_clear 1; intuition.
@@ -195,8 +195,8 @@ Lemma add_3 : forall m x y e e',
 Proof.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl;auto.
- intros; apply (In_inv_3 H1); auto.
- constructor 2; apply (In_inv_3 H2); auto.
+ intros; apply (In_inv_3 H0); auto.
+ constructor 2; apply (In_inv_3 H1); auto.
  inversion_clear 2; auto.
 Qed.
 
@@ -206,10 +206,10 @@ Proof.
  intros m x y e e'. generalize y e; clear y e.
  functional induction (add x e' m);simpl;auto.
  inversion_clear 2.
- compute in H2; elim H0; auto.
- inversion H2. 
- constructor 2; inversion_clear H2; auto.
- compute in H3; elim H1; auto.
+ compute in H1; elim H; auto.
+ inversion H1. 
+ constructor 2; inversion_clear H1; auto.
+ compute in H2; elim H; auto.
  inversion_clear 2; auto.
 Qed.
 
@@ -268,21 +268,21 @@ Proof.
  intros m Hm x y; generalize Hm; clear Hm.
  functional induction (remove x m);simpl;intros;auto.
 
- red; inversion 1; inversion H2.
+ red; inversion 1; inversion H1.
 
  inversion_clear Hm.
  subst.
- swap H2.
- destruct H as (e,H); unfold PX.MapsTo in H.
+ swap H1.
+ destruct H3 as (e,H3); unfold PX.MapsTo in H3.
  apply InA_eqk with (y,e); auto.
  compute; apply X.eq_trans with x; auto.
   
  intro H2.
  destruct H2 as (e,H2); inversion_clear H2.
- compute in H3; destruct H3.
+ compute in H1; destruct H1.
  elim _x; apply X.eq_trans with y; auto.
  inversion_clear Hm.
- elim (IHt0 H4 H1).
+ elim (IHt0 H3 H).
  exists e; auto.
 Qed.
   
@@ -292,8 +292,8 @@ Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
  functional induction (remove x m);auto.
  inversion_clear 3; auto.
- compute in H3; destruct H3.
- elim H1; apply X.eq_trans with k'; auto.
+ compute in H2; destruct H2.
+ elim H; apply X.eq_trans with k'; auto.
   
  inversion_clear 1; inversion_clear 2; auto.
 Qed.
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 5b912f8b2..425cfdfac 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -515,7 +515,7 @@ Proof.
  (* LT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt y0 H2); intuition_in.
+ rewrite (IHt y0 H1); intuition_in.
  (* EQ *)  
  inv avl.
  intuition.
@@ -523,7 +523,7 @@ Proof.
  (* GT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt y0 H3); intuition_in.
+ rewrite (IHt y0 H2); intuition_in.
 Qed.
 
 Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s).
@@ -533,14 +533,14 @@ Proof.
  (* lt_tree -> lt_tree (add ...) *)
  red; red in H5.
  intros.
- rewrite (add_in l x y0 H1) in H2.
+ rewrite (add_in l x y0 H) in H1.
  intuition.
  eauto.
  inv bst; inv avl; apply bal_bst; auto.
  (* gt_tree -> gt_tree (add ...) *)
  red; red in H5.
  intros.
- rewrite (add_in r x y0 H7) in H2.
+ rewrite (add_in r x y0 H6) in H1.
  intuition.
  apply MX.lt_eq with x; auto.
 Qed.
@@ -722,13 +722,13 @@ Proof.
  intros l x r; functional induction (remove_min l x r); simpl in *; intros.
  intuition_in.
  (* l = Node *)
- inversion_clear H1.
- generalize (remove_min_avl ll lx lr lh H2).
+ inversion_clear H.
+ generalize (remove_min_avl ll lx lr lh H1).
  rewrite H0; simpl; intros.
  rewrite bal_in; auto.
- rewrite H0 in IHp;generalize (IHp lh y H2).
+ rewrite H0 in IHp;generalize (IHp lh y H1).
  intuition.
- inversion_clear H9; intuition.
+ inversion_clear H8; intuition.
 Qed.
 
 Lemma remove_min_bst : forall l x r h, 
@@ -788,7 +788,7 @@ Proof.
  intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
  split; auto; avl_nns; omega_max.
  split; auto; avl_nns; simpl in *; omega_max.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  generalize (remove_min_avl_1 l2 x2 r2 h2 H0).
  rewrite H2; simpl; destruct 1.
  split.
@@ -809,7 +809,7 @@ Proof.
  intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros.
  intuition_in.
  intuition_in.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H2; auto].
  rewrite bal_in; auto.
  generalize (remove_min_avl l2 x2 r2 h2); rewrite H2; simpl; auto.
@@ -822,7 +822,7 @@ Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 ->
  bst (merge s1 s2). 
 Proof.
  intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  apply bal_bst; auto.
  generalize (remove_min_bst l2 x2 r2 h2); rewrite H2; simpl in *; auto.
  intro; intro.
@@ -901,8 +901,8 @@ Proof.
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in l x y0) in H1; auto.
- destruct H1; eauto.
+ rewrite (remove_in l x y0) in H; auto.
+ destruct H; eauto.
  (* EQ *)
  inv avl; inv bst.
  apply merge_bst; eauto.
@@ -910,8 +910,8 @@ Proof.
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in r x y0) in H1; auto.
- destruct H1; eauto.
+ rewrite (remove_in r x y0) in H; auto.
+ destruct H; eauto.
 Qed.
 
  (** * Minimum element *)
@@ -1038,7 +1038,7 @@ Function concat (s1 s2 : t) : t  :=
 Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2).
 Proof.
  intros s1 s2; functional induction (concat s1 s2); subst;auto.
- destruct _x;try contradiction;clear H1.
+ destruct s1;try contradiction;clear H1.
  intros; apply join_avl; auto.
  generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H2; simpl; auto.
 Qed.
@@ -1048,7 +1048,7 @@ Lemma concat_bst :   forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 ->
  bst (concat s1 s2).
 Proof. 
  intros s1 s2; functional induction (concat s1 s2); subst ;auto.
- destruct _x;try contradiction;clear H1. 
+ destruct s1;try contradiction;clear H1. 
  intros;  apply join_bst; auto.
  generalize (remove_min_bst l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto.
  generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto.
@@ -1064,10 +1064,10 @@ Proof.
  intros s1 s2; functional induction (concat s1 s2);subst;simpl.
  intuition.
  inversion_clear H5.
- destruct _x;try contradiction;clear H1;intuition.
+ destruct s1;try contradiction;clear H1;intuition.
  inversion_clear H5.
- destruct _x;try contradiction;clear H1; intros. 
- rewrite (join_in  (Node _x1 t _x2 i) m s2' y H0).
+ destruct s1;try contradiction;clear H1; intros. 
+ rewrite (join_in  (Node s1_1 t s1_2 i) m s2' y H0).
  generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto.
  generalize (remove_min_in l2 x2 r2 h2 y H3); rewrite H2; simpl.
  intro EQ; rewrite EQ; intuition.