Wf_Z.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.
Require Import Znat.
Require Import Zmisc.
Require Import Wf_nat.
Local Open Scope Z_scope.

Our purpose is to write an induction shema for {0,1,2,...} similar to the nat schema (Theorem Natlike_rec). For that the following implications will be used :

 ∀n:nat, Q n == ∀n:nat, P (Z.of_nat n) ===> ∀x:Z, x <= 0 -> P x

       	     /\
             ||
             ||

 (Q O) ∧ (∀n:nat, Q n -> Q (S n)) <=== (P 0) ∧ (∀x:Z, P x -> P (Z.succ x))

				  <=== (Z.of_nat (S n) = Z.succ (Z.of_nat n))

				  <=== Z_of_nat_complete

Then the diagram will be closed and the theorem proved.

Lemma Z_of_nat_complete (x : Z) :
 0 <= x -> exists n : nat, x = Z.of_nat n.x:Z
0 <= x -> exists n : nat, x = Z.of_nat n
Proof.x:Z
0 <= x -> exists n : nat, x = Z.of_nat n
 intros H.x:Z
H:0 <= x
exists n : nat, x = Z.of_nat n exists (Z.to_nat x).x:Z
H:0 <= x
x = Z.of_nat (Z.to_nat x) symmetry.x:Z
H:0 <= x
Z.of_nat (Z.to_nat x) = x now apply Z2Nat.id.
Qed.

Lemma Z_of_nat_complete_inf (x : Z) :
 0 <= x -> {n : nat | x = Z.of_nat n}.x:Z
0 <= x -> {n : nat | x = Z.of_nat n}
Proof.x:Z
0 <= x -> {n : nat | x = Z.of_nat n}
 intros H.x:Z
H:0 <= x
{n : nat | x = Z.of_nat n} exists (Z.to_nat x).x:Z
H:0 <= x
x = Z.of_nat (Z.to_nat x) symmetry.x:Z
H:0 <= x
Z.of_nat (Z.to_nat x) = x now apply Z2Nat.id.
Qed.

Lemma Z_of_nat_prop :
  forall P:Z -> Prop,
    (forall n:nat, P (Z.of_nat n)) -> forall x:Z, 0 <= x -> P x.forall P : Z -> Prop,
(forall n : nat, P (Z.of_nat n)) ->
forall x : Z, 0 <= x -> P x
Proof.forall P : Z -> Prop,
(forall n : nat, P (Z.of_nat n)) ->
forall x : Z, 0 <= x -> P x
 intros P H x Hx.P:Z -> Prop
H:forall n : nat, P (Z.of_nat n)
x:Z
Hx:0 <= x
P x now destruct (Z_of_nat_complete x Hx) as (n,->).
Qed.

Lemma Z_of_nat_set :
 forall P:Z -> Set,
   (forall n:nat, P (Z.of_nat n)) -> forall x:Z, 0 <= x -> P x.forall P : Z -> Set,
(forall n : nat, P (Z.of_nat n)) ->
forall x : Z, 0 <= x -> P x
Proof.forall P : Z -> Set,
(forall n : nat, P (Z.of_nat n)) ->
forall x : Z, 0 <= x -> P x
 intros P H x Hx.P:Z -> Set
H:forall n : nat, P (Z.of_nat n)
x:Z
Hx:0 <= x
P x now destruct (Z_of_nat_complete_inf x Hx) as (n,->).
Qed.

Lemma natlike_ind :
 forall P:Z -> Prop,
   P 0 ->
   (forall x:Z, 0 <= x -> P x -> P (Z.succ x)) ->
   forall x:Z, 0 <= x -> P x.forall P : Z -> Prop,
P 0 ->
(forall x : Z, 0 <= x -> P x -> P (Z.succ x)) ->
forall x : Z, 0 <= x -> P x
Proof.forall P : Z -> Prop,
P 0 ->
(forall x : Z, 0 <= x -> P x -> P (Z.succ x)) ->
forall x : Z, 0 <= x -> P x
 intros P Ho Hrec x Hx; apply Z_of_nat_prop; trivial.P:Z -> Prop
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
forall n : nat, P (Z.of_nat n)
 induction n.P:Z -> Prop
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
P (Z.of_nat 0)
P:Z -> Prop
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
n:nat
IHn:P (Z.of_nat n)
P (Z.of_nat (S n)) exact Ho.P:Z -> Prop
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
n:nat
IHn:P (Z.of_nat n)
P (Z.of_nat (S n))
 rewrite Nat2Z.inj_succ.P:Z -> Prop
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
n:nat
IHn:P (Z.of_nat n)
P (Z.succ (Z.of_nat n)) apply Hrec; trivial using Nat2Z.is_nonneg.
Qed.

