Missing_theos.v 86.1 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2016-2018 Sylvie Boldo
#<br />#
Copyright (C) 2016-2018 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.
*)

BOLDO Sylvie's avatar
BOLDO Sylvie committed
20
Require Import Psatz.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
21

22
From Flocq Require Import Core Plus_error Mult_error Operations Sterbenz.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
23
From Flocq Require Import Pff Ftranslate_flocq2Pff.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
24 25 26

Open Scope R_scope.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
27 28
Section FTS.
Variable emin prec : Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
29
Variable choice : Z -> bool.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
30 31 32
Hypothesis precisionNotZero : (1 < prec)%Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Hypothesis emin_neg: (emin <= 0)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
33 34 35
Hypothesis choice_sym: forall x, choice x  = negb (choice (- (x + 1))).


BOLDO Sylvie's avatar
BOLDO Sylvie committed
36 37

Notation format := (generic_format radix2 (FLT_exp emin prec)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
38
Notation round_flt :=(round radix2 (FLT_exp emin prec) (Znearest choice)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
39 40
Notation bpow e := (bpow radix2 e).

BOLDO Sylvie's avatar
BOLDO Sylvie committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54

Lemma round_N_opp_sym: forall x, round_flt (- x) =
       - round_flt x.
Proof.
intros x; unfold round; rewrite <- F2R_Zopp.
rewrite cexp_opp; f_equal; f_equal.
rewrite scaled_mantissa_opp.
rewrite Znearest_opp.
generalize (scaled_mantissa radix2 (FLT_exp emin prec) x).
intros z; unfold Znearest; case (Rcompare _); try easy.
now rewrite <- choice_sym.
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
55 56 57 58 59 60 61
(** inputs *)
Variable x y:R.
Hypothesis Fx: format x.
Hypothesis Fy: format y.

(** algorithm *)
Let a := round_flt (x+y).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
62
Let b := round_flt (y+round_flt (x-a)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
63 64

(** Theorem *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
65
Theorem Fast2Sum_correct: Rabs y <= Rabs x -> a+b=x+y.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
66 67 68 69 70 71 72 73 74 75 76 77 78 79
Proof with auto with typeclass_instances.
intros H.
(* *)
destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
   prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero x)
  as (fx,(Hfx,Hfx')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
   prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero y)
  as (fy,(Hfy,Hfy')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
(* *)
80 81
pose (Iplus := fun (f g:Pff.float) => RND_Closest
        (make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
BOLDO Sylvie's avatar
BOLDO Sylvie committed
82
         (FtoR radix2 f + FtoR radix2 g)).
83 84
pose (Iminus := fun (f g:Pff.float) => RND_Closest
        (make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
BOLDO Sylvie's avatar
BOLDO Sylvie committed
85
         (FtoR radix2 f - FtoR radix2 g)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
86
assert (H1: forall x y, FtoR 2 (Iplus x y) = round_flt (FtoR 2 x + FtoR 2 y)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
87 88 89 90 91 92 93 94 95
clear -prec_gt_0_ precisionNotZero emin_neg; intros x y.
unfold Iplus.
apply trans_eq with (round radix2
  (FLT_exp (- dExp (make_bound radix2 prec emin)) prec)
  (Znearest choice) (FtoR radix2 x + FtoR radix2 y)).
apply pff_round_N_is_round; try assumption.
now apply make_bound_p.
rewrite make_bound_Emin; try assumption.
now rewrite Zopp_involutive.
96
assert (H2: forall x y, FtoR 2 (Iminus x y) = round_flt (FtoR 2 x - FtoR 2 y)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
97 98 99 100 101 102 103 104 105
clear -prec_gt_0_ precisionNotZero emin_neg; intros x y.
unfold Iminus.
apply trans_eq with (round radix2
  (FLT_exp (- dExp (make_bound radix2 prec emin)) prec)
  (Znearest choice) (FtoR radix2 x - FtoR radix2 y)).
apply pff_round_N_is_round; try assumption.
now apply make_bound_p.
rewrite make_bound_Emin; try assumption.
now rewrite Zopp_involutive.
106
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
107 108
assert (K: FtoR 2 (Iminus fy (Iminus (Iplus fx fy) fx)) =
       FtoR 2 fx + FtoR 2 fy - FtoR 2 (Iplus fx fy)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
109
apply Pff.Dekker_FTS with (make_bound radix2 prec emin) (Zabs_nat prec); try assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
110 111 112
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
113 114
(* . *)
intros p q Fp Fq.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
115 116
apply RND_Closest_correct.
apply Nat2Z.inj_lt.
117 118 119 120 121 122
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
(* . *)
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
123 124
apply sym_not_eq, Nat.lt_neq.
apply lt_Zlt_inv.
125 126 127
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
apply FcanonicFopp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
128 129
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
130 131
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
132 133
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
134 135
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
136 137
rewrite Fopp_correct, 2!H1, 2!Fopp_correct, <- Ropp_plus_distr.
now rewrite round_N_opp_sym.
138 139 140 141
(* . *)
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
142
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
143 144
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
145 146
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
147 148
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
149 150
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
151 152 153 154 155 156
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
rewrite H1,H2.
rewrite Fopp_correct.
f_equal; ring.
(* . *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
157
unfold Pff.FtoRradix.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
158 159
change 2%Z with (radix_val radix2).
rewrite Hfx, Hfy; assumption.
160 161 162 163 164 165 166
(* *)
generalize K; rewrite 2!H2, H1.
change 2%Z with (radix_val radix2).
rewrite Hfx, Hfy; fold a; unfold b; intros K'.
apply Rplus_eq_reg_r with (-a).
apply trans_eq with (round_flt (y - round_flt (a - x))).
2: rewrite K'; ring.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
167 168
ring_simplify; f_equal; unfold Rminus; f_equal.
rewrite <- round_N_opp_sym.
169 170
f_equal; ring.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
171

172
End FTS.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
173

174
Section TS.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
175

176
Variable emin prec : Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
177
Variable choice : Z -> bool.
178 179 180
Hypothesis precisionNotZero : (1 < prec)%Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Hypothesis emin_neg: (emin <= 0)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
181
Hypothesis choice_sym: forall x, choice x  = negb (choice (- (x + 1))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
182

183
Notation format := (generic_format radix2 (FLT_exp emin prec)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
184
Notation round_flt :=(round radix2 (FLT_exp emin prec) (Znearest choice)).
185
Notation bpow e := (bpow radix2 e).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
186

187 188 189 190
(** inputs *)
Variable x y:R.
Hypothesis Fx: format x.
Hypothesis Fy: format y.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
191

192 193 194 195 196 197
(** algorithm *)
Let a  := round_flt (x+y).
Let x' := round_flt (a-x).
Let dx := round_flt (x- round_flt (a-x')).
Let dy := round_flt (y - x').
Let b  := round_flt (dx + dy).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
198

199
(** Theorem *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
200
Theorem TwoSum_correct: a+b=x+y.
201
Proof with auto with typeclass_instances.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
202
(* *)
203 204 205 206 207 208 209 210 211 212
destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
   prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero x)
  as (fx,(Hfx,Hfx')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
   prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero y)
  as (fy,(Hfy,Hfy')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
213
(* *)
214 215
pose (Iplus := fun (f g:Pff.float) => RND_Closest
        (make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
BOLDO Sylvie's avatar
BOLDO Sylvie committed
216
         (FtoR radix2 f + FtoR radix2 g)).
217 218
pose (Iminus := fun (f g:Pff.float) => RND_Closest
        (make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
BOLDO Sylvie's avatar
BOLDO Sylvie committed
219
         (FtoR radix2 f - FtoR radix2 g)).
220
assert (H1: forall x y, FtoR 2 (Iplus x y) = round_flt (FtoR 2 x + FtoR 2 y)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
221 222 223 224 225 226 227 228 229
clear -prec_gt_0_ precisionNotZero emin_neg; intros x y.
unfold Iplus.
apply trans_eq with (round radix2
  (FLT_exp (- dExp (make_bound radix2 prec emin)) prec)
  (Znearest choice) (FtoR radix2 x + FtoR radix2 y)).
apply pff_round_N_is_round; try assumption.
now apply make_bound_p.
rewrite make_bound_Emin; try assumption.
now rewrite Zopp_involutive.
230
assert (H2: forall x y, FtoR 2 (Iminus x y) = round_flt (FtoR 2 x - FtoR 2 y)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
231 232 233 234 235 236 237 238 239
clear -prec_gt_0_ precisionNotZero emin_neg; intros x y.
unfold Iminus.
apply trans_eq with (round radix2
  (FLT_exp (- dExp (make_bound radix2 prec emin)) prec)
  (Znearest choice) (FtoR radix2 x - FtoR radix2 y)).
apply pff_round_N_is_round; try assumption.
now apply make_bound_p.
rewrite make_bound_Emin; try assumption.
now rewrite Zopp_involutive.
240 241 242 243 244 245 246 247 248 249
(* *)
assert (K: FtoR 2 (Iplus (Iminus fx (Iminus (Iplus fx fy) (Iminus (Iplus fx fy) fx)))
            (Iminus fy (Iminus (Iplus fx fy) fx))) =
       FtoR 2 fx + FtoR 2 fy - FtoR 2 (Iplus fx fy)).
apply Knuth with (make_bound radix2 prec emin) (Zabs_nat prec); try assumption.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
(* . *)
intros p q Fp Fq.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
250 251
apply RND_Closest_correct.
apply Nat2Z.inj_lt.
252 253 254
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
(* . *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
255
unfold FtoRradix.
256 257 258 259 260 261
intros p q r s Fp Fq Fr Fs M1 M2.
now rewrite 2!H1, M1, M2.
(* . *)
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
262
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
263 264
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
265 266
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
267 268
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
269 270
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
271 272
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
273
now rewrite 2!H1, Rplus_comm.
274 275 276 277
(* . *)
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
278
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
279 280 281
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
apply FcanonicFopp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
282 283
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
284 285
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
286 287
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
288 289
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
290 291
rewrite Fopp_correct, 2!H1, 2!Fopp_correct, <- Ropp_plus_distr.
now rewrite round_N_opp_sym.
292 293 294 295
(* . *)
intros p q.
apply FcanonicUnique with radix2 (make_bound radix2 prec emin) (Zabs_nat prec).
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
296
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
297 298
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
299 300
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
301 302
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
303 304
apply RND_Closest_canonic.
apply Nat2Z.inj_lt.
305 306
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
307
rewrite H1, H2, Fopp_correct.
308 309 310 311 312 313 314 315
f_equal; ring.
(* *)
generalize K; rewrite 2!H1, 5!H2, H1.
change 2%Z with (radix_val radix2).
rewrite Hfx, Hfy.
fold a; fold x'; fold dx; fold dy; fold b.
intros K'; rewrite K'; ring.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
316 317


318
End TS.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
319 320 321 322




323 324 325 326
Section Veltkamp.

Variable beta : radix.
Variable emin prec : Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
327
Variable choice : Z -> bool.
328 329 330 331 332 333
Variable s:Z.
Hypothesis precisionGe3 : (3 <= prec)%Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Hypothesis emin_neg: (emin <= 0)%Z.

Notation format := (generic_format beta (FLT_exp emin prec)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
334 335
Notation round_flt :=(round beta (FLT_exp emin prec) (Znearest choice)).
Notation round_flt_s :=(round beta (FLT_exp emin (prec-s)) (Znearest choice)).
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356
Notation ulp_flt :=(ulp beta (FLT_exp emin prec)).
Notation bpow e := (bpow beta e).

(** inputs *)
Hypothesis SLe: (2 <= s)%Z.
Hypothesis SGe: (s <= prec-2)%Z.
Variable x:R.
Hypothesis Fx: format x.

(** algorithm *)
Let p := round_flt (x*(bpow s+1)).
Let q:= round_flt (x-p).
Let hx:=round_flt (q+p).
Let tx:=round_flt (x-hx).


(** Theorems *)

Lemma C_format: format (bpow s +1).
Proof with auto with typeclass_instances.
apply generic_format_FLT.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
357
exists (Defs.Float beta (Zpower beta s+1)%Z 0%Z); simpl.
358
unfold F2R; simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
359
rewrite plus_IZR, IZR_Zpower; try omega.
360 361 362 363 364 365 366 367 368 369 370
simpl; ring.
rewrite Zabs_eq.
apply Zle_lt_trans with (beta^s+beta^0)%Z.
simpl; omega.
apply Zle_lt_trans with (beta^s+beta^s)%Z.
apply Zplus_le_compat_l.
apply Zpower_le; omega.
apply Zle_lt_trans with (2*beta^s)%Z.
omega.
apply Zle_lt_trans with (beta^1*beta^s)%Z.
apply Zmult_le_compat_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
371
rewrite Z.pow_1_r.
372 373 374 375 376 377
apply Zle_bool_imp_le; apply beta.
apply Zpower_ge_0.
rewrite <- Zpower_plus; try omega.
apply Zpower_lt; omega.
apply Zle_trans with (beta^s)%Z; try omega.
apply Zpower_ge_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
378
assumption.
379 380 381
Qed.


382
Theorem Veltkamp_Even:
383
  (choice = fun z => negb (Z.even z)) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
384
   hx = round_flt_s x.
385
Proof with auto with typeclass_instances.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
386
intros Hchoice.
387
assert (precisionNotZero : (1 < prec)%Z) by omega.
388 389 390 391 392 393
destruct (format_is_pff_format beta (make_bound beta prec emin)
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x)
  as (fx,(Hfx,Hfx')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
394
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
395 396 397 398 399
  (x*(bpow s+1)))
  as (fp,(Hfp, (Hfp',Hfp''))).
rewrite make_bound_Emin in Hfp''; try assumption.
replace (--emin)%Z with emin in Hfp'' by omega.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
400
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
401 402 403 404 405
  (x-p))
  as (fq,(Hfq, (Hfq',Hfq''))).
rewrite make_bound_Emin in Hfq''; try assumption.
replace (--emin)%Z with emin in Hfq'' by omega.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
406
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
407 408 409 410 411
  (q+p))
  as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
(* *)
412
destruct VeltkampEven with beta (make_bound beta prec emin) (Zabs_nat s)
413 414 415 416 417 418 419 420 421
   (Zabs_nat prec) fx fp fq fhx as (hx', (H1,H2)); try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
replace 2%nat with (Zabs_nat 2) by easy.
apply Zabs_nat_le; omega.
apply Nat2Z.inj_le.
rewrite inj_abs; try omega.
rewrite inj_minus, Zmax_r; rewrite inj_abs; simpl; omega.
rewrite Hfx; rewrite inj_abs; try omega.
422
rewrite bpow_powerRZ in Hfp'; exact Hfp'.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
423 424
rewrite Hfx, Hfp'', <- Hchoice; assumption.
rewrite Hfp'', Hfq'', <- Hchoice; assumption.
425
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
426
unfold hx; rewrite Hchoice, <- Hfhx'', <- H1.
427
apply trans_eq with (FtoR beta (RND_EvenClosest
428
 (make_bound beta (prec-s) emin) beta (Zabs_nat (prec-s)) x)).
429
generalize (EvenClosestUniqueP (make_bound beta (prec-s) emin) beta
430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454
   (Zabs_nat (prec-s))); unfold UniqueP; intros T.
apply T with x; clear T.
apply radix_gt_1.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
rewrite <- Hfx.
replace (Zabs_nat (prec-s)) with (Zabs_nat prec - Zabs_nat s)%nat.
replace (make_bound beta (prec - s) emin) with
  (Bound  (Pos.of_succ_nat
                 (Peano.pred
                    (Z.abs_nat
                       (Zpower_nat beta (Z.abs_nat prec - Z.abs_nat s)))))
           (dExp (make_bound beta prec emin))).
exact H2.
generalize (make_bound_Emin beta (prec-s) _ emin_neg).
generalize (make_bound_p beta (prec-s) emin).
destruct (make_bound beta (prec-s) emin) as (l1,l2).
simpl; intros H3 H4; f_equal.
apply Pos2Z.inj.
rewrite H3; try omega.
replace (Z.abs_nat (prec - s)) with (Z.abs_nat prec - Z.abs_nat s)%nat.
rewrite <- (p'GivesBound beta (make_bound beta prec emin) (Zabs_nat s) (Zabs_nat prec)) at 2.
simpl; easy.
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
455 456
apply ZleLe; rewrite inj_abs; auto with zarith.
apply ZleLe; rewrite inj_minus, 2!inj_abs, Zmax_r; simpl; auto with zarith.
457
apply Nat2Z.inj.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
458 459
rewrite inj_minus; repeat rewrite inj_abs; try omega.
apply Zmax_r; omega.
460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477
apply N2Z.inj.
rewrite H4.
rewrite Zabs2N.id_abs.
now apply Z.abs_neq.
apply Nat2Z.inj.
rewrite inj_abs; try omega.
rewrite inj_minus, Zmax_r; rewrite 2!inj_abs; omega.
apply RND_EvenClosest_correct.
apply radix_gt_1.
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
apply make_bound_p; omega.
rewrite pff_round_NE_is_round; try omega.
f_equal; f_equal.
rewrite make_bound_Emin; omega.
apply make_bound_p; omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
478 479 480 481 482 483 484 485 486 487
Theorem Veltkamp: exists choice': Z->bool ,
   hx = round beta (FLT_exp emin (prec-s)) (Znearest choice') x.
Proof with auto with typeclass_instances.
assert (precisionNotZero : (1 < prec)%Z) by omega.
destruct (format_is_pff_format beta (make_bound beta prec emin)
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x)
  as (fx,(Hfx,Hfx')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
488
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
489 490 491 492 493
  choice (x*(bpow s+1)))
  as (fp,(Hfp, (Hfp',Hfp''))).
rewrite make_bound_Emin in Hfp''; try assumption.
replace (--emin)%Z with emin in Hfp'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
494
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
495 496 497 498 499
  choice (x-p))
  as (fq,(Hfq, (Hfq',Hfq''))).
rewrite make_bound_Emin in Hfq''; try assumption.
replace (--emin)%Z with emin in Hfq'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
500
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
501 502 503 504 505
  choice (q+p))
  as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
(* *)
506
destruct Veltkamp with beta (make_bound beta prec emin) (Zabs_nat s)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
507 508 509 510 511 512 513 514 515
   (Zabs_nat prec) fx fp fq fhx as (H1,(hx', (H2,(H3,H4)))); try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
replace 2%nat with (Zabs_nat 2) by easy.
apply Zabs_nat_le; omega.
apply Nat2Z.inj_le.
rewrite inj_abs; try omega.
rewrite inj_minus, Zmax_r; rewrite inj_abs; simpl; omega.
rewrite Hfx; rewrite inj_abs; try omega.
516
rewrite bpow_powerRZ in Hfp'; exact Hfp'.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535
rewrite Hfx, Hfp''; assumption.
rewrite Hfp'', Hfq''; assumption.
(* *)
destruct pff_round_is_round_N with beta (make_bound beta (prec-s) emin)
 (Z.abs_nat (prec-s)) (FtoR beta fx) hx' as (choice',M).
rewrite Zabs2Nat.id.
apply make_bound_p; omega.
rewrite inj_abs; simpl; omega.
unfold make_bound.
replace (Z.to_pos (beta ^ (prec - s))) with (Pos.of_succ_nat
                 (Init.Nat.pred
                    (Z.abs_nat
                       (Zpower_nat beta
                          (Z.abs_nat prec - Z.abs_nat s))))).
replace (Z.abs_N emin) with (dExp (make_bound beta prec emin)) by easy.
exact H3.
apply Zpos_eq_iff.
apply trans_eq with (Zpower_nat beta (Z.abs_nat prec - Z.abs_nat s)).
rewrite <- p''GivesBound with (b:=make_bound beta prec emin) at 2.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
536
simpl; auto.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
537 538 539 540 541 542 543 544 545 546 547 548 549
apply radix_gt_1.
rewrite Zpower_Zpower_nat,Z2Pos.id.
f_equal; apply sym_eq, Zabs2Nat.inj_sub; omega.
apply Zpower_nat_less.
apply radix_gt_1.
omega.
exists choice'.
unfold hx; rewrite <- Hfhx'', <- H2, M.
f_equal; try easy.
f_equal.
rewrite make_bound_Emin; omega.
rewrite inj_abs; simpl; omega.
Qed.
550

BOLDO Sylvie's avatar
BOLDO Sylvie committed
551
Theorem Veltkamp_tail:
552 553
 x = hx+tx /\  generic_format beta (FLT_exp emin s) tx.
Proof with auto with typeclass_instances.
554
assert (precisionNotZero : (1 < prec)%Z) by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
555 556 557 558 559
destruct (format_is_pff_format beta (make_bound beta prec emin)
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x)
  as (fx,(Hfx,Hfx')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
560
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
561
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
562
  choice (x*(bpow s+1)))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
563 564 565
  as (fp,(Hfp, (Hfp',Hfp''))).
rewrite make_bound_Emin in Hfp''; try assumption.
replace (--emin)%Z with emin in Hfp'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
566
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
567
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
568
  choice (x-p))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
569 570 571
  as (fq,(Hfq, (Hfq',Hfq''))).
rewrite make_bound_Emin in Hfq''; try assumption.
replace (--emin)%Z with emin in Hfq'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
572
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
573
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
574
  choice (q+p))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
575 576 577
  as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
578
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
579
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
580
  choice (x-hx))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
581 582 583 584
  as (ftx,(Hftx, (Hftx',Hftx''))).
rewrite make_bound_Emin in Hftx''; try assumption.
replace (--emin)%Z with emin in Hftx'' by omega.
(* *)
585
destruct Veltkamp_tail with beta (make_bound beta prec emin) (Zabs_nat s)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
586 587 588 589 590 591 592 593 594
   (Zabs_nat prec) fx fp fq fhx ftx as (tx', (H1,(H2,(H3,H4)))); try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
replace 2%nat with (Zabs_nat 2) by easy.
apply Zabs_nat_le; omega.
apply Nat2Z.inj_le.
rewrite inj_abs; try omega.
rewrite inj_minus, Zmax_r; rewrite inj_abs; simpl; omega.
rewrite Hfx; rewrite inj_abs; try omega.
595
rewrite bpow_powerRZ in Hfp'; apply Hfp'.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613
rewrite Hfx, Hfp''; apply Hfq'.
rewrite Hfp'', Hfq''; apply Hfhx'.
rewrite Hfhx'', Hfx; apply Hftx'.
(* *)
split.
rewrite <- Hfx, <-H2, Hfhx'', H1, Hftx''; easy.
unfold tx; rewrite <- Hftx'', <- H1.
replace emin with (-dExp (Bound
       (Pos.of_succ_nat
                 (Peano.pred (Z.abs_nat (Zpower_nat beta (Z.abs_nat s)))))
       (dExp (make_bound beta prec emin))))%Z.
apply pff_format_is_format; try assumption; try omega.
simpl.
rewrite Zpos_P_of_succ_nat, inj_pred.
rewrite <- Zsucc_pred.
apply inj_abs.
apply Zpower_NR0.
apply Zlt_le_weak; apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
614
apply sym_not_eq, Nat.lt_neq, lt_Zlt_inv.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
615 616 617 618 619 620 621 622
rewrite inj_abs.
apply Zpower_nat_less.
apply radix_gt_1.
apply Zpower_NR0.
apply Zlt_le_weak; apply radix_gt_0.
simpl.
rewrite Zabs2N.id_abs.
rewrite Z.abs_neq; omega.
623 624 625 626
Qed.

End Veltkamp.

627 628 629 630 631 632 633 634 635
Section Underf_mult_aux.

Variable beta : radix.
Variable b: Fbound.
Variable prec: Z.

Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat beta (Zabs_nat prec).
Hypothesis precisionGt1 : (1 < prec)%Z.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
636

637
Lemma underf_mult_aux:
BOLDO Sylvie's avatar
BOLDO Sylvie committed
638
 forall e x y,
639 640
  Fbounded b x ->
  Fbounded b y ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
641
   (bpow beta (e + 2 * prec - 1)%Z <= Rabs (FtoR beta x * FtoR beta y)) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
642
     (e <= Pff.Fexp x + Pff.Fexp y)%Z.
643
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
644
intros e x y Fx Fy H.
645
assert (HH: forall z, Fbounded b z
BOLDO Sylvie's avatar
BOLDO Sylvie committed
646
   -> Rabs (FtoR beta z) < bpow beta (Pff.Fexp z + prec)).
647
clear -precisionGt1 pGivesBound; intros z Hz.
648
unfold FtoR; rewrite <- bpow_powerRZ.
649 650 651 652 653 654 655
rewrite Rabs_mult, Rmult_comm.
rewrite Rabs_right.
2: apply Rle_ge, bpow_ge_0.
rewrite bpow_plus; apply Rmult_lt_compat_l.
apply bpow_gt_0.
destruct Hz as (T1,T2).
rewrite pGivesBound in T1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
656 657
rewrite <- abs_IZR, <- IZR_Zpower;[idtac|omega].
apply IZR_lt.
658 659
apply Zlt_le_trans with (1:=T1).
rewrite Zpower_Zpower_nat; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
660
assert (e+2*prec-1 < (Pff.Fexp x+prec) +(Pff.Fexp y +prec))%Z; try omega.
661 662 663 664 665 666 667 668 669 670 671
(* *)
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=H).
rewrite Rabs_mult, bpow_plus.
apply Rmult_lt_compat.
apply Rabs_pos.
apply Rabs_pos.
now apply HH.
now apply HH.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
672 673 674 675 676
Lemma underf_mult_aux':
 forall x y,
  Fbounded b x ->
  Fbounded b y ->
   (bpow beta (-dExp b + 2 * prec - 1)%Z <= Rabs (FtoR beta x * FtoR beta y)) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
677
     (-dExp b <= Pff.Fexp x + Pff.Fexp y)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
678 679 680 681 682 683 684
Proof.
intros.
now apply underf_mult_aux.
Qed.



685 686 687
End Underf_mult_aux.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
688 689
Section Dekker.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
690 691
Variable beta : radix.
Variable emin prec: Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
692
Variable choice : Z -> bool.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
693 694 695 696 697 698 699
Let s:= (prec- Z.div2 prec)%Z.

Hypothesis precisionGe4 : (4 <= prec)%Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Hypothesis emin_neg: (emin < 0)%Z.

Notation format := (generic_format beta (FLT_exp emin prec)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
700 701
Notation round_flt :=(round beta (FLT_exp emin prec) (Znearest choice)).
Notation round_flt_s :=(round beta (FLT_exp emin (prec-s)) (Znearest choice)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736
Notation ulp_flt :=(ulp beta (FLT_exp emin prec)).
Notation bpow e := (bpow beta e).

(** inputs *)
Variable x y:R.
Hypothesis Fx: format x.
Hypothesis Fy: format y.

(*** algorithm *)
(** first Veltkamp *)
Let px := round_flt (x*(bpow s+1)).
Let qx:= round_flt (x-px).
Let hx:=round_flt (qx+px).
Let tx:=round_flt (x-hx).

(** second Veltkamp *)
Let py := round_flt (y*(bpow s+1)).
Let qy:= round_flt (y-py).
Let hy:=round_flt (qy+py).
Let ty:=round_flt (y-hy).

(** all products *)
Let x1y1:=round_flt (hx*hy).
Let x1y2:=round_flt (hx*ty).
Let x2y1:=round_flt (tx*hy).
Let x2y2:=round_flt (tx*ty).

(** final summation *)
Let r :=round_flt(x*y).
Let t1 :=round_flt (-r+x1y1).
Let t2 :=round_flt (t1+x1y2).
Let t3 :=round_flt (t2+x2y1).
Let t4 :=round_flt (t3+x2y2).

Theorem Dekker: (radix_val beta=2)%Z \/ (Z.Even prec) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
737
  (x*y=0 \/ bpow (emin + 2 * prec - 1) <= Rabs (x * y) ->  (x*y=r+t4)%R) /\
BOLDO Sylvie's avatar
BOLDO Sylvie committed
738 739 740
    (Rabs (x*y-(r+t4)) <= (7/2)*bpow emin)%R.
Proof with auto with typeclass_instances.
intros HH.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786
(* x=0 *)
case (Req_dec x 0); intros Kx.
assert (Kr: r=0).
unfold r; rewrite Kx, Rmult_0_l, round_0...
assert (Khx: hx=0).
unfold hx, qx, px; rewrite Kx, Rmult_0_l, round_0...
rewrite Rplus_0_r, Rminus_0_l, Ropp_0, round_0...
apply round_0...
assert (Kt4: t4=0).
unfold t4, t3, t2, t1, x1y1, x1y2, x2y1, x2y2, tx; rewrite Kr, Kx, Khx.
rewrite 2!Rmult_0_l, round_0...
rewrite Rminus_0_r, Rplus_0_r, round_0...
rewrite 2!Rmult_0_l, round_0...
rewrite 3!Rplus_0_r, Ropp_0; repeat rewrite round_0...
rewrite Kx, Kr, Kt4.
split;[intros; ring|idtac].
rewrite Rmult_0_l, Rplus_0_l, Rminus_0_l, Ropp_0, Rabs_R0.
apply Rmult_le_pos; try apply bpow_ge_0.
apply Rmult_le_pos.
apply Fourier_util.Rle_zero_pos_plus1; apply Rmult_le_pos.
left; apply Rlt_0_2.
apply Fourier_util.Rle_zero_pos_plus1; left; apply Rlt_0_2.
left; apply pos_half_prf.
(* y = 0 *)
case (Req_dec y 0); intros Ky.
assert (Kr: r=0).
unfold r; rewrite Ky, Rmult_0_r, round_0...
assert (Khy: hy=0).
unfold hy, qy, py; rewrite Ky, Rmult_0_l, round_0...
rewrite Rplus_0_r, Rminus_0_l, Ropp_0, round_0...
apply round_0...
assert (Kt4: t4=0).
unfold t4, t3, t2, t1, x1y1, x1y2, x2y1, x2y2, ty; rewrite Kr, Ky, Khy.
rewrite 2!Rmult_0_r, round_0...
rewrite Rminus_0_r, Rplus_0_r, round_0...
rewrite 2!Rmult_0_r, round_0...
rewrite 3!Rplus_0_r, Ropp_0; repeat rewrite round_0...
rewrite Ky, Kr, Kt4.
split;[intros; ring|idtac].
rewrite Rmult_0_r, Rplus_0_l, Rminus_0_l, Ropp_0, Rabs_R0.
apply Rmult_le_pos; try apply bpow_ge_0.
apply Rmult_le_pos.
apply Fourier_util.Rle_zero_pos_plus1; apply Rmult_le_pos.
left; apply Rlt_0_2.
apply Fourier_util.Rle_zero_pos_plus1; left; apply Rlt_0_2.
left; apply pos_half_prf.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
787 788 789 790 791 792 793 794
(* Veltkamp x *)
assert (precisionNotZero : (1 < prec)%Z) by omega.
assert (emin_neg': (emin <= 0)%Z) by omega.
destruct (format_is_pff_format_can beta (make_bound beta prec emin)
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x)
  as (fx,(Hfx,Hfx')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
795
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
796
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
797
  choice (x*(bpow s+1)))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
798 799 800
  as (fpx,(Hfpx, (Hfpx',Hfpx''))).
rewrite make_bound_Emin in Hfpx''; try assumption.
replace (--emin)%Z with emin in Hfpx'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
801
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
802
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
803
  choice (x-px))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
804 805 806
  as (fqx,(Hfqx, (Hfqx',Hfqx''))).
rewrite make_bound_Emin in Hfqx''; try assumption.
replace (--emin)%Z with emin in Hfqx'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
807
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
808
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
809
  choice (qx+px))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
810 811 812
  as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
813
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
814
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
815
  choice (x-hx))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
816 817 818 819 820 821 822 823 824
  as (ftx,(Hftx, (Hftx',Hftx''))).
rewrite make_bound_Emin in Hftx''; try assumption.
replace (--emin)%Z with emin in Hftx'' by omega.
(* Veltkamp y*)
destruct (format_is_pff_format_can beta (make_bound beta prec emin)
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero y)
  as (fy,(Hfy,Hfy')).
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
825
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
826
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
827
  choice (y*(bpow s+1)))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
828 829 830
  as (fpy,(Hfpy, (Hfpy',Hfpy''))).
rewrite make_bound_Emin in Hfpy''; try assumption.
replace (--emin)%Z with emin in Hfpy'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
831
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
832
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
833
  choice (y-py))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
834 835 836
  as (fqy,(Hfqy, (Hfqy',Hfqy''))).
rewrite make_bound_Emin in Hfqy''; try assumption.
replace (--emin)%Z with emin in Hfqy'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
837
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
838
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
839
  choice (qy+py))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
840 841 842
  as (fhy,(Hfhy, (Hfhy',Hfhy''))).
rewrite make_bound_Emin in Hfhy''; try assumption.
replace (--emin)%Z with emin in Hfhy'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
843
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
844
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
845
  choice (y-hy))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
846 847 848 849
  as (fty,(Hfty, (Hfty',Hfty''))).
rewrite make_bound_Emin in Hfty''; try assumption.
replace (--emin)%Z with emin in Hfty'' by omega.
(* products *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
850
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
851
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
852
  choice (hx*hy))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
853 854 855
  as (fx1y1,(Hfx1y1, (Hfx1y1',Hfx1y1''))).
rewrite make_bound_Emin in Hfx1y1''; try assumption.
replace (--emin)%Z with emin in Hfx1y1'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
856
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
857
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
858
  choice (hx*ty))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
859 860 861
  as (fx1y2,(Hfx1y2, (Hfx1y2',Hfx1y2''))).
rewrite make_bound_Emin in Hfx1y2''; try assumption.
replace (--emin)%Z with emin in Hfx1y2'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
862
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
863
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
864
  choice (tx*hy))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
865 866 867
  as (fx2y1,(Hfx2y1, (Hfx2y1',Hfx2y1''))).
rewrite make_bound_Emin in Hfx2y1''; try assumption.
replace (--emin)%Z with emin in Hfx2y1'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
868
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
869
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
870
  choice (tx*ty))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
871 872 873 874
  as (fx2y2,(Hfx2y2, (Hfx2y2',Hfx2y2''))).
rewrite make_bound_Emin in Hfx2y2''; try assumption.
replace (--emin)%Z with emin in Hfx2y2'' by omega.
(* t_is *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
875
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
876
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
877
  choice (x*y))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
878 879 880
  as (fr,(Hfr, (Hfr',Hfr''))).
rewrite make_bound_Emin in Hfr''; try assumption.
replace (--emin)%Z with emin in Hfr'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
881
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
882
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
883
  choice (-r+x1y1))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
884 885 886
  as (ft1,(Hft1, (Hft1',Hft1''))).
rewrite make_bound_Emin in Hft1''; try assumption.
replace (--emin)%Z with emin in Hft1'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
887
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
888
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
889
  choice (t1+x1y2))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
890 891 892
  as (ft2,(Hft2, (Hft2',Hft2''))).
rewrite make_bound_Emin in Hft2''; try assumption.
replace (--emin)%Z with emin in Hft2'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
893
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
894
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
895
  choice (t2+x2y1))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
896 897 898
  as (ft3,(Hft3, (Hft3',Hft3''))).
rewrite make_bound_Emin in Hft3''; try assumption.
replace (--emin)%Z with emin in Hft3'' by omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
899
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
900
   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
BOLDO Sylvie's avatar
BOLDO Sylvie committed
901
  choice (t3+x2y2))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
902 903 904 905 906 907
  as (ft4,(Hft4, (Hft4',Hft4''))).
rewrite make_bound_Emin in Hft4''; try assumption.
replace (--emin)%Z with emin in Hft4'' by omega.
(* *)
assert (Hs:(s =(Z.abs_nat prec - Nat.div2 (Z.abs_nat prec))%nat)).
unfold s; rewrite inj_minus.
908 909 910 911 912 913 914 915 916 917
assert (TT: (Z.div2 prec = Nat.div2 (Z.abs_nat prec))%Z).
rewrite Nat.div2_div, Z.div2_div, div_Zdiv; simpl.
rewrite inj_abs; omega.
omega.
rewrite <- TT.
rewrite inj_abs; try omega.
rewrite Z.max_r; try omega.
assert (Z.div2 prec <= prec)%Z; try omega.
rewrite Z.div2_div; apply Zlt_le_weak.
apply Z_div_lt; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
918
(* *)
919
assert (D:(((- dExp (make_bound beta prec emin) <= Pff.Fexp fx + Pff.Fexp fy)%Z ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
920 921 922
        (FtoR beta fx * FtoR beta fy = FtoR beta fr + FtoR beta ft4)) /\
   Rabs (FtoR beta fx * FtoR beta fy - (FtoR beta fr + FtoR beta ft4)) <=
       7 / 2 * powerRZ beta (- dExp (make_bound beta prec emin)))).
923
apply Dekker with (Zabs_nat prec) fpx fqx fhx ftx fpy fqy fhy fty
BOLDO Sylvie's avatar
BOLDO Sylvie committed
924 925 926 927 928 929
   fx1y1 fx1y2 fx2y1 fx2y2 ft1 ft2 ft3; try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
replace 4%nat with (Zabs_nat 4) by easy.
apply Zabs_nat_le; omega.
(* . *)
930
rewrite Hfx, <- Hs, <- bpow_powerRZ; apply Hfpx'.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
931 932 933
rewrite Hfx, Hfpx''; apply Hfqx'.
rewrite Hfpx'', Hfqx''; apply Hfhx'.
rewrite Hfx, Hfhx''; apply Hftx'.
934
rewrite Hfy, <- Hs, <- bpow_powerRZ; apply Hfpy'.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
935 936 937 938 939 940 941 942 943 944 945 946 947 948
rewrite Hfy, Hfpy''; apply Hfqy'.
rewrite Hfpy'', Hfqy''; apply Hfhy'.
rewrite Hfy, Hfhy''; apply Hfty'.
rewrite Hfhx'', Hfhy''; apply Hfx1y1'.
rewrite Hfhx'', Hfty''; apply Hfx1y2'.
rewrite Hftx'', Hfhy''; apply Hfx2y1'.
rewrite Hftx'', Hfty''; apply Hfx2y2'.
rewrite Hfx, Hfy; apply Hfr'.
rewrite Hfr'', Hfx1y1''; apply Hft1'.
rewrite Hft1'', Hfx1y2''; apply Hft2'.
rewrite Hft2'', Hfx2y1''; apply Hft3'.
rewrite Hft3'', Hfx2y2''; apply Hft4'.
rewrite make_bound_Emin; omega.
case HH; intros K;[now left|right].
949
destruct K as (l,Hl).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
950
apply even_equiv.
951 952 953 954 955
exists (Zabs_nat l).
apply Nat2Z.inj.
rewrite inj_mult.
rewrite 2!inj_abs; try omega.
rewrite Hl; simpl; easy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
956 957
(* *)
rewrite <- Hfx, <- Hfy.
958 959 960 961 962
unfold r; rewrite <- Hfr''.
unfold t4; rewrite <- Hft4''.
destruct D as (D1,D2); split.
intros L.
apply D1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
963
apply underf_mult_aux' with beta prec; try assumption.
964 965 966
apply make_bound_p; assumption.
now apply FcanonicBound with beta.
now apply FcanonicBound with beta.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
967 968 969 970 971 972
case L; intros L'.
contradict L'.
apply Rmult_integral_contrapositive_currified.
rewrite Hfx; easy.
rewrite Hfy; easy.
apply Rle_trans with (2:=L').
973 974 975 976 977
right; repeat f_equal.
rewrite make_bound_Emin, Zopp_involutive; omega.
apply Rle_trans with (1:=D2).
rewrite make_bound_Emin, Zopp_involutive.
2: omega.
978
rewrite bpow_powerRZ.
979 980
now right.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
981 982 983 984


End Dekker.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
985
Section ErrFMA_V1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
986

BOLDO Sylvie's avatar
BOLDO Sylvie committed
987
Variable beta : radix.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
988
Variable emin prec : Z.