summaryrefslogtreecommitdiff
path: root/theories/ZArith/Wf_Z.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /theories/ZArith/Wf_Z.v
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/ZArith/Wf_Z.v')
-rw-r--r--theories/ZArith/Wf_Z.v355
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.