Lemma natlike_rec :
 forall P:Z -> Set,
   P 0 ->
   (forall x:Z, 0 <= x -> P x -> P (Z.succ x)) ->
   forall x:Z, 0 <= x -> P x.forall P : Z -> Set,
P 0 ->
(forall x : Z, 0 <= x -> P x -> P (Z.succ x)) ->
forall x : Z, 0 <= x -> P x
Proof.forall P : Z -> Set,
P 0 ->
(forall x : Z, 0 <= x -> P x -> P (Z.succ x)) ->
forall x : Z, 0 <= x -> P x
 intros P Ho Hrec x Hx; apply Z_of_nat_set; trivial.P:Z -> Set
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
forall n : nat, P (Z.of_nat n)
 induction n.P:Z -> Set
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
P (Z.of_nat 0)
P:Z -> Set
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
n:nat
IHn:P (Z.of_nat n)
P (Z.of_nat (S n)) exact Ho.P:Z -> Set
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
n:nat
IHn:P (Z.of_nat n)
P (Z.of_nat (S n))
 rewrite Nat2Z.inj_succ.P:Z -> Set
Ho:P 0
Hrec:forall x0 : Z, 0 <= x0 -> P x0 -> P (Z.succ x0)
x:Z
Hx:0 <= x
n:nat
IHn:P (Z.of_nat n)
P (Z.succ (Z.of_nat n)) apply Hrec; trivial using Nat2Z.is_nonneg.
Qed.

Section Efficient_Rec.

natlike_rec2 is the same as natlike_rec, but with a different proof, designed to give a better extracted term.

  Let R (a b:Z) := 0 <= a /\ a < b.

  Let R_wf : well_founded R.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
well_founded R
  Proof.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
well_founded R
   apply well_founded_lt_compat with Z.to_nat.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
forall x y : Z, R x y -> (Z.to_nat x < Z.to_nat y)%nat
   intros x y (Hx,H).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
x, y:Z
Hx:0 <= x
H:x < y
(Z.to_nat x < Z.to_nat y)%nat apply Z2Nat.inj_lt; Z.order.
  Qed.

  Lemma natlike_rec2 :
    forall P:Z -> Type,
      P 0 ->
      (forall z:Z, 0 <= z -> P z -> P (Z.succ z)) ->
      forall z:Z, 0 <= z -> P z.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall P : Z -> Type,
P 0 ->
(forall z : Z, 0 <= z -> P z -> P (Z.succ z)) ->
forall z : Z, 0 <= z -> P z
  Proof.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall P : Z -> Type,
P 0 ->
(forall z : Z, 0 <= z -> P z -> P (Z.succ z)) ->
forall z : Z, 0 <= z -> P z
   intros P Ho Hrec.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
forall z : Z, 0 <= z -> P z
   induction z as [z IH] using (well_founded_induction_type R_wf).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z0 : Z, 0 <= z0 -> P z0 -> P (Z.succ z0)
z:Z
IH:forall y : Z, R y z -> 0 <= y -> P y
0 <= z -> P z
   destruct z; intros Hz.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
IH:forall y : Z, R y 0 -> 0 <= y -> P y
Hz:0 <= 0
P 0
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
P (Z.pos p)
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y : Z, R y (Z.neg p) -> 0 <= y -> P y
Hz:0 <= Z.neg p
P (Z.neg p)
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
IH:forall y : Z, R y 0 -> 0 <= y -> P y
Hz:0 <= 0
P 0 apply Ho.
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
P (Z.pos p) set (y:=Z.pred (Zpos p)).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y0 : Z, R y0 (Z.pos p) -> 0 <= y0 -> P y0
Hz:0 <= Z.pos p
y:=Z.pred (Z.pos p):Z
P (Z.pos p)
     assert (LE : 0 <= y) by (unfold y; now apply Z.lt_le_pred).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y0 : Z, R y0 (Z.pos p) -> 0 <= y0 -> P y0
