Library Coq.ZArith.Wf_Z

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.

Lemma Z_of_nat_complete_inf (x : Z) :
0 <= x -> {n : nat | x = Z.of_nat n}.

Lemma Z_of_nat_prop :
forall P:Z -> Prop,
(forall n:nat, P (Z.of_nat n)) -> forall x:Z, 0 <= x -> P x.

Lemma Z_of_nat_set :
forall P:Z -> Set,
(forall n:nat, P (Z.of_nat n)) -> forall x:Z, 0 <= x -> P x.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

End Efficient_Rec.