Double_rounding_odd_radix.v 85.3 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
(**
This example is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2014-2018 Pierre Roux

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.
*)

18 19 20
(** * Conditions for innocuous double rounding. *)

Require Import Psatz.
21
From Flocq Require Import Raux Defs Generic_fmt Operations Ulp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
22
From Flocq Require Import FLX FLT FTZ Double_rounding.
23 24 25 26 27 28 29

Open Scope R_scope.

Section Double_round_beta_odd.

Variable beta : radix.
Notation bpow e := (bpow beta e).
30
Notation mag x := (mag beta x).
31 32 33 34 35 36

(** A little tactic to simplify terms of the form [bpow a * bpow b]. *)
Ltac bpow_simplify :=
  (* bpow ex * bpow ey ~~> bpow (ex + ey) *)
  repeat
    match goal with
Guillaume Melquiond's avatar
Guillaume Melquiond committed
37
      | |- context [(Raux.bpow _ _ * Raux.bpow _ _)] =>
38
        rewrite <- bpow_plus
Guillaume Melquiond's avatar
Guillaume Melquiond committed
39
      | |- context [(?X1 * Raux.bpow _ _ * Raux.bpow _ _)] =>
40
        rewrite (Rmult_assoc X1); rewrite <- bpow_plus
Guillaume Melquiond's avatar
Guillaume Melquiond committed
41
      | |- context [(?X1 * (?X2 * Raux.bpow _ _) * Raux.bpow _ _)] =>
42 43 44 45 46 47
        rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 * X2));
        rewrite <- bpow_plus
    end;
  (* ring_simplify arguments of bpow *)
  repeat
    match goal with
Guillaume Melquiond's avatar
Guillaume Melquiond committed
48
      | |- context [(Raux.bpow _ ?X)] =>
49 50 51
        progress ring_simplify X
    end;
  (* bpow 0 ~~> 1 *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
52
  change (Raux.bpow _ 0) with 1;
53 54 55 56 57 58 59 60 61 62 63 64 65
  repeat
    match goal with
      | |- context [(_ * 1)] =>
        rewrite Rmult_1_r
    end.

Hypothesis Obeta : exists n, (beta = 2 * n + 1 :> Z)%Z.

Lemma midpoint_beta_odd_remains_pos :
  forall x,
  0 < x ->
  forall (ex1 ex2 : Z),
  (ex2 <= ex1)%Z ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
66
  x = IZR (Zfloor (x * bpow (- ex1))) * bpow ex1 ->
67 68
  exists x',
    0 < x'
69
    /\ (mag x' = mag x :> Z)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
70
    /\ x' = IZR (Zfloor (x' * bpow (- ex2))) * bpow ex2
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
    /\ x + / 2 * bpow ex1 = x' + / 2 * bpow ex2.
Proof.
intros x Px ex1 ex2 Hf2.
set (z := (ex1 - ex2)%Z).
assert (Hz : Z_of_nat (Zabs_nat z) = z).
{ rewrite Zabs2Nat.id_abs.
  rewrite <- cond_Zopp_Zlt_bool; unfold cond_Zopp.
  assert (H : (z <? 0)%Z = false); [|now rewrite H].
  apply Zlt_bool_false; unfold z; omega. }
revert Hz.
generalize (Zabs_nat z); intro n.
unfold z; clear z; revert ex1 ex2 Hf2.
induction n.
- simpl.
  intros ex1 ex2 _ Hf1 Fx.
  exists x.
  assert (H : ex2 = ex1) by omega.
  split; [|split; [|split]].
  + exact Px.
  + reflexivity.
91
  + revert Fx; unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
92
    now rewrite H.
93
  + now unfold ulp, cexp; rewrite H.
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116
- intros ex1 ex2 Hf2 HSn Fx.
  destruct Obeta as (nb,Hb).
  assert (Hbeta : (2 <= beta)%Z).
  { destruct beta as (beta_val,beta_prop).
    now apply Zle_bool_imp_le. }
  assert (Nnnb : (1 <= nb)%Z) by omega.
  assert (Hf1 : (ex1 = ex2 + Z.of_nat n + 1 :> Z)%Z); [|clear HSn].
  { rewrite <- Zplus_assoc.
    replace (_ + 1)%Z with (Z.of_nat (S n)); [omega|].
    simpl.
    now rewrite Zpos_P_of_succ_nat. }
  assert (Hf2' : (ex2 + 1 <= ex1)%Z).
  { rewrite Hf1.
    rewrite <- Zplus_assoc.
    apply Zplus_le_compat_l.
    rewrite <- (Zplus_0_l 1) at 1; apply Zplus_le_compat_r.
    apply Zle_0_nat. }
  assert (Hd1 : Z.of_nat n = (ex1 - (ex2 + 1))%Z);
    [now rewrite Hf1; ring|].
  set (ex2' := (ex2 + 1)%Z).
  destruct (IHn ex1 ex2' Hf2' Hd1 Fx)
    as (x',(Px',(Hlx',(Fx',Hx')))); clear Hd1 IHn.
  set (u := bpow ex2).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
117
  exists (x' + IZR nb * u).
118 119 120 121
  split; [|split; [|split]].
  + apply (Rlt_le_trans _ _ _ Px').
    rewrite <- (Rplus_0_r x') at 1; apply Rplus_le_compat_l.
    apply Rmult_le_pos.
122
    * apply IZR_le; omega.
123 124
    * now apply bpow_ge_0.
  + rewrite <- Hlx'.
125
    apply (mag_plus_eps beta (fun e => (e - (mag x' - ex2'))%Z));
126 127
      [| |split].
    * exact Px'.
128
    * unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
129 130 131 132
      bpow_simplify.
      rewrite Ztrunc_floor; [exact Fx'|].
      now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0].
    * apply Rmult_le_pos; [|now apply bpow_ge_0].
133
      apply IZR_le; omega.
134
    * rewrite ulp_neq_0;[idtac| now apply Rgt_not_eq].
135
      unfold u, ex2', cexp; bpow_simplify.
136 137 138
      rewrite Zplus_comm; rewrite bpow_plus.
      apply Rmult_lt_compat_r; [now apply bpow_gt_0|].
      rewrite bpow_1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
139
      apply IZR_lt; omega.
140 141 142 143 144
  + rewrite Fx' at 1.
    unfold ex2' at 2.
    rewrite Zplus_comm; rewrite bpow_plus; fold u.
    rewrite <- Rmult_assoc; rewrite <- Rmult_plus_distr_r.
    apply Rmult_eq_compat_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
145
    replace (IZR _) with (x' * bpow (- ex2'));
146 147 148 149 150
      [|now apply (Rmult_eq_reg_r (bpow ex2'));
         [|now apply Rgt_not_eq; apply bpow_gt_0]; bpow_simplify].
    rewrite Rmult_plus_distr_r.
    unfold u, ex2'; bpow_simplify.
    rewrite Fx' at 2; unfold ex2'; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
151 152 153
    rewrite bpow_1; rewrite <- mult_IZR; rewrite <- plus_IZR.
    rewrite Zfloor_IZR.
    rewrite plus_IZR.
154 155 156
    apply f_equal2; [|reflexivity].
    replace (- ex2 - 1)%Z with (- ex2')%Z; [|now unfold ex2'; ring].
    rewrite Fx' at 1; unfold ex2'; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
157
    now rewrite mult_IZR; rewrite <- bpow_1.
158 159 160 161 162
  + rewrite Hx'.
    rewrite Rplus_assoc; apply Rplus_eq_compat_l.
    rewrite <- Rmult_plus_distr_r.
    unfold ex2'; rewrite Zplus_comm; rewrite bpow_plus.
    rewrite <- Rmult_assoc; apply Rmult_eq_compat_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
163
    rewrite (Rmult_eq_reg_l 2 _ (IZR nb + / 2)); [reflexivity| |lra].
164
    field_simplify; apply Rmult_eq_compat_r.
165
    rewrite bpow_1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
166
    now rewrite <- mult_IZR; rewrite <- plus_IZR; apply f_equal.
167 168 169 170 171 172 173
Qed.

Lemma midpoint_beta_odd_remains :
  forall x,
  0 <= x ->
  forall (ex1 ex2 : Z),
  (ex2 <= ex1)%Z ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
174
  x = IZR (Zfloor (x * bpow (- ex1))) * bpow ex1 ->
175 176
  exists x',
    0 <= x'
Guillaume Melquiond's avatar
Guillaume Melquiond committed
177
    /\ x' = IZR (Zfloor (x' * bpow (- ex2))) * bpow ex2
178 179 180 181 182 183 184 185 186 187 188
    /\ x + / 2 * bpow ex1 = x' + / 2 * bpow ex2.
Proof.
intros x Px ex1 ex2 Hf2 Hx.
set (x1 := x + bpow ex1).
assert (Px1 : 0 < x1).
{ apply (Rle_lt_trans _ _ _ Px).
  rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l, bpow_gt_0. }
destruct (midpoint_beta_odd_remains_pos x1 Px1 ex1 ex2 Hf2)
  as (x',(Hx'1,(Hx'2,(Hx'3,Hx'4)))).
{ unfold x1 at 2.
  rewrite Rmult_plus_distr_r, Hx; bpow_simplify.
189
  rewrite <- plus_IZR.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
190
  now rewrite Zfloor_IZR, plus_IZR, Rmult_plus_distr_r, Rmult_1_l, <- Hx. }
191 192 193 194 195 196 197 198
assert (Hx' : x' = x1 + / 2 * bpow ex1 - / 2 * bpow ex2).
{ rewrite Hx'4; ring. }
exists (x' - bpow ex1); split; [|split].
- rewrite Hx'; unfold x1; ring_simplify.
  replace (_ - _) with (x + (/ 2 * (bpow ex1 - bpow ex2))) by ring.
  apply Rplus_le_le_0_compat; [exact Px|]; apply Rmult_le_pos; [lra|].
  now apply Rle_0_minus, bpow_le.
- rewrite Rmult_minus_distr_r; rewrite Hx'3 at 2; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
199 200 201
  rewrite <- (IZR_Zpower beta (ex1 - ex2)); [|now apply Zle_minus_le_0].
  rewrite <- minus_IZR, Zfloor_IZR, minus_IZR.
  rewrite (IZR_Zpower beta (ex1 - ex2)); [|now apply Zle_minus_le_0].
202 203 204 205 206 207 208 209 210 211 212
  rewrite Rmult_minus_distr_r; bpow_simplify.
  now rewrite Hx'3 at 1.
- rewrite Hx'; unfold x1; ring.
Qed.

Lemma neq_midpoint_beta_odd_aux1 :
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  forall x,
  0 < x ->
213
  (fexp2 (mag x) <= fexp1 (mag x))%Z ->
214
  midp beta fexp1 x - / 2 * ulp beta fexp2 x <= x < midp beta fexp1 x ->
215
  round_round_eq beta fexp1 fexp2 choice1 choice2 x.
216 217
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
218 219
unfold midp in Hx.
rewrite 2!ulp_neq_0 in Hx; try now apply Rgt_not_eq.
220
unfold round_round_eq.
221 222
set (ex1 := fexp1 (mag x)).
set (ex2 := fexp2 (mag x)).
223 224 225 226
set (rx1 := round beta fexp1 Zfloor x).
assert (Prx1 : 0 <= rx1).
{ rewrite <- (round_0 beta fexp1 Zfloor).
  now apply round_le; [exact Vfexp1|apply valid_rnd_DN|apply Rlt_le]. }
Guillaume Melquiond's avatar
Guillaume Melquiond committed
227
assert (Hrx1 : rx1 = IZR (Zfloor (rx1 * bpow (- ex1))) * bpow ex1).
228
{ unfold rx1 at 2; unfold round, F2R, scaled_mantissa, cexp; simpl.
229
  unfold ex1; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
230
  now rewrite Zfloor_IZR. }
231 232 233 234 235 236 237 238
destruct (midpoint_beta_odd_remains rx1 Prx1 ex1 ex2 Hf2f1 Hrx1)
  as (rx2,(Nnrx2, (Hrx2, Hrx12))).
assert (Hx' : rx2 <= x < rx2 + / 2 * bpow ex2).
{ split.
  - replace rx2 with (rx2 + / 2 * bpow ex2 - / 2 * bpow ex2) by ring.
    rewrite <- Hrx12; apply Hx.
  - rewrite <- Hrx12; apply Hx. }
assert (Hr2 : round beta fexp2 (Znearest choice2) x = rx2).
239
{ unfold round, F2R, scaled_mantissa, cexp; simpl.
240
  apply (Rmult_eq_reg_r (bpow (- fexp2 (mag x))));
241 242 243 244 245 246 247 248 249 250
    [|now apply Rgt_not_eq, Rlt_gt, bpow_gt_0].
  bpow_simplify.
  rewrite (Znearest_imp _ _ (Zfloor (rx2 * bpow (- ex2)))).
  - now rewrite Hrx2 at 2; unfold ex2; bpow_simplify.
  - apply Rabs_lt; split.
    + apply Rlt_le_trans with 0; [lra|].
      apply Rle_0_minus.
      apply (Rmult_le_reg_r (bpow ex2)); [now apply bpow_gt_0|].
      fold ex2; bpow_simplify.
      now rewrite <- Hrx2.
251
    + apply (Rmult_lt_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|].
252 253 254 255 256 257 258 259 260 261 262
      rewrite Rmult_minus_distr_r; fold ex2; bpow_simplify.
      rewrite <- Hrx2.
      now apply (Rplus_lt_reg_l rx2); ring_simplify. }
rewrite Hr2.
assert (Hrx2' : rx1 <= rx2 < rx1 + / 2 * bpow ex1).
{ split.
  - apply (Rplus_le_reg_r (/ 2 * bpow ex1)).
    rewrite Hrx12.
    apply Rplus_le_compat_l.
    apply Rmult_le_compat_l; [lra|].
    now apply bpow_le.
263
  - apply (Rle_lt_trans _ _ _ (proj1 Hx') (proj2 Hx)). }
264
assert (Hrx2r : rx2 = round beta fexp2 Zfloor x).
265
{ unfold round, F2R, scaled_mantissa, cexp; simpl.
266 267 268 269 270 271
  fold ex2; rewrite Hrx2.
  apply Rmult_eq_compat_r, f_equal.
  apply eq_sym, Zfloor_imp; split.
  - apply (Rle_trans _ _ _ (Zfloor_lb _)).
    now apply Rmult_le_compat_r; [apply bpow_ge_0|].
  - apply (Rmult_lt_reg_r (bpow ex2)); [now apply bpow_gt_0|]; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
272
    rewrite plus_IZR, Rmult_plus_distr_r, <- Hrx2.
273 274 275 276 277 278
    apply (Rlt_le_trans _ _ _ (proj2 Hx')).
    apply Rplus_le_compat_l, Rmult_le_compat_r; [apply bpow_ge_0|simpl; lra]. }
destruct (Rle_or_lt rx2 0) as [Nprx2|Prx2].
{ (* rx2 = 0 *)
  assert (Zrx2 : rx2 = 0); [now apply Rle_antisym|].
  rewrite Zrx2, round_0; [|now apply valid_rnd_N].
279
  unfold round, F2R, scaled_mantissa, cexp; simpl.
280
  apply (Rmult_eq_reg_r (bpow (- fexp1 (mag x))));
281
    [|now apply Rgt_not_eq, bpow_gt_0]; rewrite Rmult_0_l; bpow_simplify.
282
  apply IZR_eq, eq_sym, Znearest_imp.
283 284 285 286
  apply Rabs_lt; simpl; unfold Rminus; rewrite Ropp_0, Rplus_0_r.
  split.
  - apply Rlt_trans with 0; [lra|].
    now apply Rmult_lt_0_compat; [|apply bpow_gt_0].
287
  - apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|].
288 289 290 291 292
    bpow_simplify.
    rewrite Zrx2, Rplus_0_l in Hx'.
    apply (Rlt_le_trans _ _ _ (proj2 Hx')), Rmult_le_compat_l; [lra|].
    now apply bpow_le. }
(* 0 < rx2 *)
293 294
assert (Hl2 : mag rx2 = mag x :> Z).
{ now rewrite Hrx2r; apply mag_DN; [|rewrite <- Hrx2r]. }
295
assert (Hr12 : round beta fexp1 (Znearest choice1) rx2 = rx1).
296
{ unfold round, F2R, scaled_mantissa, cexp; simpl.
297 298 299
  rewrite Hl2; fold ex1.
  apply (Rmult_eq_reg_r (bpow (- ex1)));
    [|now apply Rgt_not_eq, bpow_gt_0]; bpow_simplify.
300
  unfold rx1, round, F2R, scaled_mantissa, cexp; simpl.
301 302 303 304 305 306 307
  fold ex1; bpow_simplify.
  apply f_equal, Znearest_imp.
  apply Rabs_lt; split.
  - apply Rlt_le_trans with 0; [lra|apply Rle_0_minus].
    now apply (Rmult_le_reg_r (bpow ex1)); bpow_simplify; [apply bpow_gt_0|].
  - apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
    rewrite Rmult_minus_distr_r; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
308
    change (IZR _ * _) with rx1.
309 310 311 312
    apply (Rplus_lt_reg_r rx1); ring_simplify.
    apply (Rlt_le_trans _ _ _ (proj2 Hrx2')), Rplus_le_compat_l.
    now apply Rmult_le_compat_l; [lra|right]. }
rewrite Hr12.
313
unfold rx1, round, F2R, scaled_mantissa, cexp; simpl; fold ex1.
314 315 316 317
apply Rmult_eq_compat_r, f_equal, eq_sym, Znearest_imp, Rabs_lt; split.
- apply Rlt_le_trans with 0; [lra|]; apply Rle_0_minus, Zfloor_lb.
- apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
  rewrite Rmult_minus_distr_r; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
318
  change (IZR _ * _) with rx1.
319 320 321 322 323 324 325 326 327
  now apply (Rplus_lt_reg_l rx1); ring_simplify.
Qed.

Lemma neq_midpoint_beta_odd_aux2 :
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  forall x,
  0 < x ->
328
  (fexp2 (mag x) < fexp1 (mag x))%Z ->
329
  midp beta fexp1 x < x <= midp beta fexp1 x + / 2 * ulp beta fexp2 x ->
330
  round_round_eq beta fexp1 fexp2 choice1 choice2 x.
331 332
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
333 334
unfold midp in Hx.
rewrite 2!ulp_neq_0 in Hx; try now apply Rgt_not_eq.
335
unfold round_round_eq.
336 337
set (ex1 := fexp1 (mag x)).
set (ex2 := fexp2 (mag x)).
338 339 340 341 342 343 344 345 346 347 348
set (rx1 := round beta fexp1 Zfloor x).
assert (Hbeta : (2 <= beta)%Z).
{ destruct beta as (beta_val,beta_prop).
  now apply Zle_bool_imp_le. }
destruct (generic_format_EM beta fexp2 x) as [F2x|NF2x].
{ (* generic_format beta fexp2 x *)
  now rewrite (round_generic _ fexp2); [|apply valid_rnd_N|]. }
(* ~ generic_format beta fexp2 x *)
assert (Nnrx1 : 0 <= rx1).
{ rewrite <- (round_0 beta fexp1 Zfloor).
  now apply round_le; [exact Vfexp1|apply valid_rnd_DN|apply Rlt_le]. }
Guillaume Melquiond's avatar
Guillaume Melquiond committed
349
assert (Hrx1 : rx1 = IZR (Zfloor (rx1 * bpow (- ex1))) * bpow ex1).
350
{ unfold rx1 at 2; unfold round, F2R, scaled_mantissa, cexp; simpl.
351
  unfold ex1; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
352
  now rewrite Zfloor_IZR. }
353
set (rx1c := round beta fexp1 Zceil x).
354
assert (Hf2f1' : (fexp2 (mag x) <= fexp1 (mag x))%Z) by omega.
355
assert (NF1x : ~ generic_format beta fexp1 x).
356
{ now intro H; apply NF2x, (generic_inclusion_mag _ fexp1). }
357
assert (Hrx1c : rx1c = rx1 + ulp beta fexp1 x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
358
{ now apply round_UP_DN_ulp. }
359
rewrite ulp_neq_0 in Hrx1c; try now apply Rgt_not_eq.
360 361
destruct (midpoint_beta_odd_remains rx1 Nnrx1 ex1 ex2 Hf2f1' Hrx1)
  as (rx2,(Nnrx2, (Hrx2, Hrx12))).
362
set (rx2c := rx2 + bpow (fexp2 (mag x))).
363
assert (Hx' : rx2c - / 2 * bpow ex2 < x <= rx2c).
364
{ unfold rx2c, cexp; fold ex1; fold ex2; split.
365 366 367 368
  - replace (_ - _) with (rx2 + / 2 * bpow ex2) by field.
    rewrite <- Hrx12; apply Hx.
  - replace (_ + _) with (rx2 + / 2 * bpow ex2 + / 2 * bpow ex2) by field.
    rewrite <- Hrx12; apply Hx. }
Guillaume Melquiond's avatar
Guillaume Melquiond committed
369
assert (Hrx2c : rx2c = IZR (Zfloor (rx2c * bpow (- ex2))) * bpow ex2).
370
{ unfold rx2c, ulp, cexp; fold ex2; rewrite Rmult_plus_distr_r.
371 372
  bpow_simplify.
  rewrite Hrx2 at 2; bpow_simplify.
373
  rewrite <- plus_IZR, Zfloor_IZR, plus_IZR; simpl.
374 375 376 377
  now rewrite Rmult_plus_distr_r; apply f_equal2; [|now rewrite Rmult_1_l]. }
assert (Prx2c : 0 < rx2c).
{ now apply Rplus_le_lt_0_compat; [|apply bpow_gt_0]. }
assert (Hr2 : round beta fexp2 (Znearest choice2) x = rx2c).
378
{ unfold round, F2R, scaled_mantissa, cexp; simpl; fold ex2.
379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
  apply (Rmult_eq_reg_r (bpow (- ex2))); [|now apply Rgt_not_eq, bpow_gt_0].
  bpow_simplify.
  rewrite (Znearest_imp _ _ (Zfloor (rx2c * bpow (- ex2)))).
  - now apply (Rmult_eq_reg_r (bpow ex2)); bpow_simplify;
    [apply eq_sym|apply Rgt_not_eq, bpow_gt_0].
  - apply Rabs_lt; split.
    + apply (Rmult_lt_reg_r (bpow ex2)); [now apply bpow_gt_0|].
      rewrite Rmult_minus_distr_r; bpow_simplify.
      rewrite <- Hrx2c.
      now apply (Rplus_lt_reg_l rx2c); ring_simplify.
    + apply Rle_lt_trans with 0; [|lra].
      apply Rle_minus.
      apply (Rmult_le_reg_r (bpow ex2)); [now apply bpow_gt_0|]; bpow_simplify.
      now rewrite <- Hrx2c. }
rewrite Hr2.
assert (Hrx2' : rx1c - / 2 * bpow ex1 < rx2c <= rx1c).
{ split.
396
  - rewrite Hrx1c; unfold ulp, cexp; fold ex1.
397 398 399
    replace (_ - _) with (rx1 + / 2 * bpow ex1) by field.
    apply (Rlt_le_trans _ _ _ (proj1 Hx) (proj2 Hx')).
  - apply (Rplus_le_reg_r (- / 2 * bpow ex2)).
400
    unfold rx2c, ulp, cexp; fold ex2.
401 402 403
    replace (_ + _) with (rx2 + / 2 * bpow ex2) by field.
    rewrite <- Hrx12.
    rewrite Hrx1c, Rplus_assoc; apply Rplus_le_compat_l.
404
    unfold ulp, cexp; fold ex1.
405 406 407 408
    apply (Rplus_le_reg_r (- / 2 * bpow ex1)); field_simplify.
    unfold Rdiv; apply Rmult_le_compat_r; [lra|].
    now apply Rle_0_minus, bpow_le. }
assert (Hr1 : round beta fexp1 (Znearest choice1) x = rx1c).
409
{ unfold rx1c, round, F2R, scaled_mantissa, cexp; simpl; fold ex1.
410 411 412
  apply Rmult_eq_compat_r, f_equal, Znearest_imp, Rabs_lt; split.
  - apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
    rewrite Rmult_minus_distr_r; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
413
    change (IZR _ * _) with rx1c.
414
    apply (Rplus_lt_reg_l rx1c); ring_simplify.
415
    rewrite Hrx1c; unfold ulp, cexp; fold ex1.
416 417 418 419 420 421
    now replace (_ - _) with (rx1 + / 2 * bpow ex1) by field.
  - apply Rlt_le_trans with 0; [|lra]; apply Rlt_minus.
    apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]; bpow_simplify.
    assert (H : x <= rx1c); [now apply round_UP_pt|].
    destruct H as [H|H]; [exact H|].
    casetype False; apply NF1x.
422
    unfold generic_format, F2R, scaled_mantissa, cexp; simpl; fold ex1.
423 424 425
    rewrite Ztrunc_floor;
      [|now apply Rmult_le_pos;[apply Rlt_le|apply bpow_ge_0]].
    rewrite H at 2.
426
    unfold rx1c, round, F2R, scaled_mantissa, cexp; simpl; fold ex1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
427
    now bpow_simplify; rewrite Zfloor_IZR; rewrite H at 1. }
428 429 430 431 432
rewrite Hr1.
destruct (Rle_or_lt rx1 0) as [Nprx1|Prx1].
{ (* rx1 = 0 *)
  assert (Zrx1 : rx1 = 0); [now apply Rle_antisym|].
  rewrite Hrx1c, Zrx1, Rplus_0_l.
433
  unfold rx2c, ulp, cexp; fold ex1; fold ex2.
434 435 436 437 438
  replace (_ + _) with (rx2 + / 2 * bpow ex2 + / 2 * bpow ex2) by field.
  rewrite <- Hrx12, Zrx1, Rplus_0_l.
  assert (Ph12 : 0 < / 2 * bpow ex1 + / 2 * bpow ex2).
  { now apply Rplus_lt_0_compat;
    (apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]). }
439 440
  assert (Hf1 : (fexp1 (mag x) <= mag x)%Z).
  { apply mag_ge_bpow.
441 442 443 444 445 446
    rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
    apply Rle_trans with (/ 2 * bpow ex1).
    - unfold Zminus; rewrite bpow_plus, Rmult_comm.
      fold ex1; apply Rmult_le_compat_r; [now apply bpow_ge_0|].
      rewrite bpow_opp; apply Rinv_le; [lra|].
      simpl; unfold Z.pow_pos; simpl; rewrite Zmult_1_r.
447
      now apply IZR_le.
448 449
    - apply Rlt_le.
      now rewrite <- (Rplus_0_l (_ * _)), <- Zrx1. }
450 451
  assert (Hl1 : mag (/ 2 * bpow ex1 + / 2 * bpow ex2) = mag x :> Z).
  { apply mag_unique; split.
452 453
    - rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
      apply Rle_trans with x.
454
      + destruct (mag x) as (ex, Hex); simpl.
455 456 457 458 459 460 461 462 463
        now rewrite <- (Rabs_right x);
          [apply Hex, Rgt_not_eq|apply Rle_ge, Rlt_le].
      + rewrite <- (Rplus_0_l (_ * _)), <- Zrx1.
        apply Hx.
    - rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
      apply Rlt_le_trans with (bpow ex1); [|now apply bpow_le].
      rewrite <- (Rmult_1_l (bpow ex1)) at 2.
      replace (1 * bpow ex1) with (/ 2 * bpow ex1 + / 2 * bpow ex1) by field.
      now apply Rplus_lt_compat_l, Rmult_lt_compat_l; [lra|apply bpow_lt]. }
464
  unfold round, F2R, scaled_mantissa, cexp; simpl; rewrite Hl1.
465 466
  fold ex1; apply (Rmult_eq_reg_r (bpow (- ex1)));
    [|now apply Rgt_not_eq, bpow_gt_0]; bpow_simplify.
467
  apply IZR_eq, Znearest_imp; simpl.
468 469 470 471 472 473 474 475 476 477 478 479
  apply Rabs_lt; simpl; split.
  - apply (Rplus_lt_reg_r 1); replace (- _ + _) with (/ 2) by field.
    ring_simplify; apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
    rewrite Rmult_plus_distr_r; bpow_simplify.
    rewrite <- (Rplus_0_r (_ * _)) at 1; apply Rplus_lt_compat_l.
    apply Rmult_lt_0_compat; [lra|apply bpow_gt_0].
  - apply (Rplus_lt_reg_r 1); ring_simplify.
    apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
    do 2 rewrite Rmult_plus_distr_r; bpow_simplify.
    now apply Rplus_lt_compat_l, Rmult_lt_compat;
      [lra|apply bpow_ge_0|lra|apply bpow_lt]. }
(* 0 < rx1 *)
480 481 482 483
assert (Hl1 : mag rx1 = mag x :> Z).
{ now apply mag_DN. }
assert (Hl2 : mag rx2c = mag x :> Z).
{ apply mag_unique; rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
484 485 486 487 488 489 490
  replace rx2c with (rx1 + (/ 2 * bpow ex1 + / 2 * bpow ex2));
    [|now rewrite <- Rplus_assoc, Hrx12;
       replace (_ + _) with (rx2 + bpow ex2) by field].
  split.
  - rewrite <- Rplus_assoc.
    apply Rle_trans with x; [|now apply Hx].
    apply Rge_le; rewrite <- (Rabs_right x) at 1; [|now apply Rle_ge, Rlt_le];
491
    apply Rle_ge; destruct (mag x) as (ex,Hex); simpl; apply Hex.
492 493 494 495 496 497
    now apply Rgt_not_eq.
  - apply Rlt_le_trans with (rx1 + bpow ex1).
    + apply Rplus_lt_compat_l.
      rewrite <- (Rmult_1_l (bpow ex1)) at 2.
      replace (1 * bpow ex1) with (/ 2 * bpow ex1 + / 2 * bpow ex1) by field.
      now apply Rplus_lt_compat_l, Rmult_lt_compat_l; [lra|apply bpow_lt].
498
    + unfold ex1; rewrite <- Hl1.
499
      fold (cexp beta fexp1 rx1); rewrite <- ulp_neq_0; try now apply Rgt_not_eq.
500
      apply id_p_ulp_le_bpow; [exact Prx1| |].
501
      * now apply generic_format_round; [|apply valid_rnd_DN].
502
      * destruct (mag rx1) as (erx1, Herx1); simpl.
503 504
        rewrite <- (Rabs_right rx1) at 1; [|now apply Rle_ge, Rlt_le].
        now apply Herx1, Rgt_not_eq. }
505
unfold round, F2R, scaled_mantissa, cexp; simpl.
506 507 508 509
rewrite Hl2; fold ex1.
apply (Rmult_eq_reg_r (bpow (- ex1)));
  [|now apply Rgt_not_eq, bpow_gt_0]; bpow_simplify.
rewrite Hrx1c, Rmult_plus_distr_r.
510
unfold rx1, round, F2R, scaled_mantissa, ulp, cexp; simpl; fold ex1.
511
bpow_simplify.
512
rewrite <- plus_IZR; apply f_equal, Znearest_imp.
513
apply Rabs_lt; split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
514
- rewrite plus_IZR; simpl; apply (Rplus_lt_reg_r 1); ring_simplify.
515 516 517
  replace (- _ + _) with (/ 2) by field.
  apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
  rewrite Rmult_minus_distr_r; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
518
  change (IZR _ * _) with rx1.
519 520 521 522
  apply (Rplus_lt_reg_l rx1); ring_simplify.
  apply Rlt_le_trans with x; [apply Hx|apply Hx'].
- apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|].
  rewrite Rmult_minus_distr_r; bpow_simplify.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
523 524
  rewrite plus_IZR, Rmult_plus_distr_r; simpl; rewrite Rmult_1_l.
  change (IZR _ * _ + _) with (rx1 + bpow (cexp beta fexp1 x)).
525 526 527 528 529 530 531 532 533 534
  rewrite <- Hrx1c; lra.
Qed.

(* neq_midpoint_beta_odd_aux{1,2} together *)
Lemma neq_midpoint_beta_odd_aux3 :
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  forall x,
  0 < x ->
535 536
  (fexp2 (mag x) <= fexp1 (mag x))%Z ->
  (fexp1 (mag x) <= mag x)%Z ->
537
  x <> midp beta fexp1 x ->
538
  round_round_eq beta fexp1 fexp2 choice1 choice2 x.
539 540 541 542
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx.
destruct (generic_format_EM beta fexp2 x) as [F2x|NF2x].
{ (* generic_format beta fexp2 x *)
543
  unfold round_round_eq.
544 545 546
  now rewrite (round_generic _ fexp2); [|apply valid_rnd_N|]. }
(* ~ generic_format beta fexp2 x *)
assert (NF1x : ~ generic_format beta fexp1 x).
547
{ now intro H; apply NF2x, (generic_inclusion_mag _ fexp1). }
548 549 550 551 552 553
destruct (Rle_or_lt x (midp beta fexp1 x)) as [H1|H1].
- (* x < midp fexp1 x *)
  assert (H1' : x < midp beta fexp1 x) by lra.
  destruct (Rlt_or_le x (midp beta fexp1 x - / 2 * ulp beta fexp2 x))
    as [H2|H2].
  + (* x < midp fexp1 x - / 2 * ulp beta fexp2 x *)
554
    now apply round_round_lt_mid.
555 556 557 558
  + (* midp fexp1 x - / 2 * ulp beta fexp2 x <= x *)
    now apply neq_midpoint_beta_odd_aux1; [| | | |split].
- (* midp fexp1 x < x *)
  assert (Hm : midp' beta fexp1 x = midp beta fexp1 x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
559
  { now unfold midp', midp; rewrite round_UP_DN_ulp; [field|]. }
560 561 562
  destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [H3|H3].
  + (* fexp2 (mag x) = fexp1 (mag x) *)
    assert (H3' : fexp2 (mag x) = fexp1 (mag x));
563
    [now apply Zle_antisym|].
564
    now apply round_round_gt_mid_same_place; [| | |rewrite Hm].
565
  + (* fexp2 (mag x) < fexp1 (mag x) *)
566 567 568
    destruct (Rlt_or_le (midp beta fexp1 x + / 2 * ulp beta fexp2 x) x)
      as [H2|H2].
    * (* midp fexp1 x + / 2 * ulp beta fexp2 x < x *)
569
      now apply round_round_gt_mid_further_place; [| | |omega| |rewrite Hm].
570
    * (* x <= midp fexp1 x + / 2 * ulp beta fexp2 x *)
571 572 573 574
      now apply neq_midpoint_beta_odd_aux2; [| | | |split].
Qed.

(* neq_midpoint_beta_odd_aux3 without the hypothesis
575
   fexp1 (mag x) <= mag x *)
576 577 578 579 580 581
Lemma neq_midpoint_beta_odd :
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  forall x,
  0 < x ->
582
  (fexp2 (mag x) <= fexp1 (mag x))%Z ->
583
  x <> midp beta fexp1 x ->
584
  round_round_eq beta fexp1 fexp2 choice1 choice2 x.
585 586
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
587 588
destruct (Zle_or_lt (fexp1 (mag x)) (mag x)) as [H1|H1].
{ (* fexp1 (mag x) <= mag x *)
589
  now apply neq_midpoint_beta_odd_aux3. }
590
(* mag x < fexp1 (mag x) *)
591
unfold round_round_eq.
592
revert Hf2f1 Hx H1.
593
destruct (mag x) as (ex,Hex); simpl.
594 595 596
specialize (Hex (Rgt_not_eq _ _ Px)).
intros Hf2f1 Hx H1.
rewrite Rabs_right in Hex; [|now apply Rle_ge, Rlt_le].
597
rewrite (round_N_small_pos _ fexp1 _ x ex Hex H1).
598 599 600
destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
- (* fexp1 ex = fexp2 ex *)
  replace (fexp1 ex) with (fexp2 ex) in H1; [|now apply Zle_antisym].
601
  rewrite (round_N_small_pos _ fexp2 _ x ex Hex H1).
602
  now rewrite round_0; [|apply valid_rnd_N].
603
- (* fexp2 (mag x) < fexp1 (mag x) *)
604 605 606 607 608 609
  set (r2 := round beta fexp2 (Znearest choice2) x).
  destruct (Req_dec r2 0) as [Zr2|Nzr2].
  { (* r2 = 0 *)
    now rewrite Zr2, round_0; [|apply valid_rnd_N]. }
  (* r2 <> 0 *)
  assert (B1 : Rabs (r2 - x) <= / 2 * ulp beta fexp2 x);
BOLDO Sylvie's avatar
BOLDO Sylvie committed
610
    [now apply error_le_half_ulp|].
611
  rewrite ulp_neq_0 in B1; try now apply Rgt_not_eq.
612
  unfold round, F2R, scaled_mantissa, cexp; simpl.
613
  apply (Rmult_eq_reg_r (bpow (- fexp1 (mag r2))));
614 615
    [|now apply Rgt_not_eq, bpow_gt_0].
  rewrite Rmult_0_l; bpow_simplify.
616
  apply IZR_eq, Znearest_imp.
617 618
  simpl; unfold Rminus; rewrite Ropp_0, Rplus_0_r.
  rewrite Rabs_mult, (Rabs_right (bpow _)); [|now apply Rle_ge, bpow_ge_0].
619
  apply (Rmult_lt_reg_r (bpow (fexp1 (mag r2)))); [now apply bpow_gt_0|].
620 621 622
  bpow_simplify.
  replace r2 with (r2 - x + x) by ring.
  apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)).
623
  apply Rlt_le_trans with (/ 2 * bpow (cexp beta fexp2 x) + bpow ex);
624 625 626 627 628 629
    [now apply Rplus_le_lt_compat;
      [|rewrite Rabs_right; [|apply Rle_ge, Rlt_le]]|].
  replace (_ - _ + _) with r2 by ring.
  assert (Hbeta : (2 <= beta)%Z).
  { destruct beta as (beta_val,beta_prop).
    now apply Zle_bool_imp_le. }
630 631
  assert (Hex' : mag x = ex :> Z).
  { now apply mag_unique;
632
    rewrite Rabs_right; [|apply Rle_ge, Rlt_le]. }
633 634
  assert (Hl2 : (mag r2 <= fexp1 ex)%Z).
  { apply (mag_le_bpow _ _ _ Nzr2).
635 636
    replace r2 with (r2 - x + x) by ring.
    apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)).
637
    apply Rlt_le_trans with (/ 2 * bpow (cexp beta fexp2 x) + bpow ex);
638 639 640
      [now apply Rplus_le_lt_compat;
        [|rewrite Rabs_right; [|apply Rle_ge, Rlt_le]]|].
    apply Rle_trans with (2 * bpow (fexp1 ex - 1)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
641
    - replace (2 * bpow (fexp1 ex - 1)) with (bpow (fexp1 ex - 1) + bpow (fexp1 ex - 1)) by ring.
642 643
      apply Rplus_le_compat; [|now apply bpow_le; omega].
      apply Rle_trans with (bpow (fexp2 ex)); [|now apply bpow_le; omega].
644
      rewrite <- (Rmult_1_l (bpow (fexp2 _))); unfold cexp.
645 646 647 648 649 650 651
      rewrite Hex'; apply Rmult_le_compat_r; [apply bpow_ge_0|lra].
    - rewrite <- (Rmult_1_l (bpow (fexp1 _))).
      unfold Zminus; rewrite Zplus_comm, bpow_plus, <- Rmult_assoc.
      apply Rmult_le_compat_r; [now apply bpow_ge_0|].
      apply (Rmult_le_reg_r (bpow 1)); [now apply bpow_gt_0|].
      rewrite Rmult_1_l; bpow_simplify.
      simpl; unfold Z.pow_pos; simpl; rewrite Zmult_1_r.
652
      now apply IZR_le. }
653
  assert (Hf1r2 : fexp1 (mag r2) = fexp1 ex).
654 655 656 657 658
  { now apply (proj2 (Vfexp1 ex)); [omega|]. }
  rewrite Hf1r2.
  replace (bpow ex) with (/ 2 * (2 * bpow ex)) by field.
  rewrite <- Rmult_plus_distr_l; apply Rmult_le_compat_l; [lra|].
  apply Rle_trans with (3 * bpow (fexp1 ex - 1)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
659 660
  + replace (3 * bpow (fexp1 ex - 1)) with (bpow (fexp1 ex - 1) + 2 * bpow (fexp1 ex - 1)) by ring.
    apply Rplus_le_compat.
661
    * apply bpow_le; unfold cexp; rewrite Hex'; omega.
662 663 664 665 666 667 668
    * apply Rmult_le_compat_l; [lra|]; apply bpow_le; omega.
  + rewrite <- (Rmult_1_l (bpow (fexp1 _))).
    unfold Zminus; rewrite Zplus_comm, bpow_plus, <- Rmult_assoc.
    apply Rmult_le_compat_r; [now apply bpow_ge_0|].
    apply (Rmult_le_reg_r (bpow 1)); [now apply bpow_gt_0|].
    rewrite Rmult_1_l; bpow_simplify.
    simpl; unfold Z.pow_pos; simpl; rewrite Zmult_1_r.
669
    apply IZR_le.
670 671 672 673 674 675 676 677
    destruct (Zle_or_lt beta 2) as [Hb2|Hb2]; [|omega].
    assert (Hbeta' : beta = 2%Z :> Z); [now apply Zle_antisym|].
    casetype False.
    rewrite <- Zodd_ex_iff in Obeta.
    apply (Zodd_not_Zeven _ Obeta).
    now rewrite Hbeta'.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
678
(* argh: was 0 <= IZR mx. This becomes incorrect in FLX with the new ulp. *)
679 680 681
Lemma float_neq_midpoint_beta_odd :
  forall (mx ex : Z),
  forall (fexp : Z -> Z),
Guillaume Melquiond's avatar
Guillaume Melquiond committed
682 683
  0 < IZR mx ->
  IZR mx * bpow ex <> midp beta fexp (IZR mx * bpow ex).
684 685
Proof.
intros mx ex fexp Hmx.
686
unfold midp; rewrite ulp_neq_0.
687
unfold round, F2R, scaled_mantissa, cexp; simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
688 689
set (exf := fexp (mag (IZR mx * bpow ex))).
set (mxf := Zfloor (IZR mx * bpow ex * bpow (- exf))).
690 691 692 693 694
destruct (Zle_or_lt exf ex) as [Hm|Hm].
- (* exf <= ex *)
  replace ex with (ex - exf + exf)%Z by ring.
  rewrite bpow_plus.
  intro H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
695
  apply (Rplus_eq_compat_l (- IZR mxf * bpow exf)) in H.
696 697
  revert H.
  rewrite <- Rmult_assoc, <- Rmult_plus_distr_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
698
  rewrite <- (IZR_Zpower _ (_ - _)); [|now apply Zle_minus_le_0].
699 700 701
  intro H.
  ring_simplify in H.
  rewrite <- Rmult_plus_distr_r in H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
702
  rewrite <- opp_IZR, <- mult_IZR, <- plus_IZR, Rmult_comm in H.
703 704 705
  apply Rmult_eq_reg_l in H; [|now apply Rgt_not_eq, bpow_gt_0].
  apply (Rmult_eq_compat_l 2) in H.
  revert H.
706 707
  rewrite <- mult_IZR, Rinv_r; [|lra].
  apply IZR_neq.
708 709 710 711 712
  intro H.
  apply (Zodd_not_Zeven 1); [now simpl|].
  rewrite <- H.
  now apply Zeven_mult_Zeven_l.
- assert (Hm' : (ex <= exf)%Z) by omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
713
  assert (Nnmxy : 0 <= IZR mxf * bpow exf).
714
  { apply Rmult_le_pos; [|now apply bpow_ge_0].
715
    apply IZR_le; unfold mxf.
716 717
    apply Zfloor_lub; simpl.
    apply Rmult_le_pos; [|now apply bpow_ge_0].
718
    now apply Rmult_le_pos; [now left|apply bpow_ge_0]. }
719 720
  destruct (midpoint_beta_odd_remains _ Nnmxy _ _ Hm')
    as (x',(_,(Hx',Hxx'))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
721
  { now bpow_simplify; rewrite Zfloor_IZR. }
722 723 724
  rewrite Hxx', Hx'.
  set (mx' := Zfloor (x' * bpow (- ex))).
  intro H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
725
  apply (Rplus_eq_compat_l (- IZR mx' * bpow ex)) in H.
726 727 728 729 730
  revert H.
  rewrite <- Rmult_plus_distr_r.
  intro H.
  ring_simplify in H.
  rewrite <- Rmult_plus_distr_r in H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
731
  rewrite <- opp_IZR, <- plus_IZR, Rmult_comm in H.
732 733 734
  apply Rmult_eq_reg_l in H; [|now apply Rgt_not_eq, bpow_gt_0].
  apply (Rmult_eq_compat_l 2) in H.
  revert H.
735 736
  rewrite <- mult_IZR, Rinv_r; [|lra].
  apply IZR_neq.
737 738 739 740
  intro H.
  apply (Zodd_not_Zeven 1); [now simpl|].
  rewrite <- H.
  now apply Zeven_mult_Zeven_l.
741 742 743
- apply Rmult_integral_contrapositive_currified.
  now apply Rgt_not_eq, Rlt_gt.
  apply Rgt_not_eq, bpow_gt_0.
744 745 746 747
Qed.

Section Double_round_mult_beta_odd.

748
Lemma round_round_mult_beta_odd_aux1 :
749 750 751 752 753 754 755
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  (forall ex, (fexp2 ex <= fexp1 ex)%Z) ->
  forall x y,
  0 < x -> 0 < y ->
  generic_format beta fexp1 x -> generic_format beta fexp1 y ->
756
  round_round_eq beta fexp1 fexp2 choice1 choice2 (x * y).
757 758 759 760 761 762 763
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hfexp x y Px Py Fx Fy.
apply neq_midpoint_beta_odd; try assumption.
- now apply Rmult_lt_0_compat.
- apply Hfexp.
- intro Hxy.
  revert Fx Fy.
764
  unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
765 766 767 768
  set (mx := Ztrunc (x * bpow (- fexp1 (mag x)))).
  set (my := Ztrunc (y * bpow (- fexp1 (mag y)))).
  set (ex := mag x).
  set (ey := mag y).
769 770 771 772
  intros Fx Fy.
  revert Hxy.
  rewrite Fx, Fy.
  replace (_ * _)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
773 774
  with (IZR mx * IZR my * bpow (fexp1 ex) * bpow (fexp1 ey)) by ring.
  rewrite <- mult_IZR, Rmult_assoc, <- bpow_plus.
775
  apply float_neq_midpoint_beta_odd.
776 777
  apply (Rmult_lt_reg_r (bpow (fexp1 ex))); [now apply bpow_gt_0|].
  apply (Rmult_lt_reg_r (bpow (fexp1 ey))); [now apply bpow_gt_0|].
778
  do 2 rewrite Rmult_0_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
779
  rewrite mult_IZR;
780
    replace (_ * _)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
781
    with (IZR mx * bpow (fexp1 ex) * (IZR my * bpow (fexp1 ey))) by ring.
782
  rewrite <- Fx, <- Fy.
783
  now apply Rmult_lt_0_compat.
784 785
Qed.

786
Lemma round_round_mult_beta_odd_aux2 :
787 788 789 790 791 792 793
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  (forall ex, (fexp2 ex <= fexp1 ex)%Z) ->
  forall x y,
  0 <= x -> 0 <= y ->
  generic_format beta fexp1 x -> generic_format beta fexp1 y ->
794
  round_round_eq beta fexp1 fexp2 choice1 choice2 (x * y).
795 796 797 798
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hfexp x y Nnx Nny Fx Fy.
destruct (Req_dec x 0) as [Zx|Nzx].
- (* x = 0 *)
799
  unfold round_round_eq.
800 801 802 803 804
  now rewrite Zx, Rmult_0_l, round_0; [|apply valid_rnd_N].
- (* 0 < x *)
  assert (Px : 0 < x); [lra|].
  destruct (Req_dec y 0) as [Zy|Nzy].
  + (* y = 0 *)
805
    unfold round_round_eq.
806 807 808
    now rewrite Zy, Rmult_0_r, round_0; [|apply valid_rnd_N].
  + (* 0 < y *)
    assert (Py : 0 < y); [lra|].
809
    now apply round_round_mult_beta_odd_aux1.
810 811
Qed.

812
Lemma round_round_mult_beta_odd :
813 814 815 816 817 818
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  (forall ex, (fexp2 ex <= fexp1 ex)%Z) ->
  forall x y,
  generic_format beta fexp1 x -> generic_format beta fexp1 y ->
819
  round_round_eq beta fexp1 fexp2 choice1 choice2 (x * y).
820 821
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Fx Fy.
822
unfold round_round_eq.
823 824 825 826 827 828 829
destruct (Rlt_or_le x 0) as [Sx|Sx]; destruct (Rlt_or_le y 0) as [Sy|Sy].
- (* x < 0, y < 0 *)
  replace (x * y) with ((- x) * (- y)); [|ring].
  assert (Px : 0 <= - x); [lra|].
  assert (Py : 0 <= - y); [lra|].
  apply generic_format_opp in Fx.
  apply generic_format_opp in Fy.
830
  now apply round_round_mult_beta_odd_aux2.
831 832 833 834 835 836
- (* x < 0, 0 <= y *)
  replace (x * y) with (- ((- x) * y)); [|ring].
  assert (Px : 0 <= - x); [lra|].
  apply generic_format_opp in Fx.
  do 3 rewrite round_N_opp.
  apply Ropp_eq_compat.
837
  now apply round_round_mult_beta_odd_aux2.
838 839 840 841 842 843
- (* 0 <= x, y < 0 *)
  replace (x * y) with (- (x * (- y))); [|ring].
  assert (Py : 0 <= - y); [lra|].
  apply generic_format_opp in Fy.
  do 3 rewrite round_N_opp.
  apply Ropp_eq_compat.
844
  now apply round_round_mult_beta_odd_aux2.
845
- (* 0 <= x, 0 <= y *)
846
  now apply round_round_mult_beta_odd_aux2.
847 848 849 850 851 852 853 854 855 856
Qed.

Section Double_round_mult_beta_odd_FLX.

Variable prec : Z.
Variable prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

857
Theorem round_round_mult_beta_odd_FLX :
858 859 860 861
  forall choice1 choice2,
  (prec <= prec')%Z ->
  forall x y,
  FLX_format beta prec x -> FLX_format beta prec y ->
862
  round_round_eq beta (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x * y).
863 864
Proof.
intros choice1 choice2 Hprec x y Fx Fy.
865
apply round_round_mult_beta_odd.
866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882
- now apply FLX_exp_valid.
- now apply FLX_exp_valid.
- intro ex; unfold FLX_exp; omega.
- now apply generic_format_FLX.
- now apply generic_format_FLX.
Qed.

End Double_round_mult_beta_odd_FLX.

Section Double_round_mult_beta_odd_FLT.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

883
Theorem round_round_mult_beta_odd_FLT :
884 885 886 887
  forall choice1 choice2,
  (emin' <= emin)%Z -> (prec <= prec')%Z ->
  forall x y,
  FLT_format beta emin prec x -> FLT_format beta emin prec y ->
888
  round_round_eq beta (FLT_exp emin prec) (FLT_exp emin' prec')
889 890 891
                  choice1 choice2 (x * y).
Proof.
intros choice1 choice2 Hemin Hprec x y Fx Fy.
892
apply round_round_mult_beta_odd.
893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912
- now apply FLT_exp_valid.
- now apply FLT_exp_valid.
- intro ex; unfold FLT_exp.
  generalize (Zmax_spec (ex - prec) emin).
  generalize (Zmax_spec (ex - prec') emin').
  omega.
- now apply generic_format_FLT.
- now apply generic_format_FLT.
Qed.

End Double_round_mult_beta_odd_FLT.

Section Double_round_mult_beta_odd_FTZ.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

913
Theorem round_round_mult_beta_odd_FTZ :
914 915 916 917
  forall choice1 choice2,
  (emin' + prec' <= emin + prec)%Z -> (prec <= prec')%Z ->
  forall x y,
  FTZ_format beta emin prec x -> FTZ_format beta emin prec y ->
918
  round_round_eq beta (FTZ_exp emin prec) (FTZ_exp emin' prec')
919 920 921
                  choice1 choice2 (x * y).
Proof.
intros choice1 choice2 Hemin Hprec x y Fx Fy.
922
apply round_round_mult_beta_odd.
923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939
- now apply FTZ_exp_valid.
- now apply FTZ_exp_valid.
- intro ex; unfold FTZ_exp.
  unfold Prec_gt_0 in prec_gt_0_.
  destruct (Z.ltb_spec (ex - prec') emin');
  destruct (Z.ltb_spec (ex - prec) emin);
  omega.
- now apply generic_format_FTZ.
- now apply generic_format_FTZ.
Qed.

End Double_round_mult_beta_odd_FTZ.

End Double_round_mult_beta_odd.

Section Double_round_plus_beta_odd.

940
Lemma round_round_plus_beta_odd_aux1 :
941 942 943 944 945 946 947
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  (forall ex, (fexp2 ex <= fexp1 ex)%Z) ->
  forall x y,
  0 < x -> 0 < y ->
  generic_format beta fexp1 x -> generic_format beta fexp1 y ->
948
  round_round_eq beta fexp1 fexp2 choice1 choice2 (x + y).
949 950 951 952 953 954 955
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hfexp x y Px Py Fx Fy.
apply neq_midpoint_beta_odd; try assumption.
- now apply Rplus_lt_0_compat.
- apply Hfexp.
- intro Hxy.
  revert Fx Fy.
956
  unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
957 958 959 960
  set (mx := Ztrunc (x * bpow (- fexp1 (mag x)))).
  set (my := Ztrunc (y * bpow (- fexp1 (mag y)))).
  set (ex := mag x).
  set (ey := mag y).
961 962 963 964 965 966
  intros Fx Fy.
  revert Hxy.
  rewrite Fx, Fy.
  destruct (Zle_or_lt (fexp1 ex) (fexp1 ey)) as [Hexy|Hexy].
  + replace (fexp1 ey) with (fexp1 ey - fexp1 ex + fexp1 ex)%Z by ring.
    rewrite bpow_plus, <- Rmult_assoc, <- Rmult_plus_distr_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
967 968
    rewrite <- IZR_Zpower; [|now apply Zle_minus_le_0].
    rewrite <- mult_IZR, <- plus_IZR.
969
    apply float_neq_midpoint_beta_odd.
970
    apply (Rmult_lt_reg_r (bpow (fexp1 ex))); [now apply bpow_gt_0|].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
971
    rewrite plus_IZR, mult_IZR, IZR_Zpower; [|now apply Zle_minus_le_0].
972 973
    rewrite Rmult_0_l, Rmult_plus_distr_r; bpow_simplify.
    rewrite <- Fx, <- Fy.
974
    now apply Rplus_lt_0_compat.
975 976
  + replace (fexp1 ex) with (fexp1 ex - fexp1 ey + fexp1 ey)%Z by ring.
    rewrite bpow_plus, <- Rmult_assoc, <- Rmult_plus_distr_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
977 978
    rewrite <- IZR_Zpower; [|omega].
    rewrite <- mult_IZR, <- plus_IZR.
979
    apply float_neq_midpoint_beta_odd.
980
    apply (Rmult_lt_reg_r (bpow (fexp1 ey))); [now apply bpow_gt_0|].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
981
    rewrite plus_IZR, mult_IZR, IZR_Zpower; [|omega].
982 983
    rewrite Rmult_0_l, Rmult_plus_distr_r; bpow_simplify.
    rewrite <- Fx, <- Fy.
984
    now apply Rplus_lt_0_compat.
985 986
Qed.

987
Lemma round_round_plus_beta_odd_aux2 :
988 989 990 991 992 993 994
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  (forall ex, (fexp2 ex <= fexp1 ex)%Z) ->
  forall x y,
  0 <= x -> 0 <= y ->
  generic_format beta fexp1 x -> generic_format beta fexp1 y ->
995
  round_round_eq beta fexp1 fexp2 choice1 choice2 (x + y).
996 997 998 999
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hfexp x y Nnx Nny Fx Fy.
destruct (Req_dec x 0) as [Zx|Nzx]; destruct (Req_dec y 0) as [Zy|Nzy].
- (* x = 0, y = 0 *)
1000
  unfold round_round_eq.
1001 1002 1003 1004 1005 1006 1007
  now rewrite Zx, Zy, Rplus_0_l, round_0; [|apply valid_rnd_N].
- (* x = 0, 0 < y *)
  assert (Py : 0 < y); [lra|].
  rewrite Zx, Rplus_0_l.
  apply (neq_midpoint_beta_odd _ _ Vfexp1 Vfexp2 _ _ _ Py (Hfexp _)).
  rewrite Fy; unfold F2R, scaled_mantissa; simpl.
  apply float_neq_midpoint_beta_odd.
1008
  apply Rmult_lt_reg_r with (bpow (cexp beta fexp1 y)).
1009 1010 1011 1012
  apply bpow_gt_0.
  rewrite Rmult_0_l.
  apply Rlt_le_trans with (1:=Py).
  right; rewrite Fy at 1; unfold F2R, scaled_mantissa; now simpl.
1013 1014 1015 1016 1017 1018
- (* 0 < x, y = 0 *)
  assert (Px : 0 < x); [lra|].
  rewrite Zy, Rplus_0_r.
  apply (neq_midpoint_beta_odd _ _ Vfexp1 Vfexp2 _ _ _ Px (Hfexp _)).
  rewrite Fx; unfold F2R, scaled_mantissa; simpl.
  apply float_neq_midpoint_beta_odd.
1019
  apply Rmult_lt_reg_r with (bpow (cexp beta fexp1 x)).
1020 1021 1022 1023
  apply bpow_gt_0.
  rewrite Rmult_0_l.
  apply Rlt_le_trans with (1:=Px).
  right; rewrite Fx at 1; unfold F2R, scaled_mantissa; now simpl.
1024 1025 1026
- (* 0 < x, 0 < y *)
  assert (Px : 0 < x); [lra|].
  assert (Py : 0 < y); [lra|].
1027
  now apply round_round_plus_beta_odd_aux1.
1028 1029
Qed.

1030
Lemma round_round_minus_beta_odd_aux1 :
1031 1032 1033 1034 1035 1036 1037
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  (forall ex, (fexp2 ex <= fexp1 ex)%Z) ->
  forall x y,
  0 < x -> 0 < y -> y < x ->
  generic_format beta fexp1 x -> generic_format beta fexp1 y ->
1038
  round_round_eq beta fexp1 fexp2 choice1 choice2 (x - y).
1039 1040 1041 1042 1043 1044 1045
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hfexp x y Px Py Hxy Fx Fy.
apply neq_midpoint_beta_odd; try assumption.
- now apply Rlt_Rminus.
- apply Hfexp.
- intro Hxy'.
  revert Fx Fy.
1046
  unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
1047 1048 1049 1050
  set (mx := Ztrunc (x * bpow (- fexp1 (mag x)))).
  set (my := Ztrunc (y * bpow (- fexp1 (mag y)))).
  set (ex := mag x).
  set (ey := mag y).
1051 1052 1053 1054 1055 1056
  intros Fx Fy.
  revert Hxy'.
  rewrite Fx, Fy.
  destruct (Zle_or_lt (fexp1 ex) (fexp1 ey)) as [Hexy|Hexy].
  + replace (fexp1 ey) with (fexp1 ey - fexp1 ex + fexp1 ex)%Z by ring.
    rewrite bpow_plus, <- Rmult_assoc, <- Rmult_minus_distr_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1057 1058
    rewrite <- IZR_Zpower; [|now apply Zle_minus_le_0].
    rewrite <- mult_IZR, <- minus_IZR.
1059
    apply float_neq_midpoint_beta_odd.
1060
    apply (Rmult_lt_reg_r (bpow (fexp1 ex))); [now apply bpow_gt_0|].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1061
    rewrite minus_IZR, mult_IZR, IZR_Zpower; [|now apply Zle_minus_le_0].
1062 1063
    rewrite Rmult_0_l, Rmult_minus_distr_r; bpow_simplify.
    rewrite <- Fx, <- Fy.
1064
    now apply Rlt_Rminus.
1065 1066
  + replace (fexp1 ex) with (fexp1 ex - fexp1 ey + fexp1 ey)%Z by ring.
    rewrite bpow_plus, <- Rmult_assoc, <- Rmult_minus_distr_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1067 1068
    rewrite <- IZR_Zpower; [|omega].
    rewrite <- mult_IZR, <- minus_IZR.
1069
    apply float_neq_midpoint_beta_odd.
1070
    apply (Rmult_lt_reg_r (bpow (fexp1 ey))); [now apply bpow_gt_0|].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1071
    rewrite minus_IZR, mult_IZR, IZR_Zpower; [|omega].
1072 1073
    rewrite Rmult_0_l, Rmult_minus_distr_r; bpow_simplify.
    rewrite <- Fx, <- Fy.
1074
    now apply Rlt_Rminus.
1075 1076
Qed.

1077
Lemma round_round_minus_beta_odd_aux2 :
1078 1079 1080 1081 1082 1083 1084
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  (forall ex, (fexp2 ex <= fexp1 ex)%Z) ->
  forall x y,
  0 <= x -> 0 <= y ->
  generic_format beta fexp1 x -> generic_format beta fexp1 y ->
1085
  round_round_eq beta fexp1 fexp2 choice1 choice2 (x - y).
1086 1087 1088 1089
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hfexp x y Nnx Nny Fx Fy.
destruct (Req_dec x 0) as [Zx|Nzx]; destruct (Req_dec y 0) as [Zy|Nzy].
- (* x = 0, y = 0 *)
1090
  unfold round_round_eq.
1091 1092 1093 1094 1095
  unfold Rminus.
  now rewrite Zx, Zy, Rplus_0_l, Ropp_0, round_0; [|apply valid_rnd_N].
- (* x = 0, 0 < y *)
  assert (Py : 0 < y); [lra|].
  unfold Rminus; rewrite Zx, Rplus_0_l.
1096
  unfold round_round_eq; do 3 rewrite round_N_opp; apply f_equal.
1097 1098 1099
  apply (neq_midpoint_beta_odd _ _ Vfexp1 Vfexp2 _ _ _ Py (Hfexp _)).
  rewrite Fy; unfold F2R, scaled_mantissa; simpl.
  apply float_neq_midpoint_beta_odd.
1100
  apply Rmult_lt_reg_r with (bpow (cexp beta fexp1 y)).
1101 1102 1103
  apply bpow_gt_0.
  rewrite Rmult_0_l; apply Rlt_le_trans with (1:=Py).
  right; rewrite Fy at 1; unfold F2R, scaled_mantissa; now simpl.
1104 1105 1106 1107 1108 1109
- (* 0 < x, y = 0 *)
  assert (Px : 0 < x); [lra|].
  unfold Rminus; rewrite Zy, Ropp_0, Rplus_0_r.
  apply (neq_midpoint_beta_odd _ _ Vfexp1 Vfexp2 _ _ _ Px (Hfexp _)).
  rewrite Fx; unfold F2R, scaled_mantissa; simpl.
  apply float_neq_midpoint_beta_odd.
1110
  apply Rmult_lt_reg_r with (bpow (cexp beta fexp1 x)).
1111 1112 1113
  apply bpow_gt_0.
  rewrite Rmult_0_l; apply Rlt_le_trans with (1:=Px).
  right; rewrite Fx at 1; unfold F2R, scaled_mantissa; now simpl.
1114 1115 1116 1117 1118
- (* 0 < x, 0 < y *)
  assert (Px : 0 < x); [lra|].
  assert (Py : 0 < y); [lra|].
  destruct (Rtotal_order x y) as [Hxy|[Hxy|Hxy]].
  + replace (x - y) with (- (y - x)) by ring.
1119 1120 1121
    unfold round_round_eq; do 3 rewrite round_N_opp; apply f_equal.
    now apply round_round_minus_beta_odd_aux1.
  + unfold round_round_eq.
1122
    now rewrite (Rminus_diag_eq _ _ Hxy), round_0; [|apply valid_rnd_N].
1123
  + now apply round_round_minus_beta_odd_aux1.
1124 1125
Qed.

1126
Lemma round_round_plus_beta_odd :
1127 1128 1129 1130 1131 1132
  forall (fexp1 fexp2 : Z -> Z),
  Valid_exp fexp1 -> Valid_exp fexp2 ->
  forall (choice1 choice2 : Z -> bool),
  (forall ex, (fexp2 ex <= fexp1 ex)%Z) ->
  forall x y,
  generic_format beta fexp1 x -> generic_format beta fexp1 y ->
1133
  round_round_eq beta fexp1 fexp2 choice1 choice2 (x + y).
1134 1135
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Fx Fy.
1136
unfold round_round_eq.
1137 1138 1139 1140 1141 1142 1143 1144
destruct (Rlt_or_le x 0) as [Sx|Sx]; destruct (Rlt_or_le y 0) as [Sy|Sy].
- (* x < 0, y < 0 *)
  replace (x + y) with (- ((- x) + (- y))); [|ring].
  assert (Px : 0 <= - x); [lra|].
  assert (Py : 0 <= - y); [lra|].
  do 3 rewrite round_N_opp; apply f_equal.
  apply generic_format_opp in Fx.
  apply generic_format_opp in Fy.
1145
  now apply round_round_plus_beta_odd_aux2.
1146 1147 1148 1149 1150
- (* x < 0, 0 <= y *)
  replace (x + y) with (- ((- x) - y)); [|ring].
  assert (Px : 0 <= - x); [lra|].
  apply generic_format_opp in Fx.
  do 3 rewrite round_N_opp; apply f_equal.
1151
  now apply round_round_minus_beta_odd_aux2.
1152 1153 1154 1155
- (* 0 <= x, y < 0 *)
  replace (x + y) with (x - (- y)); [|ring].
  assert (Py : 0 <= - y); [lra|].
  apply generic_format_opp in Fy.
1156
  now