Library Coq.ZArith.Wf_Z
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 (inject_nat n)) ===> (x:Z)`x > 0) -> (P x)
/\
||
||
(Q O) (n:nat)(Q n)->(Q (S n)) <=== (P 0) (x:Z) (P x) -> (P (Zs x))
<=== (inject_nat (S n))=(Zs (inject_nat n))
<=== inject_nat_complete
Then the diagram will be closed and the theorem proved.
Lemma Z_of_nat_complete :
forall x:Z, 0 <=
x ->
exists n :
nat,
x =
Z_of_nat n.
Lemma ZL4_inf :
forall y:positive, {
h :
nat |
nat_of_P y =
S h}.
Lemma Z_of_nat_complete_inf :
forall 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 (
Zsucc 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 (
Zsucc 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 (
Zsucc z)) ->
forall z:Z, 0 <=
z ->
P z.
A variant of the previous using Zpred instead of Zs.
Lemma natlike_rec3 :
forall P:Z ->
Type,
P 0 ->
(
forall z:Z, 0 <
z ->
P (
Zpred z) ->
P z) ->
forall z:Z, 0 <=
z ->
P z.
A more general induction principle on non-negative numbers using Zlt.
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 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.
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 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.
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.