Library Coq.ZArith.Wf_Z



Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.
Require Import Znat.
Require Import Zmisc.
Require Import Wf_nat.
Open Local 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 (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.