Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot

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

1 files changed, 12 insertions, 1 deletions

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 01509fa12..11d213202 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -50,6 +50,17 @@ Chapter Well_founded.
 
  Definition Acc_rec [P:A->Set] := (Acc_rect P).
 
+ (** A simplified version of Acc_rec(t) *)
+
+ Section AccIter.
+  Variable P : A -> Type. 
+  Variable F : (x:A)((y:A)(R y x)-> (P y))->(P x).
+
+  Fixpoint Acc_iter [x:A;a:(Acc x)] : (P x)
+     := (F x ([y:A][h:(R y x)](Acc_iter y (Acc_inv x a y h)))).
+
+ End AccIter.
+
  (** A relation is well-founded if every element is accessible *)
 
  Definition well_founded := (a:A)(Acc a).
@@ -61,7 +72,7 @@ Chapter Well_founded.
  Theorem well_founded_induction_type : 
         (P:A->Type)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
  Proof.
-  Intros; Apply (Acc_rect P); Auto.
+  Intros; Apply (Acc_iter P); Auto.
  Qed.
 
  Theorem well_founded_induction :