recursion bien fondee sur des pairs

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

2 files changed, 44 insertions, 1 deletions

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index dff48c9537..93111571f7 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -19,6 +19,7 @@ V7only [Unset Implicit Arguments.].
 
 Require Logic.
 Require LogicSyntax.
+Require Datatypes.
 
 (** Well-founded induction principle on Prop *)
 
@@ -131,3 +132,27 @@ Qed.
 End FixPoint.
 
 End Well_founded. 
+
+(** A recursor over pairs *)
+
+Chapter Well_founded_2.
+
+  Variable A,B : Set.
+  Variable R : A * B -> A * B -> Prop.
+
+  Variable P : A -> B -> Type. 
+  Variable F : (x:A)(x':B)((y:A)(y':B)(R (y,y') (x,x'))-> (P y y'))->(P x x').
+
+  Fixpoint Acc_iter_2 [x:A;x':B;a:(Acc ? R (x,x'))] : (P x x')
+     := (F x x' ([y:A][y':B][h:(R (y,y') (x,x'))](Acc_iter_2 y y' (Acc_inv ? ? (x,x') a (y,y') h)))).
+
+  Hypothesis Rwf : (well_founded ? R).
+
+  Theorem well_founded_induction_type_2 : 
+     ((x:A)(x':B)((y:A)(y':B)(R (y,y') (x,x'))->(P y y'))->(P x x'))->(a:A)(b:B)(P a b).
+  Proof.
+   Intros; Apply Acc_iter_2; Auto.
+  Qed.
+
+End Well_founded_2.
+
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 122de1e2de..c303b6fe7c 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -147,6 +147,23 @@ Intuition; Elim H1; Simpl; Trivial.
 Qed.
 
 Lemma natlike_rec2 : (P:Z->Type)(P `0`) -> 
+        ((z:Z)`0<=z` -> (P z) -> (P (Zs z))) -> (z:Z)`0<=z` -> (P z).
+Proof.
+Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf).
+Intro x; Case x.
+Trivial.
+Intros.
+Assert `0<=(Zpred (POS p))`.
+Apply Zlt_ZERO_pred_le_ZERO; Unfold Zlt; Simpl; Trivial.
+Rewrite Zs_pred.
+Apply Hrec.
+Auto.
+Apply X; Unfold R; Intuition.
+Intros; Elim H; Simpl; Trivial.
+Qed.
+
+(** variant using [Zpred] instead of [Zs] *)
+Lemma natlike_rec3 : (P:Z->Type)(P `0`) -> 
         ((z:Z)`0<z` -> (P (Zpred z)) -> (P z)) -> (z:Z)`0<=z` -> (P z).
 Proof.
 Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf).
@@ -205,7 +222,7 @@ Auto with zarith.
 
 Split; [ Assumption | Exact (Zlt_n_Sn x) ].
 
-Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_rec.
+Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_rec2.
 Intros.
 Absurd `0 <= 0`; Try Assumption.
 Apply Zgt_not_le.
@@ -221,3 +238,4 @@ Apply Zgt_S_le. Apply Zlt_gt. Intuition.
 
 Assumption.
 Qed.
+