Revert "En cours pour 'generalize in clause' et 'induction in clause'"

Sorry, was committed mistakenly.

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

1 files changed, 52 insertions, 41 deletions

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index dd22d493e..b55451233 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -24,16 +24,16 @@ Definition gtof (a b:A) := f b > f a.
 
 Theorem well_founded_ltof : well_founded ltof.
 Proof.
-(* forall n (a : A), f a < n -> Acc ltof a *)
-
-  intro a; assert (H: f a <= f a) by trivial with arith.
-  set (n:=f a) in H at 2. clearbody n. (*
-  remember (f a) in H at 2. as n.
-  revert H. generalize (f a) at 2 as n; intros n. revert a. *) induction n in a, H |- *; apply Acc_intro;
-(*  induction (f a) in a, H at 2 |- *; apply Acc_intro; *)
-  intros b ltfafb; unfold ltof in ltfafb.
-  - inversion H as [H0|]. rewrite H0 in ltfafb. inversion ltfafb.
-  - apply IHn. apply le_S_n, lt_le_trans with (f a); assumption.
+  red.
+  cut (forall n (a:A), f a < n -> Acc ltof a).
+  intros H a; apply (H (S (f a))); auto with arith.
+  induction n.
+  intros; absurd (f a < 0); auto with arith.
+  intros a ltSma.
+  apply Acc_intro.
+  unfold ltof; intros b ltfafb.
+  apply IHn.
+  apply lt_le_trans with (f a); auto with arith.
 Defined.
 
 Theorem well_founded_gtof : well_founded gtof.
@@ -67,11 +67,15 @@ Theorem induction_ltof1 :
   forall P:A -> Set,
     (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
-  intros P F a; assert (H : f a < S (f a)) by trivial with arith.
-  induction (S (f a)) in a, H |- *.
-  - absurd (f a < 0); auto with arith.
-  - apply F. intros b ltfafb. apply IHn, le_S_n.
-    induction H; auto using Le.le_n_S.
+  intros P F; cut (forall n (a:A), f a < n -> P a).
+  intros H a; apply (H (S (f a))); auto with arith.
+  induction n.
+  intros; absurd (f a < 0); auto with arith.
+  intros a ltSma.
+  apply F.
+  unfold ltof; intros b ltfafb.
+  apply IHn.
+  apply lt_le_trans with (f a); auto with arith.
 Defined.
 
 Theorem induction_gtof1 :
@@ -104,12 +108,16 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
 
 Theorem well_founded_lt_compat : well_founded R.
 Proof.
-  intros a; assert (H : f a < S (f a)) by trivial with arith.
-  induction (S (f a)) in a, H |- *.
-  - absurd (f a < 0); auto with arith.
-  - apply Acc_intro. intros b ltfafb. apply IHn, le_S_n.
-    apply H_compat in ltfafb.
-    induction H; auto using Le.le_n_S.
+  red.
+  cut (forall n (a:A), f a < n -> Acc R a).
+  intros H a; apply (H (S (f a))); auto with arith.
+  induction n.
+  intros; absurd (f a < 0); auto with arith.
+  intros a ltSma.
+  apply Acc_intro.
+  intros b ltfafb.
+  apply IHn.
+  apply lt_le_trans with (f a); auto with arith.
 Defined.
 
 End Well_founded_Nat.
@@ -153,7 +161,8 @@ Lemma lt_wf_double_rec :
      (forall p q, p < n -> P p q) ->
      (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
 Proof.
-  intros P Hrec p. destruct p using lt_wf_ind, m using lt_wf_ind. auto.
+  intros P Hrec p; pattern p; apply lt_wf_rec.
+  intros n H q; pattern q; apply lt_wf_rec; auto with arith.
 Defined.
 
 Lemma lt_wf_double_ind :
@@ -190,7 +199,7 @@ Section LT_WF_REL.
   Theorem well_founded_inv_lt_rel_compat : well_founded R.
   Proof.
     constructor; intros.
-    destruct (F_compat y a); trivial.
+    case (F_compat y a); trivial; intros.
     apply acc_lt_rel; trivial.
     exists x; trivial.
   Qed.
@@ -222,27 +231,29 @@ Proof.
   assert
     (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
       \/(forall n', P n' -> n<=n')).
-  { induction n.
-    - right. intros n' Hn'. apply le_O_n.
-    - destruct IHn.
-      + left; destruct H as (n', (Hlt', HPn')).
-        exists n'; split.
-        * apply lt_S; assumption.
-        * assumption.
-      + destruct (Pdec n).
-        * left; exists n; split.
-            apply lt_n_Sn.
-            split; assumption.
-        * right.
-          intros n' Hltn'.
-          destruct (le_lt_eq_dec n n') as [Hltn| ->].
-            apply H; assumption.
-            assumption.
-          destruct H0 as []; assumption. }
+  induction n.
+  right.
+  intros n' Hn'.
+  apply le_O_n.
+  destruct IHn.
+  left; destruct H as (n', (Hlt', HPn')).
+  exists n'; split.
+  apply lt_S; assumption.
+  assumption.
+  destruct (Pdec n).
+  left; exists n; split.
+  apply lt_n_Sn.
+  split; assumption.
+  right.
+  intros n' Hltn'.
+  destruct (le_lt_eq_dec n n') as [Hltn|Heqn].
+  apply H; assumption.
+  assumption.
+  destruct H0.
+  rewrite Heqn; assumption.
   destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
     repeat split;
       assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
-
 Qed.
 
 Unset Implicit Arguments.