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/

Flocq_rnd_FLT.v 5.23 KB
Newer Older
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1 2
Require Import Flocq_Raux.
Require Import Flocq_defs.
3 4
Require Import Flocq_rnd_ex.
Require Import Flocq_rnd_generic.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
5
Require Import Flocq_float_prop.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
6
Require Import Flocq_rnd_FLX.
7
Require Import Flocq_rnd_FIX.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
8 9 10 11 12

Section RND_FLT.

Variable beta : radix.

13
Notation bpow e := (bpow beta e).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
14 15 16 17

Variable emin prec : Z.
Variable Hp : Zlt 0 prec.

18 19 20 21
(* floating-point format with gradual underflow *)
Definition FLT_format (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z /\ (emin <= Fexp f)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
22

23 24 25 26 27 28 29 30 31 32 33
Definition FLT_RoundingModeP (rnd : R -> R):=
  Rounding_for_Format FLT_format rnd.

Definition FLT_exp e := Zmax (e - prec) emin.

Theorem FLT_exp_correct : valid_exp FLT_exp.
Proof.
intros k.
unfold FLT_exp.
destruct (Zmax_spec (k - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
34
split.
35 36 37 38 39
generalize (Zmax_spec (k + 1 - prec) emin).
omega.
intros H0.
apply False_ind.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
40
split.
41 42
generalize (Zmax_spec (k + 1 - prec) emin).
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
43
split.
44 45 46 47 48 49 50 51
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
intros l H0.
generalize (Zmax_spec (l - prec) emin).
omega.
Qed.

Theorem FLT_format_generic :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
52
  forall x : R, FLT_format x <-> generic_format beta FLT_exp x.
53
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
54
split.
55
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
simpl in Hx2, Hx3.
unfold generic_format, canonic, FLT_exp.
destruct (ln_beta beta x) as (ex, Hx5).
simpl.
specialize (Hx5 Hx4).
destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2).
now eexists.
now rewrite <- Hx1.
rewrite Hx1, (F2R_change_exp beta emin).
now eexists.
exact Hx3.
(* . *)
74 75 76 77 78 79
intros ((xm, xe), (Hx1, Hx2)).
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 emin).
split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
80 81
simpl.
split.
82 83
apply Zpower_gt_0.
now apply Zlt_le_trans with (2 := radix_prop beta).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
84
now apply Zlt_le_weak.
85
apply Zle_refl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
86 87
rewrite Hx1.
eexists ; repeat split.
88
destruct (ln_beta beta x) as (ex, Hx4).
89
simpl in Hx2.
90
specialize (Hx4 Hx3).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
91
apply lt_Z2R.
92
rewrite Z2R_Zpower.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
93
apply Rmult_lt_reg_r with (bpow (ex - prec)).
94 95
apply bpow_gt_0.
rewrite <- bpow_add.
96 97 98 99 100 101
replace (prec + (ex - prec))%Z with ex by ring.
apply Rle_lt_trans with (Z2R (Zabs xm) * bpow xe)%R.
rewrite Hx2.
apply Rmult_le_compat_l.
apply (Z2R_le 0).
apply Zabs_pos.
102
apply -> bpow_le.
103 104 105 106 107 108 109 110
apply Zle_max_l.
replace (Z2R (Zabs xm) * bpow xe)%R with (Rabs x).
exact (proj2 Hx4).
rewrite Hx1.
apply abs_F2R.
now apply Zlt_le_weak.
rewrite Hx2.
apply Zle_max_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
111 112
Qed.

113 114 115 116
Theorem FLT_format_satisfies_any :
  satisfies_any FLT_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp _)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
117 118 119
intros x.
apply iff_sym.
apply FLT_format_generic.
120 121
exact FLT_exp_correct.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
122

Guillaume Melquiond's avatar
Guillaume Melquiond committed
123 124
Theorem FLT_format_FLX :
  forall x : R,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
