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.
intro x; destruct x; intros;
[ exists 0%nat; auto with arith
| specialize (ZL4 p); intros Hp; elim Hp; intros; exists (S x); intros;
simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x);
intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f:= Zpos);
apply nat_of_P_inj; auto with arith
| absurd (0 <= Zneg p);
[ unfold Zle in |- *; simpl in |- *; do 2 unfold not in |- *;
auto with arith
| assumption ] ].
Qed.
Lemma ZL4_inf : forall y:positive, {h : nat | nat_of_P y = S h}.
intro y; induction y as [p H| p H1| ];
[ elim H; intros x H1; exists (S x + S x)%nat; unfold nat_of_P in |- *;
simpl in |- *; rewrite ZL0; rewrite Pmult_nat_r_plus_morphism;
unfold nat_of_P in H1; rewrite H1; auto with arith
| elim H1; intros x H2; exists (x + S x)%nat; unfold nat_of_P in |- *;
simpl in |- *; rewrite ZL0; rewrite Pmult_nat_r_plus_morphism;
unfold nat_of_P in H2; rewrite H2; auto with arith
| exists 0%nat; auto with arith ].
Qed.
Lemma Z_of_nat_complete_inf :
forall x:Z, 0 <= x -> {n : nat | x = Z_of_nat n}.
intro x; destruct x; intros;
[ exists 0%nat; auto with arith
| specialize (ZL4_inf p); intros Hp; elim Hp; intros x0 H0; exists (S x0);
intros; simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x0);
intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f:= Zpos);
apply nat_of_P_inj; auto with arith
| absurd (0 <= Zneg p);
[ unfold Zle in |- *; simpl in |- *; do 2 unfold not in |- *;
auto with arith
| assumption ] ].
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.
intros P H x H0.
specialize (Z_of_nat_complete x H0).
intros Hn; elim Hn; intros.
rewrite H1; apply H.
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.
intros P H x H0.
specialize (Z_of_nat_complete_inf x H0).
intros Hn; elim Hn; intros.
rewrite p; apply H.
Qed.
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.
intros P H H0 x H1; apply Z_of_nat_prop;
[ simple induction n;
[ simpl in |- *; assumption
| intros; rewrite (inj_S n0); exact (H0 (Z_of_nat n0) (Zle_0_nat n0) H2) ]
| assumption ].
Qed.
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.
intros P H H0 x H1; apply Z_of_nat_set;
[ simple induction n;
[ simpl in |- *; assumption
| intros; rewrite (inj_S n0); exact (H0 (Z_of_nat n0) (Zle_0_nat n0) H2) ]
| assumption ].
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.
set
(f:=
fun z =>
match z with
| Zpos p => nat_of_P p
| Z0 => 0%nat
| Zneg _ => 0%nat
end) in *.
apply well_founded_lt_compat with f.
unfold R, f in |- *; clear f R.
intros x y; case x; intros; elim H; clear H.
case y; intros; apply lt_O_nat_of_P || inversion H0.
case y; intros; apply nat_of_P_lt_Lt_compare_morphism || inversion H0; auto.
intros; elim H; auto.
Qed.
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.
Proof.
intros P Ho Hrec z; pattern z in |- *;
apply (well_founded_induction_type R_wf).
intro x; case x.
trivial.
intros.
assert (0 <= Zpred (Zpos p)).
apply Zorder.Zlt_0_le_0_pred; unfold Zlt in |- *; simpl in |- *; trivial.
rewrite Zsucc_pred.
apply Hrec.
auto.
apply X; auto; unfold R in |- *; intuition; apply Zlt_pred.
intros; elim H; simpl in |- *; trivial.
Qed.
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.
Proof.
intros P Ho Hrec z; pattern z in |- *;
apply (well_founded_induction_type R_wf).
intro x; case x.
trivial.
intros; apply Hrec.
unfold Zlt in |- *; trivial.
assert (0 <= Zpred (Zpos p)).
apply Zorder.Zlt_0_le_0_pred; unfold Zlt in |- *; simpl in |- *; trivial.
apply X; auto; unfold R in |- *; intuition; apply Zlt_pred.
intros; elim H; simpl in |- *; trivial.
Qed.
A more general induction principal using Zlt.
|
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 z; pattern z in |- *; apply (well_founded_induction_type R_wf).
intro x; case x; intros.
apply Hrec; intros.
assert (H2 : 0 < 0).
apply Zle_lt_trans with y; intuition.
inversion H2.
firstorder.
unfold Zle, Zcompare in H; elim H; auto.
Defined.
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.
exact Z_lt_rec.
Qed.
End Efficient_Rec.