diff options
Diffstat (limited to 'theories/ZArith/Wf_Z.v')
| -rw-r--r-- | theories/ZArith/Wf_Z.v | 355 |
1 files changed, 181 insertions, 174 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index af1fdd0b..1d7948a5 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf_Z.v 6984 2005-05-02 10:50:15Z herbelin $ i*) +(*i $Id: Wf_Z.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import BinInt. Require Import Zcompare. @@ -35,222 +35,229 @@ Open Local Scope Z_scope. 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 ] ]. + forall x:Z, 0 <= x -> exists n : nat, x = Z_of_nat n. +Proof. + 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 ]. +Proof. + 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 ] ]. +Proof. + 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. + forall P:Z -> Prop, + (forall n:nat, P (Z_of_nat n)) -> forall x:Z, 0 <= x -> P x. +Proof. + 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. +Proof. + 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 ]. +Proof. + 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 ]. +Proof. + 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. *) + (** [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 (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. -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. -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]. *) -(** 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. -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 principle on non-negative numbers using [Zlt]. *) -(** 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. + 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. + assumption. + firstorder. + unfold Zle, Zcompare in H; elim H; auto. + Defined. -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 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. -assumption. -firstorder. -unfold Zle, Zcompare in H; elim H; auto. -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. + exact Zlt_0_rec. + Qed. -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. -exact Zlt_0_rec. -Qed. + (** Obsolete version of [Zlt] induction principle on non-negative numbers *) -(** 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. + Proof. + intros P Hrec; apply Zlt_0_rec; auto. + Qed. -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. + exact Z_lt_rec. + 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. -exact Z_lt_rec. -Qed. + (** An even more general induction principle using [Zlt]. *) -(** 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. + Proof. + intros P z Hrec x. + assert (Hexpand : forall x, x = x - z + z). + intro; unfold Zminus; rewrite <- Zplus_assoc; rewrite Zplus_opp_l; + rewrite Zplus_0_r; trivial. + intro Hz. + rewrite (Hexpand x); pattern (x - z) in |- *; apply Zlt_0_rec. + 2: apply Zplus_le_reg_r with z; rewrite <- Hexpand; assumption. + intros x0 Hlt_x0 H. + apply Hrec. + 2: change z with (0+z); apply Zplus_le_compat_r; assumption. + intro y; rewrite (Hexpand y); intros. + destruct H0. + apply Hlt_x0. + split. + apply Zplus_le_reg_r with z; assumption. + apply Zplus_lt_reg_r with z; assumption. + Qed. -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. -assert (Hexpand : forall x, x = x - z + z). - intro; unfold Zminus; rewrite <- Zplus_assoc; rewrite Zplus_opp_l; - rewrite Zplus_0_r; trivial. -intro Hz. -rewrite (Hexpand x); pattern (x - z) in |- *; apply Zlt_0_rec. -2: apply Zplus_le_reg_r with z; rewrite <- Hexpand; assumption. -intros x0 Hlt_x0 H. -apply Hrec. - 2: change z with (0+z); apply Zplus_le_compat_r; assumption. - intro y; rewrite (Hexpand y); intros. -destruct H0. -apply Hlt_x0. -split. - apply Zplus_le_reg_r with z; assumption. - apply Zplus_lt_reg_r with z; assumption. -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. -exact Zlt_lower_bound_rec. -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. + exact Zlt_lower_bound_rec. + Qed. End Efficient_Rec. |