125
  (bpow (emin + prec - 1) <= Rabs x)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
126 127 128 129 130 131 132 133 134 135 136 137 138
  ( FLT_format x <-> FLX_format beta prec x ).
Proof.
intros x Hx1.
split.
(* . *)
intros ((xm, xe), (Hx2, (Hx3, Hx4))).
rewrite Hx2.
eexists ; split ; easy.
(* . *)
intros Hx2.
destruct (Req_dec x 0) as [Hx3|Hx3].
(* . . *)
rewrite Hx3.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
139
apply <- FLT_format_generic.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
140
apply generic_format_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
141
(* . . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
142 143
destruct (proj1 (FLX_format_generic _ _ Hp x) Hx2) as ((xm, xe), (Hx4, Hx5)).
apply <- FLT_format_generic.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
144 145 146 147
rewrite Hx4.
eexists ; repeat split.
rewrite Hx5. clear Hx5.
rewrite <- Hx4.
148
destruct (ln_beta beta x) as (ex, Hx5).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
149 150 151 152 153
unfold FLX_exp, FLT_exp.
simpl.
apply sym_eq.
apply Zmax_left.
cut (emin + prec <= ex)%Z. omega.
154
apply bpow_lt_bpow with beta.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
155
apply Rle_lt_trans with (1 := Hx1).
156
now apply Hx5.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
157 158
Qed.

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
(* TODO: vérifier si ça implique ^^ *)
Theorem FLT_canonic_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  forall f : float beta,
  ( canonic beta FLT_exp x f <-> canonic beta (FLX_exp prec) x f ).
Proof.
intros x Hx f.
unfold canonic.
replace (FLT_exp (projT1 (ln_beta beta x))) with (FLX_exp prec (projT1 (ln_beta beta x))).
apply iff_refl.
unfold FLX_exp, FLT_exp.
apply sym_eq.
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
simpl.
assert (emin + prec - 1 < ex)%Z. 2: omega.
apply <- (bpow_lt beta).
apply Rle_lt_trans with (1 := Hx).
apply He.
intros H.
elim Rlt_not_le with (2 := Hx).
rewrite H, Rabs_R0.
apply bpow_gt_0.
Qed.

185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
Theorem FLT_format_FIX :
  forall x,
  (Rabs x <= bpow (emin + prec))%R ->
  ( FLT_format x <-> FIX_format beta emin x ).
Proof.
intros x Hx.
split.
(* . *)
intros ((xm, xe), (H1, (H2, H3))).
rewrite H1, (F2R_change_exp beta emin).
now eexists.
exact H3.
(* . *)
destruct Hx as [Hx|Hx].
(* . . *)
intros ((xm, xe), (H1, H2)).
rewrite H1.
eexists ; repeat split.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply Rmult_lt_reg_r with (bpow xe).
206
apply bpow_gt_0.
207 208
rewrite H1, abs_F2R in Hx.
apply Rlt_le_trans with (1 := Hx).
209 210
rewrite <- bpow_add.
apply -> bpow_le.
211 212 213 214 215 216 217 218 219 220
rewrite Zplus_comm, <- H2.
apply Zle_refl.
now apply Zlt_le_weak.
now apply Zeq_le.
(* . . *)
assert (Ha: forall x, FLT_format (Rabs x) -> FLT_format x).
clear.
intros x Ha.
unfold Rabs in Ha.
destruct (Rcase_abs x) as [Hx|Hx].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
221
apply <- FLT_format_generic.
222 223
rewrite <- (Ropp_involutive x).
apply generic_format_sym.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
224
now apply -> FLT_format_generic.
225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
exact Ha.
(* . . *)
intros _.
apply Ha.
rewrite Hx.
exists (Float beta 1 (emin + prec)).
split.
apply sym_eq.
apply Rmult_1_l.
simpl.
split.
now apply Zpower_gt_1.
omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
240
End RND_FLT.