Library Stdlib.ZArith.Wf_Z
From Stdlib Require Import BinInt.
From Stdlib Require Import Zcompare.
From Stdlib Require Import Zorder.
From Stdlib Require Import Znat.
From Stdlib Require Import Zmisc.
From Stdlib 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_completeThen 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.
Local Definition 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.