Finalement, préservation de la compatibilité pour Z_lt_induction et ajout plutôt de nouveaux énoncés

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

2 files changed, 56 insertions, 5 deletions

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index b8113b2e0..adcd40639 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -176,9 +176,9 @@ apply X; auto; unfold R in |- *; intuition; apply Zlt_pred.
 intros; elim H; simpl in |- *; trivial.
 Qed.
 
-(** A more general induction principal using [Zlt]. *)
+(** A more general induction principle on non-negative numbers using [Zlt]. *)
 
-Lemma Z_lt_rec :
+Lemma Zlt_0_rec :
  forall P:Z -> Type,
    (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
    forall x:Z, 0 <= x -> P x.
@@ -194,12 +194,63 @@ firstorder.
 unfold Zle, Zcompare in H; elim H; auto.
 Defined.
 
-Lemma Z_lt_induction :
+Lemma Zlt_0_ind :
  forall P:Z -> Prop,
    (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
    forall x:Z, 0 <= x -> P x.
 Proof.
+exact Zlt_0_rec.
+Qed.
+
+(** Obsolete version of [Zlt] induction principle on non-negative numbers *)
+
+Lemma Z_lt_rec :
+ forall P:Z -> Type,
+   (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
+   forall x:Z, 0 <= x -> P x.
+Proof.
+intros P Hrec; apply Zlt_0_rec; auto.
+Qed.
+
+Lemma Z_lt_induction :
+ forall P:Z -> Prop,
+   (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
+   forall x:Z, 0 <= x -> P x.
+Proof.
 exact Z_lt_rec.
 Qed.
 
+(** An even more general induction principle using [Zlt]. *)
+
+Lemma Zlt_lower_bound_rec :
+ forall P:Z -> Type, forall z:Z,
+   (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) ->
+   forall x:Z, z <= x -> P x.
+Proof.
+intros P z Hrec x.
+assert (Hexpand : forall x, x = x - z + z).
+  intro; unfold Zminus; rewrite <- Zplus_assoc; rewrite Zplus_opp_l;
+  rewrite Zplus_0_r; trivial.
+intro Hz.
+rewrite (Hexpand x); pattern (x - z) in |- *; apply Zlt_0_rec.
+2: apply Zplus_le_reg_r with z; rewrite <- Hexpand; assumption.
+intros x0 Hlt_x0 H.
+apply Hrec.
+  2: change z with (0+z); apply Zplus_le_compat_r; assumption.
+  intro y; rewrite (Hexpand y); intros.
+destruct H0.
+apply Hlt_x0.
+split.
+  apply Zplus_le_reg_r with z; assumption.
+  apply Zplus_lt_reg_r with z; assumption.
+Qed.
+
+Lemma Zlt_lower_bound_ind :
+ forall P:Z -> Prop, forall z:Z,
+   (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) ->
+   forall x:Z, z <= x -> P x.
+Proof.
+exact Zlt_lower_bound_rec.
+Qed.
+
 End Efficient_Rec.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 131460a75..452ebd30f 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -278,7 +278,7 @@ Lemma euclid_rec :
      (forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid.
 Proof.
 intros v3 Hv3; generalize Hv3; pattern v3 in |- *.
-apply Z_lt_rec.
+apply Zlt_0_rec.
 clear v3 Hv3; intros.
 elim (Z_zerop x); intro.
 apply Euclid_intro with (u := u1) (v := u2) (d := u3).
@@ -377,7 +377,7 @@ Definition Zgcd_pos :
 Proof.
 intros a Ha.
 apply
- (Z_lt_rec
+ (Zlt_0_rec
     (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}));
  try assumption.
 intro x; case x.