|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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.
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.
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
