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.
Proof.
intros H. exists (Z.to_nat x). symmetry. now apply Z2Nat.id.
Qed.

Lemma Z_of_nat_complete_inf (x : Z) :
0 <= x -> {n : nat | x = Z.of_nat n }.
Proof.
intros H. exists (Z.to_nat x). symmetry. 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.
Proof.
intros P H x Hx. 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.
Proof.
intros P H x Hx. 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.
Proof.
intros P Ho Hrec x Hx; apply Z_of_nat_prop; trivial.
induction n. exact Ho.
rewrite Nat2Z.inj_succ. 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.
Proof.
intros P Ho Hrec x Hx; apply Z_of_nat_set; trivial.
induction n. exact Ho.
rewrite Nat2Z.inj_succ. 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.
  Proof.
   apply well_founded_lt_compat with Z.to_nat.
   intros x y (Hx,H). 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.
  Proof.
   intros P Ho Hrec.
   induction z as [z IH] using (well_founded_induction_type R_wf).
   destruct z; intros Hz.
   - apply Ho.
   - set (y:=Z.pred (Zpos p)).
     assert (LE : 0 <= y) by (unfold y; now apply Z.lt_le_pred).
     assert (EQ : Zpos p = Z.succ y) by (unfold y; now rewrite Z.succ_pred).
     rewrite EQ. apply Hrec, IH; trivial.
     split; trivial. unfold y; apply Z.lt_pred_l.
   - 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.
  Proof.
   intros P Ho Hrec.
   induction z as [z IH] using (well_founded_induction_type R_wf).
   destruct z; intros Hz.
   - apply Ho.
   - assert (EQ : 0 <= Z.pred (Zpos p)) by now apply Z.lt_le_pred.
     apply Hrec. easy. apply IH; trivial. split; trivial.
     apply Z.lt_pred_l.
   - 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.
  Proof.
   intros P Hrec.
   induction x as [x IH] using (well_founded_induction_type R_wf).
   destruct x; intros Hx.
   - apply Hrec; trivial. intros y (Hy,Hy').
     assert (0 < 0) by now apply Z.le_lt_trans with y.
     discriminate.
   - apply Hrec; trivial. intros y (Hy,Hy').
     apply IH; trivial. now split.
   - 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.
  Proof. 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.
  Proof.
    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.
  Proof.
    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.
  Proof.
    intros P z Hrec x Hx.
    rewrite <- (Z.sub_simpl_r x z). apply Z.le_0_sub in Hx.
    pattern (x - z); apply Zlt_0_rec; trivial.
    clear x Hx. intros x IH Hx.
    apply Hrec. intros y (Hy,Hy').
    rewrite <- (Z.sub_simpl_r y z). apply IH; split.
    now rewrite Z.le_0_sub.
    now apply Z.lt_sub_lt_add_r.
    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.
  Proof.
    intros; now apply Zlt_lower_bound_rec with z.
  Qed.

End Efficient_Rec.