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/

Fcalc_digits.v 9.98 KB
Newer Older
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1
(**
2 3 4 5
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010 Sylvie Boldo
BOLDO Sylvie's avatar
BOLDO Sylvie committed
6
#<br />#
7 8 9 10 11 12 13 14 15 16 17 18 19
Copyright (C) 2010 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

20
(** * Functions for computing the number of digits of integers
21 22 23 24 25
      and related theorems. *)

Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
26
Require Import Fcore_digits.
27 28 29 30 31 32

Section Fcalc_digits.

Variable beta : radix.
Notation bpow e := (bpow beta e).

33
Notation digits := (Zdigits beta).
34 35 36 37 38 39 40 41 42 43

Theorem digits_abs :
  forall n, digits (Zabs n) = digits n.
Proof.
now intros [|n|n].
Qed.

Theorem digits_ln_beta :
  forall n,
  n <> Z0 ->
44
  digits n = ln_beta beta (Z2R n).
45 46
Proof.
intros n Hn.
47
destruct (ln_beta beta (Z2R n)) as (e, He) ; simpl.
48
specialize (He (Z2R_neq _ _ Hn)).
49
rewrite <- Z2R_abs in He.
50 51 52
assert (Hd := Zdigits_correct beta n).
assert (Hd' := Zdigits_gt_0 beta n).
apply Zle_antisym ; apply (bpow_lt_bpow beta).
53
apply Rle_lt_trans with (2 := proj2 He).
54 55
rewrite <- Z2R_Zpower by omega.
now apply Z2R_le.
56
apply Rle_lt_trans with (1 := proj1 He).
57 58
rewrite <- Z2R_Zpower by omega.
now apply Z2R_lt.
59 60
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
61 62 63 64 65 66 67
Theorem digits_ge_0 :
  forall n, (0 <= digits n)%Z.
Proof.
intros n.
destruct (Z_eq_dec n 0) as [H|H].
now rewrite H.
apply Zlt_le_weak.
68
now apply Zdigits_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
69 70
Qed.

71 72 73 74 75 76 77 78 79 80 81
Theorem ln_beta_F2R_digits :
  forall m e, m <> Z0 ->
  (ln_beta beta (F2R (Float beta m e)) = digits m + e :> Z)%Z.
Proof.
intros m e Hm.
rewrite ln_beta_F2R with (1 := Hm).
apply (f_equal (fun v => Zplus v e)).
apply sym_eq.
now apply digits_ln_beta.
Qed.

82 83 84
Theorem digits_shift :
  forall m e,
  m <> Z0 -> (0 <= e)%Z ->
85
  digits (m * Zpower beta e) = (digits m + e)%Z.
86 87
Proof.
intros m e Hm He.
88 89
rewrite <- ln_beta_F2R_digits with (1 := Hm).
rewrite digits_ln_beta.
90
rewrite Z2R_mult.
91
now rewrite Z2R_Zpower with (1 := He).
92 93 94 95 96 97 98 99
contradict Hm.
apply Zmult_integral_l with (2 := Hm).
apply neq_Z2R.
rewrite Z2R_Zpower with (1 := He).
apply Rgt_not_eq.
apply bpow_gt_0.
Qed.

100 101 102 103 104 105 106 107 108 109 110
Theorem digits_Zpower :
  forall e,
  (0 <= e)%Z ->
  digits (Zpower beta e) = (e + 1)%Z.
Proof.
intros e He.
rewrite <- (Zmult_1_l (Zpower beta e)).
rewrite digits_shift ; try easy.
apply Zplus_comm.
Qed.

111 112
Theorem digits_le :
  forall x y,
113
  (0 <= x)%Z -> (x <= y)%Z ->
114 115 116
  (digits x <= digits y)%Z.
Proof.
intros x y Hx Hxy.
117 118
case (Z_lt_le_dec 0 x).
clear Hx. intros Hx.
119
rewrite 2!digits_ln_beta.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
120 121
apply ln_beta_monotone.
now apply (Z2R_lt 0).
122
now apply Z2R_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
123 124 125
apply Zgt_not_eq.
now apply Zlt_le_trans with x.
now apply Zgt_not_eq.
126 127 128
intros Hx'.
rewrite (Zle_antisym _ _ Hx' Hx).
apply digits_ge_0.
129 130
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
131
Theorem lt_digits :
132
  forall x y,
133
  (0 <= y)%Z ->
134 135 136 137 138 139 140 141
  (digits x < digits y)%Z ->
  (x < y)%Z.
Proof.
intros x y Hy.
cut (y <= x -> digits y <= digits x)%Z. omega.
now apply digits_le.
Qed.

142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221
Theorem Zpower_le_digits :
  forall e x,
  (e < digits x)%Z ->
  (Zpower beta e <= Zabs x)%Z.
Proof.
intros [|e|e] x Hex.
(* *)
apply (Zlt_le_succ 0).
apply lt_digits.
apply Zabs_pos.
now rewrite digits_abs.
2: apply Zabs_pos.
(* *)
apply le_Z2R.
rewrite Z2R_Zpower. 2: easy.
assert (Zx: x <> Z0).
intros H.
apply Zlt_not_le with (1 := Hex).
now rewrite H.
revert Hex.
rewrite digits_ln_beta with (1 := Zx).
destruct (ln_beta beta (Z2R x)) as (ex, Ex).
unfold ln_beta_val.
specialize (Ex (Z2R_neq _ 0 Zx)).
intros Hex.
rewrite <- Z2R_abs in Ex.
apply Rle_trans with (2 := proj1 Ex).
apply bpow_le.
omega.
Qed.

Theorem digits_le_Zpower :
  forall e x,
  (Zabs x < Zpower beta e)%Z ->
  (digits x <= e)%Z.
Proof.
intros e x.
generalize (Zpower_le_digits e x).
omega.
Qed.

Theorem digits_gt_Zpower :
  forall e x,
  (Zpower beta e <= Zabs x)%Z ->
  (e < digits x)%Z.
Proof.
intros [|e|e] x Hex.
(* *)
apply Zlt_le_trans with 1%Z.
apply refl_equal.
rewrite <- digits_abs.
change 1%Z with (digits 1).
now apply digits_le.
(* *)
rewrite (Zpred_succ (Zpos e)).
apply Zlt_le_trans with (1 := Zlt_pred _).
unfold Zsucc.
rewrite <- digits_Zpower. 2: easy.
rewrite <- (digits_abs x).
apply digits_le with (2 := Hex).
apply le_Z2R.
rewrite Z2R_Zpower.
apply bpow_ge_0.
easy.
(* *)
apply Zlt_le_trans with Z0.
apply refl_equal.
apply digits_ge_0.
Qed.

Theorem Zpower_gt_digits :
  forall e x,
  (digits x <= e)%Z ->
  (Zabs x < Zpower beta e)%Z.
Proof.
intros e x Hex.
generalize (digits_gt_Zpower e x).
omega.
Qed.

222 223 224 225 226 227
(** 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.
*)

228 229
Theorem digits_mult_strong :
  forall x y,
230
  (0 <= x)%Z -> (0 <= y)%Z ->
231 232 233
  (digits (x + y + x * y) <= digits x + digits y)%Z.
Proof.
intros x y Hx Hy.
234 235 236 237 238
case (Z_lt_le_dec 0 x).
clear Hx. intros Hx.
case (Z_lt_le_dec 0 y).
clear Hy. intros Hy.
(* . *)
239 240 241 242 243 244 245
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!digits_ln_beta ; try now (apply sym_not_eq ; apply Zlt_not_eq).
246 247
apply ln_beta_le with (1 := Rgt_not_eq _ _ Hxy).
rewrite Rabs_pos_eq with (1 := Rlt_le _ _ Hxy).
248 249 250 251 252
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.
253
rewrite <- Z2R_mult.
254 255 256
apply Z2R_lt.
apply Zplus_lt_reg_r with (- (x + y + x * y + 1))%Z.
now ring_simplify.
257
rewrite bpow_plus.
258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
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.
277 278 279 280 281 282 283 284 285
(* . *)
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.
286 287
Qed.

288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304
Theorem digits_mult :
  forall x y,
  (digits (x * y) <= digits x + digits y)%Z.
Proof.
intros x y.
rewrite <- digits_abs.
rewrite <- (digits_abs x).
rewrite <- (digits_abs y).
apply Zle_trans with (digits (Zabs x + Zabs y + Zabs x * Zabs y)).
apply digits_le.
apply Zabs_pos.
rewrite Zabs_Zmult.
generalize (Zabs_pos x) (Zabs_pos y).
omega.
apply digits_mult_strong ; apply Zabs_pos.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321
Theorem digits_mult_ge :
  forall x y,
  (x <> 0)%Z -> (y <> 0)%Z ->
  (digits x + digits y - 1 <= digits (x * y))%Z.
Proof.
intros x y Zx Zy.
cut ((digits x - 1) + (digits y - 1) < digits (x * y))%Z. omega.
apply digits_gt_Zpower.
rewrite Zabs_Zmult.
rewrite Zpower_exp.
apply Zmult_le_compat.
apply Zpower_le_digits.
apply Zlt_pred.
apply Zpower_le_digits.
apply Zlt_pred.
apply Zpower_ge_0.
apply Zpower_ge_0.
322 323
generalize (Zdigits_gt_0 beta x). omega.
generalize (Zdigits_gt_0 beta y). omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
324 325
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411
Theorem digits_shr :
  forall m e,
  (0 <= m)%Z ->
  (0 <= e <= digits m)%Z ->
  digits (m / Zpower beta e) = (digits 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_digits.
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 digits_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_digits.
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_digits.
(* . *)
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_digits.
apply Zle_refl.
(* *)
revert He.
rewrite <- Hm'.
intros (H1, H2).
simpl.
now rewrite (Zle_antisym _ _ H2 H1).
Qed.

412
End Fcalc_digits.
413 414 415 416 417

Definition radix2 := Build_radix 2 (refl_equal _).

Theorem Z_of_nat_S_digits2_Pnat :
  forall m : positive,
418
  Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435
Proof.
intros m.
rewrite digits_ln_beta. 2: easy.
apply sym_eq.
apply ln_beta_unique.
generalize (digits2_Pnat m) (digits2_Pnat_correct m).
intros d H.
simpl in H.
replace (Z_of_nat (S d) - 1)%Z with (Z_of_nat d).
rewrite <- Z2R_abs.
rewrite <- 2!Z2R_Zpower_nat.
split.
now apply Z2R_le.
now apply Z2R_lt.
rewrite inj_S.
apply Zpred_succ.
Qed.
436 437

Notation digits := Zdigits (only parsing).