Hz:0 <= Z.pos p
y:=Z.pred (Z.pos p):Z
LE:0 <= y
P (Z.pos p)
     assert (EQ : Zpos p = Z.succ y) by (unfold y; now rewrite Z.succ_pred).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y0 : Z, R y0 (Z.pos p) -> 0 <= y0 -> P y0
Hz:0 <= Z.pos p
y:=Z.pred (Z.pos p):Z
LE:0 <= y
EQ:Z.pos p = Z.succ y
P (Z.pos p)
     rewrite EQ.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y0 : Z, R y0 (Z.pos p) -> 0 <= y0 -> P y0
Hz:0 <= Z.pos p
y:=Z.pred (Z.pos p):Z
LE:0 <= y
EQ:Z.pos p = Z.succ y
P (Z.succ y) apply Hrec, IH; trivial.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y0 : Z, R y0 (Z.pos p) -> 0 <= y0 -> P y0
Hz:0 <= Z.pos p
y:=Z.pred (Z.pos p):Z
LE:0 <= y
EQ:Z.pos p = Z.succ y
R y (Z.pos p)
     split; trivial.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y0 : Z, R y0 (Z.pos p) -> 0 <= y0 -> P y0
Hz:0 <= Z.pos p
y:=Z.pred (Z.pos p):Z
LE:0 <= y
EQ:Z.pos p = Z.succ y
y < Z.pos p unfold y; apply Z.lt_pred_l.
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 <= z -> P z -> P (Z.succ z)
p:positive
IH:forall y : Z, R y (Z.neg p) -> 0 <= y -> P y
Hz:0 <= Z.neg p
P (Z.neg p) now destruct Hz.
  Qed.

A variant of the previous using Z.pred instead of Z.succ.

  Lemma natlike_rec3 :
    forall P:Z -> Type,
      P 0 ->
      (forall z:Z, 0 < z -> P (Z.pred z) -> P z) ->
      forall z:Z, 0 <= z -> P z.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall P : Z -> Type,
P 0 ->
(forall z : Z, 0 < z -> P (Z.pred z) -> P z) ->
forall z : Z, 0 <= z -> P z
  Proof.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall P : Z -> Type,
P 0 ->
(forall z : Z, 0 < z -> P (Z.pred z) -> P z) ->
forall z : Z, 0 <= z -> P z
   intros P Ho Hrec.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
forall z : Z, 0 <= z -> P z
   induction z as [z IH] using (well_founded_induction_type R_wf).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z0 : Z, 0 < z0 -> P (Z.pred z0) -> P z0
z:Z
IH:forall y : Z, R y z -> 0 <= y -> P y
0 <= z -> P z
   destruct z; intros Hz.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
IH:forall y : Z, R y 0 -> 0 <= y -> P y
Hz:0 <= 0
P 0
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
P (Z.pos p)
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.neg p) -> 0 <= y -> P y
Hz:0 <= Z.neg p
P (Z.neg p)
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
IH:forall y : Z, R y 0 -> 0 <= y -> P y
Hz:0 <= 0
P 0 apply Ho.
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
P (Z.pos p) assert (EQ : 0 <= Z.pred (Zpos p)) by now apply Z.lt_le_pred.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
EQ:0 <= Z.pred (Z.pos p)
P (Z.pos p)
     apply Hrec.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
EQ:0 <= Z.pred (Z.pos p)
0 < Z.pos p
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
EQ:0 <= Z.pred (Z.pos p)
P (Z.pred (Z.pos p)) easy.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
EQ:0 <= Z.pred (Z.pos p)
P (Z.pred (Z.pos p)) apply IH; trivial.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
EQ:0 <= Z.pred (Z.pos p)
R (Z.pred (Z.pos p)) (Z.pos p) split; trivial.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hz:0 <= Z.pos p
EQ:0 <= Z.pred (Z.pos p)
Z.pred (Z.pos p) < Z.pos p
     apply Z.lt_pred_l.
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Ho:P 0
Hrec:forall z : Z, 0 < z -> P (Z.pred z) -> P z
p:positive
IH:forall y : Z, R y (Z.neg p) -> 0 <= y -> P y
Hz:0 <= Z.neg p
P (Z.neg p) now destruct Hz.
  Qed.

