From dcda0fbe3784d9cfa45ee5273e2354f3c7b2c9b8 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 4 Oct 2012 22:08:05 +0000
Subject: En cours pour 'generalize in clause' et 'induction in clause'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15852 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Wf_nat.v | 93 ++++++++++++++++++++++---------------------------
 1 file changed, 41 insertions(+), 52 deletions(-)

(limited to 'theories/Arith')

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index b55451233..dd22d493e 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.
-  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.
+(* 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.
 Defined.
 
 Theorem well_founded_gtof : well_founded gtof.
@@ -67,15 +67,11 @@ 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; 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.
+  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.
 Defined.
 
 Theorem induction_gtof1 :
@@ -108,16 +104,12 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
 
 Theorem well_founded_lt_compat : well_founded R.
 Proof.
-  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.
+  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.
 Defined.
 
 End Well_founded_Nat.
@@ -161,8 +153,7 @@ 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; pattern p; apply lt_wf_rec.
-  intros n H q; pattern q; apply lt_wf_rec; auto with arith.
+  intros P Hrec p. destruct p using lt_wf_ind, m using lt_wf_ind. auto.
 Defined.
 
 Lemma lt_wf_double_ind :
@@ -199,7 +190,7 @@ Section LT_WF_REL.
   Theorem well_founded_inv_lt_rel_compat : well_founded R.
   Proof.
     constructor; intros.
-    case (F_compat y a); trivial; intros.
+    destruct (F_compat y a); trivial.
     apply acc_lt_rel; trivial.
     exists x; trivial.
   Qed.
@@ -231,29 +222,27 @@ 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|Heqn].
-  apply H; assumption.
-  assumption.
-  destruct H0.
-  rewrite Heqn; 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| ->].
+            apply H; assumption.
+            assumption.
+          destruct H0 as []; 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.
-- 
cgit v1.2.3