Wf_Z.v

(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)

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.

intros n; 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.

intros n; 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.

Local Definition 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.

Defined.

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 z.

induction z as [z IH] using (well_founded_induction_type R_wf).

destruct z as [|p|p]; 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 z.

induction z as [z IH] using (well_founded_induction_type R_wf).

destruct z as [|p|p]; 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 x.

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 P z ? x ?; now apply Zlt_lower_bound_rec with z.

Qed.

End Efficient_Rec.

Timings for Wf_Z.v