A more general induction principle on non-negative numbers using Z.lt.

  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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
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
  Proof.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
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
   intros P Hrec.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
forall x : Z, 0 <= x -> P x
   induction x as [x IH] using (well_founded_induction_type R_wf).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x0 : Z,
(forall y : Z, 0 <= y < x0 -> P y) ->
0 <= x0 -> P x0
x:Z
IH:forall y : Z, R y x -> 0 <= y -> P y
0 <= x -> P x
   destruct x; intros Hx.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
IH:forall y : Z, R y 0 -> 0 <= y -> P y
Hx:0 <= 0
P 0
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hx:0 <= Z.pos p
P (Z.pos p)
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
p:positive
IH:forall y : Z, R y (Z.neg p) -> 0 <= y -> P y
Hx:0 <= Z.neg p
P (Z.neg p)
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
IH:forall y : Z, R y 0 -> 0 <= y -> P y
Hx:0 <= 0
P 0 apply Hrec; trivial.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
IH:forall y : Z, R y 0 -> 0 <= y -> P y
Hx:0 <= 0
forall y : Z, 0 <= y < 0 -> P y intros y (Hy,Hy').R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y0 : Z, 0 <= y0 < x -> P y0) ->
0 <= x -> P x
IH:forall y0 : Z, R y0 0 -> 0 <= y0 -> P y0
Hx:0 <= 0
y:Z
Hy:0 <= y
Hy':y < 0
P y
     assert (0 < 0) by now apply Z.le_lt_trans with y.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y0 : Z, 0 <= y0 < x -> P y0) ->
0 <= x -> P x
IH:forall y0 : Z, R y0 0 -> 0 <= y0 -> P y0
Hx:0 <= 0
y:Z
Hy:0 <= y
Hy':y < 0
H:0 < 0
P y
     discriminate.
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hx:0 <= Z.pos p
P (Z.pos p) apply Hrec; trivial.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
p:positive
IH:forall y : Z, R y (Z.pos p) -> 0 <= y -> P y
Hx:0 <= Z.pos p
forall y : Z, 0 <= y < Z.pos p -> P y intros y (Hy,Hy').R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y0 : Z, 0 <= y0 < x -> P y0) ->
0 <= x -> P x
p:positive
IH:forall y0 : Z, R y0 (Z.pos p) -> 0 <= y0 -> P y0
Hx:0 <= Z.pos p
y:Z
Hy:0 <= y
Hy':y < Z.pos p
P y
     apply IH; trivial.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y0 : Z, 0 <= y0 < x -> P y0) ->
0 <= x -> P x
p:positive
IH:forall y0 : Z, R y0 (Z.pos p) -> 0 <= y0 -> P y0
Hx:0 <= Z.pos p
y:Z
Hy:0 <= y
Hy':y < Z.pos p
R y (Z.pos p) now split.
   -R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
Hrec:forall x : Z,
(forall y : Z, 0 <= y < x -> P y) ->
0 <= x -> P x
p:positive
IH:forall y : Z, R y (Z.neg p) -> 0 <= y -> P y
Hx:0 <= Z.neg p
P (Z.neg p) now destruct Hx.
  Defined.

  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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
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 intros; now apply Zlt_0_rec. Qed.

Obsolete version of Z.lt 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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall P : Z -> Type,
(forall x : Z,
 (forall y : Z, 0 <= y < x -> P y) -> P x) ->
forall x : Z, 0 <= x -> P x
    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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall P : Z -> Prop,
(forall x : Z,
 (forall y : Z, 0 <= y < x -> P y) -> P x) ->
forall x : Z, 0 <= x -> P x
    intros; now apply Z_lt_rec.
  Qed.

