diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-07-08 13:43:16 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-07-08 13:43:16 +0000 |
commit | 4844bf0fa24d049b28a7aa1788c5d85e8b98753d (patch) | |
tree | e8d9003ad3e0e6cf6d95b9b2e7550d5fe0ae0110 /theories/ZArith | |
parent | 0f07e18c269c2c5db3c557cfa83e6d88a1cb7bd4 (diff) |
recursion bien fondee sur des pairs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4224 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
-rw-r--r-- | theories/ZArith/Wf_Z.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 122de1e2d..c303b6fe7 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. + |