From Coq Require Import ZArith Reals Psatz.

Require Import Core 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.

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.