An even more general induction principle using Z.lt.

  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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall (P : Z -> Type) (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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall (P : Z -> Type) (z : Z),
(forall x : Z,
 (forall y : Z, z <= y < x -> P y) -> z <= x -> P x) ->
forall x : Z, z <= x -> P x
    intros P z Hrec x Hx.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
Hx:z <= x
P x
    rewrite <- (Z.sub_simpl_r x z).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
Hx:z <= x
P (x - z + z) apply Z.le_0_sub in Hx.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
Hx:0 <= x - z
P (x - z + z)
    pattern (x - z); apply Zlt_0_rec; trivial.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
Hx:0 <= x - z
forall x0 : Z,
(forall y : Z, 0 <= y < x0 -> P (y + z)) ->
0 <= x0 -> P (x0 + z)
    clear x Hx.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x : Z,
(forall y : Z, z <= y < x -> P y) ->
z <= x -> P x
forall x : Z,
(forall y : Z, 0 <= y < x -> P (y + z)) ->
0 <= x -> P (x + z) intros x IH Hx.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
IH:forall y : Z, 0 <= y < x -> P (y + z)
Hx:0 <= x
P (x + z)
    apply Hrec.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
IH:forall y : Z, 0 <= y < x -> P (y + z)
Hx:0 <= x
forall y : Z, z <= y < x + z -> P y
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
IH:forall y : Z, 0 <= y < x -> P (y + z)
Hx:0 <= x
z <= x + z intros y (Hy,Hy').R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y0 : Z, z <= y0 < x0 -> P y0) ->
z <= x0 -> P x0
x:Z
IH:forall y0 : Z, 0 <= y0 < x -> P (y0 + z)
Hx:0 <= x
y:Z
Hy:z <= y
Hy':y < x + z
P y
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
IH:forall y : Z, 0 <= y < x -> P (y + z)
Hx:0 <= x
z <= x + z
    rewrite <- (Z.sub_simpl_r y z).R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y0 : Z, z <= y0 < x0 -> P y0) ->
z <= x0 -> P x0
x:Z
IH:forall y0 : Z, 0 <= y0 < x -> P (y0 + z)
Hx:0 <= x
y:Z
Hy:z <= y
Hy':y < x + z
P (y - z + z)
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
IH:forall y : Z, 0 <= y < x -> P (y + z)
Hx:0 <= x
z <= x + z apply IH; split.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y0 : Z, z <= y0 < x0 -> P y0) ->
z <= x0 -> P x0
x:Z
IH:forall y0 : Z, 0 <= y0 < x -> P (y0 + z)
Hx:0 <= x
y:Z
Hy:z <= y
Hy':y < x + z
0 <= y - z
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y0 : Z, z <= y0 < x0 -> P y0) ->
z <= x0 -> P x0
x:Z
IH:forall y0 : Z, 0 <= y0 < x -> P (y0 + z)
Hx:0 <= x
y:Z
Hy:z <= y
Hy':y < x + z
y - z < x
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
IH:forall y : Z, 0 <= y < x -> P (y + z)
Hx:0 <= x
z <= x + z
    now rewrite Z.le_0_sub.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y0 : Z, z <= y0 < x0 -> P y0) ->
z <= x0 -> P x0
x:Z
IH:forall y0 : Z, 0 <= y0 < x -> P (y0 + z)
Hx:0 <= x
y:Z
Hy:z <= y
Hy':y < x + z
y - z < x
R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
IH:forall y : Z, 0 <= y < x -> P (y + z)
Hx:0 <= x
z <= x + z
    now apply Z.lt_sub_lt_add_r.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
P:Z -> Type
z:Z
Hrec:forall x0 : Z,
(forall y : Z, z <= y < x0 -> P y) ->
z <= x0 -> P x0
x:Z
IH:forall y : Z, 0 <= y < x -> P (y + z)
Hx:0 <= x
z <= x + z
    now rewrite <- (Z.add_le_mono_r 0 x z).
  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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall (P : Z -> Prop) (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.R:=fun a b : Z => 0 <= a < b:Z -> Z -> Prop
R_wf:well_founded R
forall (P : Z -> Prop) (z : Z),
(forall x : Z,
 (forall y : Z, z <= y < x -> P y) -> z <= x -> P x) ->
forall x : Z, z <= x -> P x
    intros; now apply Zlt_lower_bound_rec with z.
  Qed.

End Efficient_Rec.