Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit bccf8968 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make Zdigits_mult_strong and Zdigits_div_Zpower axiom-free.

parent 1c6b24aa
......@@ -60,196 +60,6 @@ apply sym_eq.
now apply Zdigits_ln_beta.
Qed.
(** Characterizes the number digits of a product.
This strong version is needed for proofs of division and square root
algorithms, since they involve operation remainders.
*)
Theorem Zdigits_mult_strong :
forall x y,
(0 <= x)%Z -> (0 <= y)%Z ->
(Zdigits beta (x + y + x * y) <= Zdigits beta x + Zdigits beta y)%Z.
Proof.
intros x y Hx Hy.
case (Z_lt_le_dec 0 x).
clear Hx. intros Hx.
case (Z_lt_le_dec 0 y).
clear Hy. intros Hy.
(* . *)
assert (Hxy: (0 < Z2R (x + y + x * y))%R).
apply (Z2R_lt 0).
change Z0 with (0 + 0 + 0)%Z.
apply Zplus_lt_compat.
now apply Zplus_lt_compat.
now apply Zmult_lt_0_compat.
rewrite 3!Zdigits_ln_beta ; try now (apply sym_not_eq ; apply Zlt_not_eq).
apply ln_beta_le_bpow with (1 := Rgt_not_eq _ _ Hxy).
rewrite Rabs_pos_eq with (1 := Rlt_le _ _ Hxy).
destruct (ln_beta beta (Z2R x)) as (ex, Hex). simpl.
specialize (Hex (Rgt_not_eq _ _ (Z2R_lt _ _ Hx))).
destruct (ln_beta beta (Z2R y)) as (ey, Hey). simpl.
specialize (Hey (Rgt_not_eq _ _ (Z2R_lt _ _ Hy))).
apply Rlt_le_trans with (Z2R (x + 1) * Z2R (y + 1))%R.
rewrite <- Z2R_mult.
apply Z2R_lt.
apply Zplus_lt_reg_r with (- (x + y + x * y + 1))%Z.
now ring_simplify.
rewrite bpow_plus.
apply Rmult_le_compat ; try (apply (Z2R_le 0) ; omega).
rewrite <- (Rmult_1_r (Z2R (x + 1))).
change (F2R (Float beta (x + 1) 0) <= bpow ex)%R.
apply F2R_p1_le_bpow.
exact Hx.
unfold F2R. rewrite Rmult_1_r.
apply Rle_lt_trans with (Rabs (Z2R x)).
apply RRle_abs.
apply Hex.
rewrite <- (Rmult_1_r (Z2R (y + 1))).
change (F2R (Float beta (y + 1) 0) <= bpow ey)%R.
apply F2R_p1_le_bpow.
exact Hy.
unfold F2R. rewrite Rmult_1_r.
apply Rle_lt_trans with (Rabs (Z2R y)).
apply RRle_abs.
apply Hey.
apply neq_Z2R.
now apply Rgt_not_eq.
(* . *)
intros Hy'.
rewrite (Zle_antisym _ _ Hy' Hy).
rewrite Zmult_0_r, 3!Zplus_0_r.
apply Zle_refl.
intros Hx'.
rewrite (Zle_antisym _ _ Hx' Hx).
rewrite Zmult_0_l, Zplus_0_r, 2!Zplus_0_l.
apply Zle_refl.
Qed.
Theorem Zdigits_mult :
forall x y,
(Zdigits beta (x * y) <= Zdigits beta x + Zdigits beta y)%Z.
Proof.
intros x y.
rewrite <- Zdigits_abs.
rewrite <- (Zdigits_abs _ x).
rewrite <- (Zdigits_abs _ y).
apply Zle_trans with (Zdigits beta (Zabs x + Zabs y + Zabs x * Zabs y)).
apply Zdigits_le.
apply Zabs_pos.
rewrite Zabs_Zmult.
generalize (Zabs_pos x) (Zabs_pos y).
omega.
apply Zdigits_mult_strong ; apply Zabs_pos.
Qed.
Theorem Zdigits_mult_ge :
forall x y,
(x <> 0)%Z -> (y <> 0)%Z ->
(Zdigits beta x + Zdigits beta y - 1 <= Zdigits beta (x * y))%Z.
Proof.
intros x y Zx Zy.
cut ((Zdigits beta x - 1) + (Zdigits beta y - 1) < Zdigits beta (x * y))%Z. omega.
apply Zdigits_gt_Zpower.
rewrite Zabs_Zmult.
rewrite Zpower_exp.
apply Zmult_le_compat.
apply Zpower_le_Zdigits.
apply Zlt_pred.
apply Zpower_le_Zdigits.
apply Zlt_pred.
apply Zpower_ge_0.
apply Zpower_ge_0.
generalize (Zdigits_gt_0 beta x). omega.
generalize (Zdigits_gt_0 beta y). omega.
Qed.
Theorem Zdigits_div_Zpower :
forall m e,
(0 <= m)%Z ->
(0 <= e <= Zdigits beta m)%Z ->
Zdigits beta (m / Zpower beta e) = (Zdigits beta m - e)%Z.
Proof.
intros m e Hm He.
destruct (Zle_lt_or_eq 0 m Hm) as [Hm'|Hm'].
(* *)
destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He'].
(* . *)
unfold Zminus.
rewrite <- ln_beta_F2R_Zdigits.
2: now apply Zgt_not_eq.
assert (Hp: (0 < Zpower beta e)%Z).
apply lt_Z2R.
rewrite Z2R_Zpower with (1 := proj1 He).
apply bpow_gt_0.
rewrite Zdigits_ln_beta.
rewrite <- Zfloor_div with (1 := Zgt_not_eq _ _ Hp).
rewrite Z2R_Zpower with (1 := proj1 He).
unfold Rdiv.
rewrite <- bpow_opp.
change (Z2R m * bpow (-e))%R with (F2R (Float beta m (-e))).
destruct (ln_beta beta (F2R (Float beta m (-e)))) as (e', E').
simpl.
specialize (E' (Rgt_not_eq _ _ (F2R_gt_0_compat beta (Float beta m (-e)) Hm'))).
apply ln_beta_unique.
rewrite Rabs_pos_eq in E'.
2: now apply F2R_ge_0_compat.
rewrite Rabs_pos_eq.
split.
assert (H': (0 <= e' - 1)%Z).
(* .. *)
cut (1 <= e')%Z. omega.
apply bpow_lt_bpow with beta.
apply Rle_lt_trans with (2 := proj2 E').
simpl.
rewrite <- (Rinv_r (bpow e)).
rewrite <- bpow_opp.
unfold F2R. simpl.
apply Rmult_le_compat_r.
apply bpow_ge_0.
rewrite <- Z2R_Zpower with (1 := proj1 He).
apply Z2R_le.
rewrite <- Zabs_eq with (1 := Hm).
now apply Zpower_le_Zdigits.
apply Rgt_not_eq.
apply bpow_gt_0.
(* .. *)
rewrite <- Z2R_Zpower with (1 := H').
apply Z2R_le.
apply Zfloor_lub.
rewrite Z2R_Zpower with (1 := H').
apply E'.
apply Rle_lt_trans with (2 := proj2 E').
apply Zfloor_lb.
apply (Z2R_le 0).
apply Zfloor_lub.
now apply F2R_ge_0_compat.
apply Zgt_not_eq.
apply Zlt_le_trans with (beta^e / beta^e)%Z.
rewrite Z_div_same_full.
apply refl_equal.
now apply Zgt_not_eq.
apply Z_div_le.
now apply Zlt_gt.
rewrite <- Zabs_eq with (1 := Hm).
now apply Zpower_le_Zdigits.
(* . *)
unfold Zminus.
rewrite He', Zplus_opp_r.
rewrite Zdiv_small.
apply refl_equal.
apply conj with (1 := Hm).
pattern m at 1 ; rewrite <- Zabs_eq with (1 := Hm).
apply Zpower_gt_Zdigits.
apply Zle_refl.
(* *)
revert He.
rewrite <- Hm'.
intros (H1, H2).
simpl.
now rewrite (Zle_antisym _ _ H2 H1).
Qed.
End Fcalc_digits.
Definition radix2 := Build_radix 2 (refl_equal _).
......
......@@ -1012,4 +1012,117 @@ 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
algorithms, since they involve operation remainders.
*)
Theorem Zdigits_mult_strong :
forall x y,
(0 <= x)%Z -> (0 <= y)%Z ->
(Zdigits (x + y + x * y) <= Zdigits x + Zdigits y)%Z.
Proof.
intros x y Hx Hy.
apply Zdigits_le_Zpower.
rewrite Zabs_eq.
apply Zlt_le_trans with ((x + 1) * (y + 1))%Z.
ring_simplify.
apply Zle_lt_succ, Zle_refl.
rewrite Zpower_plus by apply Zdigits_ge_0.
apply Zmult_le_compat.
apply Zlt_le_succ.
rewrite <- (Zabs_eq x) at 1 by easy.
apply Zdigits_correct.
apply Zlt_le_succ.
rewrite <- (Zabs_eq y) at 1 by easy.
apply Zdigits_correct.
clear -Hx ; omega.
clear -Hy ; omega.
change Z0 with (0 + 0 + 0)%Z.
apply Zplus_le_compat.
now apply Zplus_le_compat.
now apply Zmult_le_0_compat.
Qed.
Theorem Zdigits_mult :
forall x y,
(Zdigits (x * y) <= Zdigits x + Zdigits y)%Z.
Proof.
intros x y.
rewrite <- Zdigits_abs.
rewrite <- (Zdigits_abs x).
rewrite <- (Zdigits_abs y).
apply Zle_trans with (Zdigits (Zabs x + Zabs y + Zabs x * Zabs y)).
apply Zdigits_le.
apply Zabs_pos.
rewrite Zabs_Zmult.
generalize (Zabs_pos x) (Zabs_pos y).
omega.
apply Zdigits_mult_strong ; apply Zabs_pos.
Qed.
Theorem Zdigits_mult_ge :
forall x y,
(x <> 0)%Z -> (y <> 0)%Z ->
(Zdigits x + Zdigits y - 1 <= Zdigits (x * y))%Z.
Proof.
intros x y Zx Zy.
cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. omega.
apply Zdigits_gt_Zpower.
rewrite Zabs_Zmult.
rewrite Zpower_exp.
apply Zmult_le_compat.
apply Zpower_le_Zdigits.
apply Zlt_pred.
apply Zpower_le_Zdigits.
apply Zlt_pred.
apply Zpower_ge_0.
apply Zpower_ge_0.
generalize (Zdigits_gt_0 x). omega.
generalize (Zdigits_gt_0 y). omega.
Qed.
Theorem Zdigits_div_Zpower :
forall m e,
(0 <= m)%Z ->
(0 <= e <= Zdigits m)%Z ->
Zdigits (m / Zpower beta e) = (Zdigits m - e)%Z.
Proof.
intros m e Hm He.
assert (H := Zdigits_correct m).
apply Zdigits_unique.
destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He'].
rewrite Zabs_eq in H by easy.
destruct H as [H1 H2].
rewrite Zabs_eq.
split.
replace (Zdigits m - e - 1)%Z with (Zdigits m - 1 - e)%Z by ring.
rewrite Z.pow_sub_r.
2: apply Zgt_not_eq, radix_gt_0.
2: clear -He He' ; omega.
apply Z_div_le with (2 := H1).
now apply Zlt_gt, Zpower_gt_0.
apply Zmult_lt_reg_r with (Zpower beta e).
now apply Zpower_gt_0.
apply Zle_lt_trans with m.
rewrite Zmult_comm.
apply Z_mult_div_ge.
now apply Zlt_gt, Zpower_gt_0.
rewrite <- Zpower_plus.
now replace (Zdigits m - e + e)%Z with (Zdigits m) by ring.
now apply Zle_minus_le_0.
apply He.
apply Z_div_pos with (2 := Hm).
now apply Zlt_gt, Zpower_gt_0.
rewrite He'.
rewrite (Zeq_minus _ (Zdigits m)) by reflexivity.
simpl.
rewrite Zdiv_small.
easy.
split.
exact Hm.
now rewrite <- (Zabs_eq m) at 1.
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