Commit 1c6b24aa authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make Zdigits <-> Zpower theorems axiom-free.

parent e5020120
......@@ -60,80 +60,6 @@ apply sym_eq.
now apply Zdigits_ln_beta.
Qed.
Theorem Zdigits_le :
forall x y,
(0 <= x)%Z -> (x <= y)%Z ->
(Zdigits beta x <= Zdigits beta y)%Z.
Proof.
intros x y Hx Hxy.
case (Z_lt_le_dec 0 x).
clear Hx. intros Hx.
rewrite 2!Zdigits_ln_beta.
apply ln_beta_le.
now apply (Z2R_lt 0).
now apply Z2R_le.
apply Zgt_not_eq.
now apply Zlt_le_trans with x.
now apply Zgt_not_eq.
intros Hx'.
rewrite (Zle_antisym _ _ Hx' Hx).
apply Zdigits_ge_0.
Qed.
Theorem lt_Zdigits :
forall x y,
(0 <= y)%Z ->
(Zdigits beta x < Zdigits beta y)%Z ->
(x < y)%Z.
Proof.
intros x y Hy.
cut (y <= x -> Zdigits beta y <= Zdigits beta x)%Z. omega.
now apply Zdigits_le.
Qed.
Theorem Zpower_le_Zdigits :
forall e x,
(e < Zdigits beta x)%Z ->
(Zpower beta e <= Zabs x)%Z.
Proof.
intros e x Hex.
destruct (Zdigits_correct beta x) as (H1,H2).
apply Zle_trans with (2 := H1).
apply Zpower_le.
clear -Hex ; omega.
Qed.
Theorem Zdigits_le_Zpower :
forall e x,
(Zabs x < Zpower beta e)%Z ->
(Zdigits beta x <= e)%Z.
Proof.
intros e x.
generalize (Zpower_le_Zdigits e x).
omega.
Qed.
Theorem Zpower_gt_Zdigits :
forall e x,
(Zdigits beta x <= e)%Z ->
(Zabs x < Zpower beta e)%Z.
Proof.
intros e x Hex.
destruct (Zdigits_correct beta x) as (H1,H2).
apply Zlt_le_trans with (1 := H2).
now apply Zpower_le.
Qed.
Theorem Zdigits_gt_Zpower :
forall e x,
(Zpower beta e <= Zabs x)%Z ->
(e < Zdigits beta x)%Z.
Proof.
intros e x Hex.
generalize (Zpower_gt_Zdigits e x).
omega.
Qed.
(** Characterizes the number digits of a product.
This strong version is needed for proofs of division and square root
......
......@@ -946,4 +946,70 @@ rewrite Zdigits_mult_Zpower ; try easy.
apply Zplus_comm.
Qed.
Theorem Zdigits_le :
forall x y,
(0 <= x)%Z -> (x <= y)%Z ->
(Zdigits x <= Zdigits y)%Z.
Proof.
intros x y Zx Hxy.
assert (Hx := Zdigits_correct x).
assert (Hy := Zdigits_correct y).
apply (Zpower_lt_Zpower beta).
zify ; omega.
Qed.
Theorem lt_Zdigits :
forall x y,
(0 <= y)%Z ->
(Zdigits x < Zdigits y)%Z ->
(x < y)%Z.
Proof.
intros x y Hy.
cut (y <= x -> Zdigits y <= Zdigits x)%Z. omega.
now apply Zdigits_le.
Qed.
Theorem Zpower_le_Zdigits :
forall e x,
(e < Zdigits x)%Z ->
(Zpower beta e <= Zabs x)%Z.
Proof.
intros e x Hex.
destruct (Zdigits_correct x) as [H1 H2].
apply Zle_trans with (2 := H1).
apply Zpower_le.
clear -Hex ; omega.
Qed.
Theorem Zdigits_le_Zpower :
forall e x,
(Zabs x < Zpower beta e)%Z ->
(Zdigits x <= e)%Z.
Proof.
intros e x.
generalize (Zpower_le_Zdigits e x).
omega.
Qed.
Theorem Zpower_gt_Zdigits :
forall e x,
(Zdigits x <= e)%Z ->
(Zabs x < Zpower beta e)%Z.
Proof.
intros e x Hex.
destruct (Zdigits_correct x) as [H1 H2].
apply Zlt_le_trans with (1 := H2).
now apply Zpower_le.
Qed.
Theorem Zdigits_gt_Zpower :
forall e x,
(Zpower beta e <= Zabs x)%Z ->
(e < Zdigits x)%Z.
Proof.
intros e x Hex.
generalize (Zpower_gt_Zdigits e x).
omega.
Qed.
End Fcore_digits.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment