Library Flocq.Prop.Double_rounding

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2014-2018 Sylvie Boldo
Copyright (C) 2014-2018 Guillaume Melquiond
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.

Conditions for innocuous double rounding.


Require Import Psatz.
Require Import Raux Defs Generic_fmt Operations Ulp FLX FLT FTZ.

Open Scope R_scope.

Section Double_round.

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

Definition round_round_eq fexp1 fexp2 choice1 choice2 x :=
  round beta fexp1 (Znearest choice1) (round beta fexp2 (Znearest choice2) x)
  = round beta fexp1 (Znearest choice1) x.

A little tactic to simplify terms of the form bpow a × bpow b.
Ltac bpow_simplify :=
  
  repeat
    match goal with
      | |- context [(Raux.bpow _ _ × Raux.bpow _ _)] ⇒
        rewrite <- bpow_plus
      | |- context [(?X1 × Raux.bpow _ _ × Raux.bpow _ _)] ⇒
        rewrite (Rmult_assoc X1); rewrite <- bpow_plus
      | |- context [(?X1 × (?X2 × Raux.bpow _ _) × Raux.bpow _ _)] ⇒
        rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
        rewrite <- bpow_plus
    end;
  
  repeat
    match goal with
      | |- context [(Raux.bpow _ ?X)] ⇒
        progress ring_simplify X
    end;
  
  change (Raux.bpow _ 0) with 1;
  repeat
    match goal with
      | |- context [(_ × 1)] ⇒
        rewrite Rmult_1_r
    end.

Definition midp (fexp : Z Z) (x : R) :=
  round beta fexp Zfloor x + / 2 × ulp beta fexp x.

Definition midp' (fexp : Z Z) (x : R) :=
  round beta fexp Zceil x - / 2 × ulp beta fexp x.

Lemma round_round_lt_mid_further_place' :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x) - 1)%Z
  x < bpow (mag x) - / 2 × ulp beta fexp2 x
  x < midp fexp1 x - / 2 × ulp beta fexp2 x
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_lt_mid_further_place :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x) - 1)%Z
  (fexp1 (mag x) mag x)%Z
  x < midp fexp1 x - / 2 × ulp beta fexp2 x
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_lt_mid_same_place :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) = fexp1 (mag x))%Z
  x < midp fexp1 x
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_lt_mid :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x))%Z
  (fexp1 (mag x) mag x)%Z
  x < midp fexp1 x
  ((fexp2 (mag x) fexp1 (mag x) - 1)%Z
   x < midp fexp1 x - / 2 × ulp beta fexp2 x)
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_gt_mid_further_place' :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x) - 1)%Z
  round beta fexp2 (Znearest choice2) x < bpow (mag x)
  midp' fexp1 x + / 2 × ulp beta fexp2 x < x
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_gt_mid_further_place :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x) - 1)%Z
  (fexp1 (mag x) mag x)%Z
  midp' fexp1 x + / 2 × ulp beta fexp2 x < x
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_gt_mid_same_place :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) = fexp1 (mag x))%Z
  midp' fexp1 x < x
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_gt_mid :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x))%Z
  (fexp1 (mag x) mag x)%Z
  midp' fexp1 x < x
  ((fexp2 (mag x) fexp1 (mag x) - 1)%Z
   midp' fexp1 x + / 2 × ulp beta fexp2 x < x)
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Section Double_round_mult.

Lemma mag_mult_disj :
   x y,
  x 0 y 0
  ((mag (x × y) = (mag x + mag y - 1)%Z :> Z)
    (mag (x × y) = (mag x + mag y)%Z :> Z)).

Definition round_round_mult_hyp fexp1 fexp2 :=
  ( ex ey, (fexp2 (ex + ey) fexp1 ex + fexp1 ey)%Z)
   ( ex ey, (fexp2 (ex + ey - 1) fexp1 ex + fexp1 ey)%Z).

Lemma round_round_mult_aux :
   (fexp1 fexp2 : Z Z),
  round_round_mult_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x × y).

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem round_round_mult :
   (fexp1 fexp2 : Z Z),
  round_round_mult_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x generic_format beta fexp1 y
  round beta fexp1 rnd (round beta fexp2 rnd (x × y))
  = round beta fexp1 rnd (x × y).

Section Double_round_mult_FLX.

Variable prec : Z.
Variable prec' : Z.

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

Theorem round_round_mult_FLX :
  (2 × prec prec')%Z
   x y,
  FLX_format beta prec x FLX_format beta prec y
  round beta (FLX_exp prec) rnd (round beta (FLX_exp prec') rnd (x × y))
  = round beta (FLX_exp prec) rnd (x × y).

End Double_round_mult_FLX.

Section Double_round_mult_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' }.

Theorem round_round_mult_FLT :
  (emin' 2 × emin)%Z (2 × prec prec')%Z
   x y,
  FLT_format beta emin prec x FLT_format beta emin prec y
  round beta (FLT_exp emin prec) rnd
        (round beta (FLT_exp emin' prec') rnd (x × y))
  = round beta (FLT_exp emin prec) rnd (x × y).

End Double_round_mult_FLT.

Section Double_round_mult_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' }.

Theorem round_round_mult_FTZ :
  (emin' + prec' 2 × emin + prec)%Z
  (2 × prec prec')%Z
   x y,
  FTZ_format beta emin prec x FTZ_format beta emin prec y
  round beta (FTZ_exp emin prec) rnd
        (round beta (FTZ_exp emin' prec') rnd (x × y))
  = round beta (FTZ_exp emin prec) rnd (x × y).

End Double_round_mult_FTZ.

End Double_round_mult.

Section Double_round_plus.

Lemma mag_plus_disj :
   x y,
  0 < y y x
  ((mag (x + y) = mag x :> Z)
    (mag (x + y) = (mag x + 1)%Z :> Z)).

Lemma mag_plus_separated :
   fexp : Z Z,
   x y,
  0 < x 0 y
  generic_format beta fexp x
  (mag y fexp (mag x))%Z
  (mag (x + y) = mag x :> Z).

Lemma mag_minus_disj :
   x y,
  0 < x 0 < y
  (mag y mag x - 2)%Z
  ((mag (x - y) = mag x :> Z)
    (mag (x - y) = (mag x - 1)%Z :> Z)).

Lemma mag_minus_separated :
   fexp : Z Z, Valid_exp fexp
   x y,
  0 < x 0 < y y < x
  bpow (mag x - 1) < x
  generic_format beta fexp x (mag y fexp (mag x))%Z
  (mag (x - y) = mag x :> Z).

Definition round_round_plus_hyp fexp1 fexp2 :=
  ( ex ey, (fexp1 (ex + 1) - 1 ey)%Z (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (fexp1 (ex - 1) + 1 ey)%Z (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (fexp1 ex - 1 ey)%Z (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (ex - 1 ey)%Z (fexp2 ex fexp1 ey)%Z).

Lemma round_round_plus_aux0_aux_aux :
   (fexp1 fexp2 : Z Z),
   x y,
  (fexp1 (mag x) fexp1 (mag y))%Z
  (fexp2 (mag (x + y))%Z fexp1 (mag x))%Z
  (fexp2 (mag (x + y))%Z fexp1 (mag y))%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x + y).

Lemma round_round_plus_aux0_aux :
   (fexp1 fexp2 : Z Z),
   x y,
  (fexp2 (mag (x + y))%Z fexp1 (mag x))%Z
  (fexp2 (mag (x + y))%Z fexp1 (mag y))%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x + y).

Lemma round_round_plus_aux0 :
   (fexp1 fexp2 : Z Z), Valid_exp fexp1
  round_round_plus_hyp fexp1 fexp2
   x y,
  (0 < x)%R (0 < y)%R (y x)%R
  (fexp1 (mag x) - 1 mag y)%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x + y).

Lemma round_round_plus_aux1_aux :
   k, (0 < k)%Z
   (fexp : Z Z),
   x y,
  0 < x 0 < y
  (mag y fexp (mag x) - k)%Z
  (mag (x + y) = mag x :> Z)
  generic_format beta fexp x
  0 < (x + y) - round beta fexp Zfloor (x + y) < bpow (fexp (mag x) - k).

Lemma round_round_plus_aux1 :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_hyp fexp1 fexp2
   x y,
  0 < x 0 < y
  (mag y fexp1 (mag x) - 2)%Z
  generic_format beta fexp1 x
  round_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma round_round_plus_aux2 :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_hyp fexp1 fexp2
   x y,
  0 < x 0 < y y x
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma round_round_plus_aux :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_hyp fexp1 fexp2
   x y,
  0 x 0 y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma round_round_minus_aux0_aux :
   (fexp1 fexp2 : Z Z),
   x y,
  (fexp2 (mag (x - y))%Z fexp1 (mag x))%Z
  (fexp2 (mag (x - y))%Z fexp1 (mag y))%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma round_round_minus_aux0 :
   (fexp1 fexp2 : Z Z),
  round_round_plus_hyp fexp1 fexp2
   x y,
  0 < y y < x
  (fexp1 (mag x) - 1 mag y)%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma round_round_minus_aux1 :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
  round_round_plus_hyp fexp1 fexp2
   x y,
  0 < y y < x
  (mag y fexp1 (mag x) - 2)%Z
  (fexp1 (mag (x - y)) - 1 mag y)%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma round_round_minus_aux2_aux :
   (fexp : Z Z),
  Valid_exp fexp
   x y,
  0 < y y < x
  (mag y fexp (mag x) - 1)%Z
  generic_format beta fexp x
  generic_format beta fexp y
  round beta fexp Zceil (x - y) - (x - y) y.

Lemma round_round_minus_aux2 :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_hyp fexp1 fexp2
   x y,
  0 < y y < x
  (mag y fexp1 (mag x) - 2)%Z
  (mag y fexp1 (mag (x - y)) - 2)%Z
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma round_round_minus_aux3 :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_hyp fexp1 fexp2
   x y,
  0 < y y x
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma round_round_minus_aux :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_hyp fexp1 fexp2
   x y,
  0 x 0 y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma round_round_plus :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma round_round_minus :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Section Double_round_plus_FLX.

Variable prec : Z.
Variable prec' : Z.

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

Lemma FLX_round_round_plus_hyp :
  (2 × prec + 1 prec')%Z
  round_round_plus_hyp (FLX_exp prec) (FLX_exp prec').

Theorem round_round_plus_FLX :
   choice1 choice2,
  (2 × prec + 1 prec')%Z
   x y,
  FLX_format beta prec x FLX_format beta prec y
  round_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y).

Theorem round_round_minus_FLX :
   choice1 choice2,
  (2 × prec + 1 prec')%Z
   x y,
  FLX_format beta prec x FLX_format beta prec y
  round_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y).

End Double_round_plus_FLX.

Section Double_round_plus_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' }.

Lemma FLT_round_round_plus_hyp :
  (emin' emin)%Z (2 × prec + 1 prec')%Z
  round_round_plus_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem round_round_plus_FLT :
   choice1 choice2,
  (emin' emin)%Z (2 × prec + 1 prec')%Z
   x y,
  FLT_format beta emin prec x FLT_format beta emin prec y
  round_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x + y).

Theorem round_round_minus_FLT :
   choice1 choice2,
  (emin' emin)%Z (2 × prec + 1 prec')%Z
   x y,
  FLT_format beta emin prec x FLT_format beta emin prec y
  round_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x - y).

End Double_round_plus_FLT.

Section Double_round_plus_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' }.

Lemma FTZ_round_round_plus_hyp :
  (emin' + prec' emin + 1)%Z (2 × prec + 1 prec')%Z
  round_round_plus_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem round_round_plus_FTZ :
   choice1 choice2,
  (emin' + prec' emin + 1)%Z (2 × prec + 1 prec')%Z
   x y,
  FTZ_format beta emin prec x FTZ_format beta emin prec y
  round_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x + y).

Theorem round_round_minus_FTZ :
   choice1 choice2,
  (emin' + prec' emin + 1)%Z (2 × prec + 1 prec')%Z
   x y,
  FTZ_format beta emin prec x FTZ_format beta emin prec y
  round_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x - y).

End Double_round_plus_FTZ.

Section Double_round_plus_radix_ge_3.

Definition round_round_plus_radix_ge_3_hyp fexp1 fexp2 :=
  ( ex ey, (fexp1 (ex + 1) ey)%Z (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (fexp1 (ex - 1) + 1 ey)%Z (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (fexp1 ex ey)%Z (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (ex - 1 ey)%Z (fexp2 ex fexp1 ey)%Z).

Lemma round_round_plus_radix_ge_3_aux0 :
   (fexp1 fexp2 : Z Z), Valid_exp fexp1
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  (0 < y)%R (y x)%R
  (fexp1 (mag x) mag y)%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x + y).

Lemma round_round_plus_radix_ge_3_aux1 :
  (3 beta)%Z
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  0 < x 0 < y
  (mag y fexp1 (mag x) - 1)%Z
  generic_format beta fexp1 x
  round_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma round_round_plus_radix_ge_3_aux2 :
  (3 beta)%Z
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  0 < y y x
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma round_round_plus_radix_ge_3_aux :
  (3 beta)%Z
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  0 x 0 y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma round_round_minus_radix_ge_3_aux0 :
   (fexp1 fexp2 : Z Z),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  0 < y y < x
  (fexp1 (mag x) mag y)%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma round_round_minus_radix_ge_3_aux1 :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  0 < y y < x
  (mag y fexp1 (mag x) - 1)%Z
  (fexp1 (mag (x - y)) mag y)%Z
  generic_format beta fexp1 x generic_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma round_round_minus_radix_ge_3_aux2 :
  (3 beta)%Z
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  0 < y y < x
  (mag y fexp1 (mag x) - 1)%Z
  (mag y fexp1 (mag (x - y)) - 1)%Z
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma round_round_minus_radix_ge_3_aux3 :
  (3 beta)%Z
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  0 < y y x
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma round_round_minus_radix_ge_3_aux :
  (3 beta)%Z
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  0 x 0 y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma round_round_plus_radix_ge_3 :
  (3 beta)%Z
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma round_round_minus_radix_ge_3 :
  (3 beta)%Z
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_plus_radix_ge_3_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Section Double_round_plus_radix_ge_3_FLX.

Variable prec : Z.
Variable prec' : Z.

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

Lemma FLX_round_round_plus_radix_ge_3_hyp :
  (2 × prec prec')%Z
  round_round_plus_radix_ge_3_hyp (FLX_exp prec) (FLX_exp prec').

Theorem round_round_plus_radix_ge_3_FLX :
  (3 beta)%Z
   choice1 choice2,
  (2 × prec prec')%Z
   x y,
  FLX_format beta prec x FLX_format beta prec y
  round_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y).

Theorem round_round_minus_radix_ge_3_FLX :
  (3 beta)%Z
   choice1 choice2,
  (2 × prec prec')%Z
   x y,
  FLX_format beta prec x FLX_format beta prec y
  round_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y).

End Double_round_plus_radix_ge_3_FLX.

Section Double_round_plus_radix_ge_3_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' }.

Lemma FLT_round_round_plus_radix_ge_3_hyp :
  (emin' emin)%Z (2 × prec prec')%Z
  round_round_plus_radix_ge_3_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem round_round_plus_radix_ge_3_FLT :
  (3 beta)%Z
   choice1 choice2,
  (emin' emin)%Z (2 × prec prec')%Z
   x y,
  FLT_format beta emin prec x FLT_format beta emin prec y
  round_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x + y).

Theorem round_round_minus_radix_ge_3_FLT :
  (3 beta)%Z
   choice1 choice2,
  (emin' emin)%Z (2 × prec prec')%Z
   x y,
  FLT_format beta emin prec x FLT_format beta emin prec y
  round_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x - y).

End Double_round_plus_radix_ge_3_FLT.

Section Double_round_plus_radix_ge_3_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' }.

Lemma FTZ_round_round_plus_radix_ge_3_hyp :
  (emin' + prec' emin + 1)%Z (2 × prec prec')%Z
  round_round_plus_radix_ge_3_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem round_round_plus_radix_ge_3_FTZ :
  (3 beta)%Z
   choice1 choice2,
  (emin' + prec' emin + 1)%Z (2 × prec prec')%Z
   x y,
  FTZ_format beta emin prec x FTZ_format beta emin prec y
  round_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x + y).

Theorem round_round_minus_radix_ge_3_FTZ :
  (3 beta)%Z
   choice1 choice2,
  (emin' + prec' emin + 1)%Z (2 × prec prec')%Z
   x y,
  FTZ_format beta emin prec x FTZ_format beta emin prec y
  round_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x - y).

End Double_round_plus_radix_ge_3_FTZ.

End Double_round_plus_radix_ge_3.

End Double_round_plus.

Lemma round_round_mid_cases :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x) - 1)%Z
  (fexp1 (mag x) mag x)%Z
  (Rabs (x - midp fexp1 x) / 2 × (ulp beta fexp2 x)
   round_round_eq fexp1 fexp2 choice1 choice2 x)
  round_round_eq fexp1 fexp2 choice1 choice2 x.
Section Double_round_sqrt.

Definition round_round_sqrt_hyp fexp1 fexp2 :=
  ( ex, (2 × fexp1 ex fexp1 (2 × ex))%Z)
   ( ex, (2 × fexp1 ex fexp1 (2 × ex - 1))%Z)
   ( ex, (fexp1 (2 × ex) < 2 × ex)%Z
                 (fexp2 ex + ex 2 × fexp1 ex - 2)%Z).

Lemma mag_sqrt_disj :
   x,
  0 < x
  (mag x = 2 × mag (sqrt x) - 1 :> Z)%Z
   (mag x = 2 × mag (sqrt x) :> Z)%Z.

Lemma round_round_sqrt_aux :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
  round_round_sqrt_hyp fexp1 fexp2
   x,
  0 < x
  (fexp2 (mag (sqrt x)) fexp1 (mag (sqrt x)) - 1)%Z
  generic_format beta fexp1 x
  / 2 × ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)).

Lemma round_round_sqrt :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_sqrt_hyp fexp1 fexp2
   x,
  generic_format beta fexp1 x
  round_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).

Section Double_round_sqrt_FLX.

Variable prec : Z.
Variable prec' : Z.

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

Lemma FLX_round_round_sqrt_hyp :
  (2 × prec + 2 prec')%Z
  round_round_sqrt_hyp (FLX_exp prec) (FLX_exp prec').

Theorem round_round_sqrt_FLX :
   choice1 choice2,
  (2 × prec + 2 prec')%Z
   x,
  FLX_format beta prec x
  round_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x).

End Double_round_sqrt_FLX.

Section Double_round_sqrt_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' }.

Lemma FLT_round_round_sqrt_hyp :
  (emin 0)%Z
  ((emin' emin - prec - 2)%Z
    (2 × emin' emin - 4 × prec - 2)%Z)
  (2 × prec + 2 prec')%Z
  round_round_sqrt_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem round_round_sqrt_FLT :
   choice1 choice2,
  (emin 0)%Z
  ((emin' emin - prec - 2)%Z
    (2 × emin' emin - 4 × prec - 2)%Z)
  (2 × prec + 2 prec')%Z
   x,
  FLT_format beta emin prec x
  round_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (sqrt x).

End Double_round_sqrt_FLT.

Section Double_round_sqrt_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' }.

Lemma FTZ_round_round_sqrt_hyp :
  (2 × (emin' + prec') emin + prec 1)%Z
  (2 × prec + 2 prec')%Z
  round_round_sqrt_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem round_round_sqrt_FTZ :
  (4 beta)%Z
   choice1 choice2,
  (2 × (emin' + prec') emin + prec 1)%Z
  (2 × prec + 2 prec')%Z
   x,
  FTZ_format beta emin prec x
  round_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (sqrt x).

End Double_round_sqrt_FTZ.

Section Double_round_sqrt_radix_ge_4.

Definition round_round_sqrt_radix_ge_4_hyp fexp1 fexp2 :=
  ( ex, (2 × fexp1 ex fexp1 (2 × ex))%Z)
   ( ex, (2 × fexp1 ex fexp1 (2 × ex - 1))%Z)
   ( ex, (fexp1 (2 × ex) < 2 × ex)%Z
                 (fexp2 ex + ex 2 × fexp1 ex - 1)%Z).

Lemma round_round_sqrt_radix_ge_4_aux :
  (4 beta)%Z
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
  round_round_sqrt_radix_ge_4_hyp fexp1 fexp2
   x,
  0 < x
  (fexp2 (mag (sqrt x)) fexp1 (mag (sqrt x)) - 1)%Z
  generic_format beta fexp1 x
  / 2 × ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)).

Lemma round_round_sqrt_radix_ge_4 :
  (4 beta)%Z
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_sqrt_radix_ge_4_hyp fexp1 fexp2
   x,
  generic_format beta fexp1 x
  round_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).

Section Double_round_sqrt_radix_ge_4_FLX.

Variable prec : Z.
Variable prec' : Z.

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

Lemma FLX_round_round_sqrt_radix_ge_4_hyp :
  (2 × prec + 1 prec')%Z
  round_round_sqrt_radix_ge_4_hyp (FLX_exp prec) (FLX_exp prec').

Theorem round_round_sqrt_radix_ge_4_FLX :
  (4 beta)%Z
   choice1 choice2,
  (2 × prec + 1 prec')%Z
   x,
  FLX_format beta prec x
  round_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x).

End Double_round_sqrt_radix_ge_4_FLX.

Section Double_round_sqrt_radix_ge_4_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' }.

Lemma FLT_round_round_sqrt_radix_ge_4_hyp :
  (emin 0)%Z
  ((emin' emin - prec - 1)%Z
    (2 × emin' emin - 4 × prec)%Z)
  (2 × prec + 1 prec')%Z
  round_round_sqrt_radix_ge_4_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem round_round_sqrt_radix_ge_4_FLT :
  (4 beta)%Z
   choice1 choice2,
  (emin 0)%Z
  ((emin' emin - prec - 1)%Z
    (2 × emin' emin - 4 × prec)%Z)
  (2 × prec + 1 prec')%Z
   x,
  FLT_format beta emin prec x
  round_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (sqrt x).

End Double_round_sqrt_radix_ge_4_FLT.

Section Double_round_sqrt_radix_ge_4_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' }.

Lemma FTZ_round_round_sqrt_radix_ge_4_hyp :
  (2 × (emin' + prec') emin + prec 1)%Z
  (2 × prec + 1 prec')%Z
  round_round_sqrt_radix_ge_4_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem round_round_sqrt_radix_ge_4_FTZ :
  (4 beta)%Z
   choice1 choice2,
  (2 × (emin' + prec') emin + prec 1)%Z
  (2 × prec + 1 prec')%Z
   x,
  FTZ_format beta emin prec x
  round_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (sqrt x).

End Double_round_sqrt_radix_ge_4_FTZ.

End Double_round_sqrt_radix_ge_4.

End Double_round_sqrt.

Section Double_round_div.

Lemma round_round_eq_mid_beta_even :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  ( n, (beta = 2 × n :> Z)%Z)
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x) - 1)%Z
  (fexp1 (mag x) mag x)%Z
  x = midp fexp1 x
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_really_zero :
   (fexp1 fexp2 : Z Z),
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (mag x fexp1 (mag x) - 2)%Z
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_zero :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp1 (mag x) = mag x + 1 :> Z)%Z
  x < bpow (mag x) - / 2 × ulp beta fexp2 x
  round_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma round_round_all_mid_cases :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
   x,
  0 < x
  (fexp2 (mag x) fexp1 (mag x) - 1)%Z
  ((fexp1 (mag x) = mag x + 1 :> Z)%Z
   bpow (mag x) - / 2 × ulp beta fexp2 x x
   round_round_eq fexp1 fexp2 choice1 choice2 x)
  ((fexp1 (mag x) mag x)%Z
   midp fexp1 x - / 2 × ulp beta fexp2 x x < midp fexp1 x
   round_round_eq fexp1 fexp2 choice1 choice2 x)
  ((fexp1 (mag x) mag x)%Z
   x = midp fexp1 x
   round_round_eq fexp1 fexp2 choice1 choice2 x)
  ((fexp1 (mag x) mag x)%Z
   midp fexp1 x < x midp fexp1 x + / 2 × ulp beta fexp2 x
   round_round_eq fexp1 fexp2 choice1 choice2 x)
  round_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma mag_div_disj :
   x y : R,
  0 < x 0 < y
  ((mag (x / y) = mag x - mag y :> Z)%Z
    (mag (x / y) = mag x - mag y + 1 :> Z)%Z).

Definition round_round_div_hyp fexp1 fexp2 :=
  ( ex, (fexp2 ex fexp1 ex - 1)%Z)
   ( ex ey, (fexp1 ex < ex)%Z (fexp1 ey < ey)%Z
                    (fexp1 (ex - ey) ex - ey + 1)%Z
                    (fexp2 (ex - ey) fexp1 ex - ey)%Z)
   ( ex ey, (fexp1 ex < ex)%Z (fexp1 ey < ey)%Z
                    (fexp1 (ex - ey + 1) ex - ey + 1 + 1)%Z
                    (fexp2 (ex - ey + 1) fexp1 ex - ey)%Z)
   ( ex ey, (fexp1 ex < ex)%Z (fexp1 ey < ey)%Z
                    (fexp1 (ex - ey) ex - ey)%Z
                    (fexp2 (ex - ey) fexp1 (ex - ey)
                                        + fexp1 ey - ey)%Z)
   ( ex ey, (fexp1 ex < ex)%Z (fexp1 ey < ey)%Z
                    (fexp1 (ex - ey) = ex - ey + 1)%Z
                    (fexp2 (ex - ey) ex - ey - ey + fexp1 ey)%Z).

Lemma round_round_div_aux0 :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_div_hyp fexp1 fexp2
   x y,
  0 < x 0 < y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  fexp1 (mag (x / y)) = (mag (x / y) + 1)%Z
  ¬ (bpow (mag (x / y)) - / 2 × ulp beta fexp2 (x / y) x / y).

Lemma round_round_div_aux1 :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_div_hyp fexp1 fexp2
   x y,
  0 < x 0 < y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  (fexp1 (mag (x / y)) mag (x / y))%Z
  ¬ (midp fexp1 (x / y) - / 2 × ulp beta fexp2 (x / y)
      x / y
     < midp fexp1 (x / y)).

Lemma round_round_div_aux2 :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  round_round_div_hyp fexp1 fexp2
   x y,
  0 < x 0 < y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  (fexp1 (mag (x / y)) mag (x / y))%Z
  ¬ (midp fexp1 (x / y)
     < x / y
      midp fexp1 (x / y) + / 2 × ulp beta fexp2 (x / y)).

Lemma round_round_div_aux :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  ( n, (beta = 2 × n :> Z)%Z)
  round_round_div_hyp fexp1 fexp2
   x y,
  0 < x 0 < y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x / y).

Lemma round_round_div :
   fexp1 fexp2 : Z Z,
  Valid_exp fexp1 Valid_exp fexp2
   (choice1 choice2 : Z bool),
  ( n, (beta = 2 × n :> Z)%Z)
  round_round_div_hyp fexp1 fexp2
   x y,
  y 0
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  round_round_eq fexp1 fexp2 choice1 choice2 (x / y).

Section Double_round_div_FLX.

Variable prec : Z.
Variable prec' : Z.

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

Lemma FLX_round_round_div_hyp :
  (2 × prec prec')%Z
  round_round_div_hyp (FLX_exp prec) (FLX_exp prec').

Theorem round_round_div_FLX :
   choice1 choice2,
  ( n, (beta = 2 × n :> Z)%Z)
  (2 × prec prec')%Z
   x y,
  y 0
  FLX_format beta prec x FLX_format beta prec y
  round_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x / y).

End Double_round_div_FLX.

Section Double_round_div_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' }.

Lemma FLT_round_round_div_hyp :
  (emin' emin - prec - 2)%Z
  (2 × prec prec')%Z
  round_round_div_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem round_round_div_FLT :
   choice1 choice2,
  ( n, (beta = 2 × n :> Z)%Z)
  (emin' emin - prec - 2)%Z
  (2 × prec prec')%Z
   x y,
  y 0
  FLT_format beta emin prec x FLT_format beta emin prec y
  round_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x / y).

End Double_round_div_FLT.

Section Double_round_div_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' }.

Lemma FTZ_round_round_div_hyp :
  (emin' + prec' emin - 1)%Z
  (2 × prec prec')%Z
  round_round_div_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem round_round_div_FTZ :
   choice1 choice2,
  ( n, (beta = 2 × n :> Z)%Z)
  (emin' + prec' emin - 1)%Z
  (2 × prec prec')%Z
   x y,
  y 0
  FTZ_format beta emin prec x FTZ_format beta emin prec y
  round_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x / y).

End Double_round_div_FTZ.

End Double_round_div.

End Double_round.