Library Flocq.Appli.Fappli_double_round
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_generic_fmt.
Require Import Fcalc_ops.
Require Import Fcore_ulp.
Require Import Psatz.
Open Scope R_scope.
Section Double_round.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Notation ln_beta x := (ln_beta beta x).
Definition double_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 [(Fcore_Raux.bpow _ _ × Fcore_Raux.bpow _ _)] ⇒
rewrite <- bpow_plus
| |- context [(?X1 × Fcore_Raux.bpow _ _ × Fcore_Raux.bpow _ _)] ⇒
rewrite (Rmult_assoc X1); rewrite <- bpow_plus
| |- context [(?X1 × (?X2 × Fcore_Raux.bpow _ _) × Fcore_Raux.bpow _ _)] ⇒
rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
rewrite <- bpow_plus
end;
repeat
match goal with
| |- context [(Fcore_Raux.bpow _ ?X)] ⇒
progress ring_simplify X
end;
change (Fcore_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 double_round_lt_mid_further_place' :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
x < bpow (ln_beta x) - / 2 × ulp beta fexp2 x →
x < midp fexp1 x - / 2 × ulp beta fexp2 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_lt_mid_further_place :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
x < midp fexp1 x - / 2 × ulp beta fexp2 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_lt_mid_same_place :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) = fexp1 (ln_beta x))%Z →
x < midp fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_lt_mid :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x))%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
x < midp fexp1 x →
((fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
x < midp fexp1 x - / 2 × ulp beta fexp2 x) →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_gt_mid_further_place' :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
round beta fexp2 (Znearest choice2) x < bpow (ln_beta x) →
midp' fexp1 x + / 2 × ulp beta fexp2 x < x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_gt_mid_further_place :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
midp' fexp1 x + / 2 × ulp beta fexp2 x < x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_gt_mid_same_place :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) = fexp1 (ln_beta x))%Z →
midp' fexp1 x < x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_gt_mid :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x))%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
midp' fexp1 x < x →
((fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
midp' fexp1 x + / 2 × ulp beta fexp2 x < x) →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Section Double_round_mult.
Lemma ln_beta_mult_disj :
∀ x y,
x ≠ 0 → y ≠ 0 →
((ln_beta (x × y) = (ln_beta x + ln_beta y - 1)%Z :> Z)
∨ (ln_beta (x × y) = (ln_beta x + ln_beta y)%Z :> Z)).
Definition double_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 double_round_mult_aux :
∀ (fexp1 fexp2 : Z → Z),
double_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 double_round_mult :
∀ (fexp1 fexp2 : Z → Z),
double_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.
Require Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.
Theorem double_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.
Require Import Fcore_FLX.
Require Import Fcore_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 double_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.
Require Import Fcore_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 double_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 ln_beta_plus_disj :
∀ x y,
0 < y → y ≤ x →
((ln_beta (x + y) = ln_beta x :> Z)
∨ (ln_beta (x + y) = (ln_beta x + 1)%Z :> Z)).
Lemma ln_beta_plus_separated :
∀ fexp : Z → Z,
∀ x y,
0 < x → 0 ≤ y →
generic_format beta fexp x →
(ln_beta y ≤ fexp (ln_beta x))%Z →
(ln_beta (x + y) = ln_beta x :> Z).
Lemma ln_beta_minus_disj :
∀ x y,
0 < x → 0 < y →
(ln_beta y ≤ ln_beta x - 2)%Z →
((ln_beta (x - y) = ln_beta x :> Z)
∨ (ln_beta (x - y) = (ln_beta x - 1)%Z :> Z)).
Lemma ln_beta_minus_separated :
∀ fexp : Z → Z, Valid_exp fexp →
∀ x y,
0 < x → 0 < y → y < x →
bpow (ln_beta x - 1) < x →
generic_format beta fexp x → (ln_beta y ≤ fexp (ln_beta x))%Z →
(ln_beta (x - y) = ln_beta x :> Z).
Definition double_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 double_round_plus_aux0_aux_aux :
∀ (fexp1 fexp2 : Z → Z),
∀ x y,
(fexp1 (ln_beta x) ≤ fexp1 (ln_beta y))%Z →
(fexp2 (ln_beta (x + y))%Z ≤ fexp1 (ln_beta x))%Z →
(fexp2 (ln_beta (x + y))%Z ≤ fexp1 (ln_beta y))%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x + y).
Lemma double_round_plus_aux0_aux :
∀ (fexp1 fexp2 : Z → Z),
∀ x y,
(fexp2 (ln_beta (x + y))%Z ≤ fexp1 (ln_beta x))%Z →
(fexp2 (ln_beta (x + y))%Z ≤ fexp1 (ln_beta y))%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x + y).
Lemma double_round_plus_aux0 :
∀ (fexp1 fexp2 : Z → Z), Valid_exp fexp1 →
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
(0 < x)%R → (0 < y)%R → (y ≤ x)%R →
(fexp1 (ln_beta x) - 1 ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x + y).
Lemma double_round_plus_aux1_aux :
∀ k, (0 < k)%Z →
∀ (fexp : Z → Z),
∀ x y,
0 < x → 0 < y →
(ln_beta y ≤ fexp (ln_beta x) - k)%Z →
(ln_beta (x + y) = ln_beta x :> Z) →
generic_format beta fexp x →
0 < (x + y) - round beta fexp Zfloor (x + y) < bpow (fexp (ln_beta x) - k).
Lemma double_round_plus_aux1 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
(ln_beta y ≤ fexp1 (ln_beta x) - 2)%Z →
generic_format beta fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_aux2 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y → y ≤ x →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_aux :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 ≤ x → 0 ≤ y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_minus_aux0_aux :
∀ (fexp1 fexp2 : Z → Z),
∀ x y,
(fexp2 (ln_beta (x - y))%Z ≤ fexp1 (ln_beta x))%Z →
(fexp2 (ln_beta (x - y))%Z ≤ fexp1 (ln_beta y))%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_aux0 :
∀ (fexp1 fexp2 : Z → Z),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(fexp1 (ln_beta x) - 1 ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_aux1 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp1 (ln_beta x) - 2)%Z →
(fexp1 (ln_beta (x - y)) - 1 ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_aux2_aux :
∀ (fexp : Z → Z),
Valid_exp fexp →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp (ln_beta x) - 1)%Z →
generic_format beta fexp x →
generic_format beta fexp y →
round beta fexp Zceil (x - y) - (x - y) ≤ y.
Lemma double_round_minus_aux2 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp1 (ln_beta x) - 2)%Z →
(ln_beta y ≤ fexp1 (ln_beta (x - y)) - 2)%Z →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_minus_aux3 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < y → y ≤ x →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_minus_aux :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 ≤ x → 0 ≤ y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_plus :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_minus :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Section Double_round_plus_FLX.
Require Import Fcore_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_double_round_plus_hyp :
(2 × prec + 1 ≤ prec')%Z →
double_round_plus_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_round_plus_FLX :
∀ choice1 choice2,
(2 × prec + 1 ≤ prec')%Z →
∀ x y,
FLX_format beta prec x → FLX_format beta prec y →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y).
Theorem double_round_minus_FLX :
∀ choice1 choice2,
(2 × prec + 1 ≤ prec')%Z →
∀ x y,
FLX_format beta prec x → FLX_format beta prec y →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y).
End Double_round_plus_FLX.
Section Double_round_plus_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_plus_hyp :
(emin' ≤ emin)%Z → (2 × prec + 1 ≤ prec')%Z →
double_round_plus_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x + y).
Theorem double_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x - y).
End Double_round_plus_FLT.
Section Double_round_plus_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_plus_hyp :
(emin' + prec' ≤ emin + 1)%Z → (2 × prec + 1 ≤ prec')%Z →
double_round_plus_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (x + y).
Theorem double_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (x - y).
End Double_round_plus_FTZ.
Section Double_round_plus_beta_ge_3.
Definition double_round_plus_beta_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 double_round_plus_beta_ge_3_aux0 :
∀ (fexp1 fexp2 : Z → Z), Valid_exp fexp1 →
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
(0 < y)%R → (y ≤ x)%R →
(fexp1 (ln_beta x) ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x + y).
Lemma double_round_plus_beta_ge_3_aux1 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
(ln_beta y ≤ fexp1 (ln_beta x) - 1)%Z →
generic_format beta fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_beta_ge_3_aux2 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y ≤ x →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_beta_ge_3_aux :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 ≤ x → 0 ≤ y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_minus_beta_ge_3_aux0 :
∀ (fexp1 fexp2 : Z → Z),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(fexp1 (ln_beta x) ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_beta_ge_3_aux1 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta (x - y)) ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_beta_ge_3_aux2 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp1 (ln_beta x) - 1)%Z →
(ln_beta y ≤ fexp1 (ln_beta (x - y)) - 1)%Z →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_minus_beta_ge_3_aux3 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y ≤ x →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_minus_beta_ge_3_aux :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 ≤ x → 0 ≤ y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_plus_beta_ge_3 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_minus_beta_ge_3 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Section Double_round_plus_beta_ge_3_FLX.
Require Import Fcore_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_double_round_plus_beta_ge_3_hyp :
(2 × prec ≤ prec')%Z →
double_round_plus_beta_ge_3_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_round_plus_beta_ge_3_FLX :
(3 ≤ beta)%Z →
∀ choice1 choice2,
(2 × prec ≤ prec')%Z →
∀ x y,
FLX_format beta prec x → FLX_format beta prec y →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y).
Theorem double_round_minus_beta_ge_3_FLX :
(3 ≤ beta)%Z →
∀ choice1 choice2,
(2 × prec ≤ prec')%Z →
∀ x y,
FLX_format beta prec x → FLX_format beta prec y →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y).
End Double_round_plus_beta_ge_3_FLX.
Section Double_round_plus_beta_ge_3_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_plus_beta_ge_3_hyp :
(emin' ≤ emin)%Z → (2 × prec ≤ prec')%Z →
double_round_plus_beta_ge_3_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_round_plus_beta_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x + y).
Theorem double_round_minus_beta_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x - y).
End Double_round_plus_beta_ge_3_FLT.
Section Double_round_plus_beta_ge_3_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_plus_beta_ge_3_hyp :
(emin' + prec' ≤ emin + 1)%Z → (2 × prec ≤ prec')%Z →
double_round_plus_beta_ge_3_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_round_plus_beta_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (x + y).
Theorem double_round_minus_beta_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (x - y).
End Double_round_plus_beta_ge_3_FTZ.
End Double_round_plus_beta_ge_3.
End Double_round_plus.
Lemma double_round_mid_cases :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
(Rabs (x - midp fexp1 x) ≤ / 2 × (ulp beta fexp2 x) →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Section Double_round_sqrt.
Definition double_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 ln_beta_sqrt_disj :
∀ x,
0 < x →
(ln_beta x = 2 × ln_beta (sqrt x) - 1 :> Z)%Z
∨ (ln_beta x = 2 × ln_beta (sqrt x) :> Z)%Z.
Lemma double_round_sqrt_aux :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
double_round_sqrt_hyp fexp1 fexp2 →
∀ x,
0 < x →
(fexp2 (ln_beta (sqrt x)) ≤ fexp1 (ln_beta (sqrt x)) - 1)%Z →
generic_format beta fexp1 x →
/ 2 × ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)).
Lemma double_round_sqrt :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_sqrt_hyp fexp1 fexp2 →
∀ x,
generic_format beta fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).
Section Double_round_sqrt_FLX.
Require Import Fcore_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_double_round_sqrt_hyp :
(2 × prec + 2 ≤ prec')%Z →
double_round_sqrt_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_round_sqrt_FLX :
∀ choice1 choice2,
(2 × prec + 2 ≤ prec')%Z →
∀ x,
FLX_format beta prec x →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x).
End Double_round_sqrt_FLX.
Section Double_round_sqrt_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_sqrt_hyp :
(emin ≤ 0)%Z →
((emin' ≤ emin - prec - 2)%Z
∨ (2 × emin' ≤ emin - 4 × prec - 2)%Z) →
(2 × prec + 2 ≤ prec')%Z →
double_round_sqrt_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (sqrt x).
End Double_round_sqrt_FLT.
Section Double_round_sqrt_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_sqrt_hyp :
(2 × (emin' + prec') ≤ emin + prec ≤ 1)%Z →
(2 × prec + 2 ≤ prec')%Z →
double_round_sqrt_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (sqrt x).
End Double_round_sqrt_FTZ.
Section Double_round_sqrt_beta_ge_4.
Definition double_round_sqrt_beta_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 double_round_sqrt_beta_ge_4_aux :
(4 ≤ beta)%Z →
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
double_round_sqrt_beta_ge_4_hyp fexp1 fexp2 →
∀ x,
0 < x →
(fexp2 (ln_beta (sqrt x)) ≤ fexp1 (ln_beta (sqrt x)) - 1)%Z →
generic_format beta fexp1 x →
/ 2 × ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)).
Lemma double_round_sqrt_beta_ge_4 :
(4 ≤ beta)%Z →
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_sqrt_beta_ge_4_hyp fexp1 fexp2 →
∀ x,
generic_format beta fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).
Section Double_round_sqrt_beta_ge_4_FLX.
Require Import Fcore_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_double_round_sqrt_beta_ge_4_hyp :
(2 × prec + 1 ≤ prec')%Z →
double_round_sqrt_beta_ge_4_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_round_sqrt_beta_ge_4_FLX :
(4 ≤ beta)%Z →
∀ choice1 choice2,
(2 × prec + 1 ≤ prec')%Z →
∀ x,
FLX_format beta prec x →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x).
End Double_round_sqrt_beta_ge_4_FLX.
Section Double_round_sqrt_beta_ge_4_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_sqrt_beta_ge_4_hyp :
(emin ≤ 0)%Z →
((emin' ≤ emin - prec - 1)%Z
∨ (2 × emin' ≤ emin - 4 × prec)%Z) →
(2 × prec + 1 ≤ prec')%Z →
double_round_sqrt_beta_ge_4_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_round_sqrt_beta_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (sqrt x).
End Double_round_sqrt_beta_ge_4_FLT.
Section Double_round_sqrt_beta_ge_4_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_sqrt_beta_ge_4_hyp :
(2 × (emin' + prec') ≤ emin + prec ≤ 1)%Z →
(2 × prec + 1 ≤ prec')%Z →
double_round_sqrt_beta_ge_4_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_round_sqrt_beta_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (sqrt x).
End Double_round_sqrt_beta_ge_4_FTZ.
End Double_round_sqrt_beta_ge_4.
End Double_round_sqrt.
Section Double_round_div.
Lemma double_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 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
x = midp fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_really_zero :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(ln_beta x ≤ fexp1 (ln_beta x) - 2)%Z →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_zero :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp1 (ln_beta x) = ln_beta x + 1 :> Z)%Z →
x < bpow (ln_beta x) - / 2 × ulp beta fexp2 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_all_mid_cases :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
((fexp1 (ln_beta x) = ln_beta x + 1 :> Z)%Z →
bpow (ln_beta x) - / 2 × ulp beta fexp2 x ≤ x →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
((fexp1 (ln_beta x) ≤ ln_beta x)%Z →
midp fexp1 x - / 2 × ulp beta fexp2 x ≤ x < midp fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
((fexp1 (ln_beta x) ≤ ln_beta x)%Z →
x = midp fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
((fexp1 (ln_beta x) ≤ ln_beta x)%Z →
midp fexp1 x < x ≤ midp fexp1 x + / 2 × ulp beta fexp2 x →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma ln_beta_div_disj :
∀ x y : R,
0 < x → 0 < y →
((ln_beta (x / y) = ln_beta x - ln_beta y :> Z)%Z
∨ (ln_beta (x / y) = ln_beta x - ln_beta y + 1 :> Z)%Z).
Definition double_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 double_round_div_aux0 :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_div_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
fexp1 (ln_beta (x / y)) = (ln_beta (x / y) + 1)%Z →
¬ (bpow (ln_beta (x / y)) - / 2 × ulp beta fexp2 (x / y) ≤ x / y).
Lemma double_round_div_aux1 :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_div_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
(fexp1 (ln_beta (x / y)) ≤ ln_beta (x / y))%Z →
¬ (midp fexp1 (x / y) - / 2 × ulp beta fexp2 (x / y)
≤ x / y
< midp fexp1 (x / y)).
Lemma double_round_div_aux2 :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_div_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
(fexp1 (ln_beta (x / y)) ≤ ln_beta (x / y))%Z →
¬ (midp fexp1 (x / y)
< x / y
≤ midp fexp1 (x / y) + / 2 × ulp beta fexp2 (x / y)).
Lemma double_round_div_aux :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
(∃ n, (beta = 2 × n :> Z)%Z) →
double_round_div_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x / y).
Lemma double_round_div :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
(∃ n, (beta = 2 × n :> Z)%Z) →
double_round_div_hyp fexp1 fexp2 →
∀ x y,
y ≠ 0 →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x / y).
Section Double_round_div_FLX.
Require Import Fcore_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_double_round_div_hyp :
(2 × prec ≤ prec')%Z →
double_round_div_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_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 →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x / y).
End Double_round_div_FLX.
Section Double_round_div_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_div_hyp :
(emin' ≤ emin - prec - 2)%Z →
(2 × prec ≤ prec')%Z →
double_round_div_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x / y).
End Double_round_div_FLT.
Section Double_round_div_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_div_hyp :
(emin' + prec' ≤ emin - 1)%Z →
(2 × prec ≤ prec')%Z →
double_round_div_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_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 →
double_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.
repeat
match goal with
| |- context [(Fcore_Raux.bpow _ _ × Fcore_Raux.bpow _ _)] ⇒
rewrite <- bpow_plus
| |- context [(?X1 × Fcore_Raux.bpow _ _ × Fcore_Raux.bpow _ _)] ⇒
rewrite (Rmult_assoc X1); rewrite <- bpow_plus
| |- context [(?X1 × (?X2 × Fcore_Raux.bpow _ _) × Fcore_Raux.bpow _ _)] ⇒
rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
rewrite <- bpow_plus
end;
repeat
match goal with
| |- context [(Fcore_Raux.bpow _ ?X)] ⇒
progress ring_simplify X
end;
change (Fcore_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 double_round_lt_mid_further_place' :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
x < bpow (ln_beta x) - / 2 × ulp beta fexp2 x →
x < midp fexp1 x - / 2 × ulp beta fexp2 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_lt_mid_further_place :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
x < midp fexp1 x - / 2 × ulp beta fexp2 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_lt_mid_same_place :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) = fexp1 (ln_beta x))%Z →
x < midp fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_lt_mid :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x))%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
x < midp fexp1 x →
((fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
x < midp fexp1 x - / 2 × ulp beta fexp2 x) →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_gt_mid_further_place' :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
round beta fexp2 (Znearest choice2) x < bpow (ln_beta x) →
midp' fexp1 x + / 2 × ulp beta fexp2 x < x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_gt_mid_further_place :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
midp' fexp1 x + / 2 × ulp beta fexp2 x < x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_gt_mid_same_place :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) = fexp1 (ln_beta x))%Z →
midp' fexp1 x < x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_gt_mid :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x))%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
midp' fexp1 x < x →
((fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
midp' fexp1 x + / 2 × ulp beta fexp2 x < x) →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Section Double_round_mult.
Lemma ln_beta_mult_disj :
∀ x y,
x ≠ 0 → y ≠ 0 →
((ln_beta (x × y) = (ln_beta x + ln_beta y - 1)%Z :> Z)
∨ (ln_beta (x × y) = (ln_beta x + ln_beta y)%Z :> Z)).
Definition double_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 double_round_mult_aux :
∀ (fexp1 fexp2 : Z → Z),
double_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 double_round_mult :
∀ (fexp1 fexp2 : Z → Z),
double_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.
Require Import Fcore_FLX.
Variable prec : Z.
Variable prec' : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.
Theorem double_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.
Require Import Fcore_FLX.
Require Import Fcore_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 double_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.
Require Import Fcore_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 double_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 ln_beta_plus_disj :
∀ x y,
0 < y → y ≤ x →
((ln_beta (x + y) = ln_beta x :> Z)
∨ (ln_beta (x + y) = (ln_beta x + 1)%Z :> Z)).
Lemma ln_beta_plus_separated :
∀ fexp : Z → Z,
∀ x y,
0 < x → 0 ≤ y →
generic_format beta fexp x →
(ln_beta y ≤ fexp (ln_beta x))%Z →
(ln_beta (x + y) = ln_beta x :> Z).
Lemma ln_beta_minus_disj :
∀ x y,
0 < x → 0 < y →
(ln_beta y ≤ ln_beta x - 2)%Z →
((ln_beta (x - y) = ln_beta x :> Z)
∨ (ln_beta (x - y) = (ln_beta x - 1)%Z :> Z)).
Lemma ln_beta_minus_separated :
∀ fexp : Z → Z, Valid_exp fexp →
∀ x y,
0 < x → 0 < y → y < x →
bpow (ln_beta x - 1) < x →
generic_format beta fexp x → (ln_beta y ≤ fexp (ln_beta x))%Z →
(ln_beta (x - y) = ln_beta x :> Z).
Definition double_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 double_round_plus_aux0_aux_aux :
∀ (fexp1 fexp2 : Z → Z),
∀ x y,
(fexp1 (ln_beta x) ≤ fexp1 (ln_beta y))%Z →
(fexp2 (ln_beta (x + y))%Z ≤ fexp1 (ln_beta x))%Z →
(fexp2 (ln_beta (x + y))%Z ≤ fexp1 (ln_beta y))%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x + y).
Lemma double_round_plus_aux0_aux :
∀ (fexp1 fexp2 : Z → Z),
∀ x y,
(fexp2 (ln_beta (x + y))%Z ≤ fexp1 (ln_beta x))%Z →
(fexp2 (ln_beta (x + y))%Z ≤ fexp1 (ln_beta y))%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x + y).
Lemma double_round_plus_aux0 :
∀ (fexp1 fexp2 : Z → Z), Valid_exp fexp1 →
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
(0 < x)%R → (0 < y)%R → (y ≤ x)%R →
(fexp1 (ln_beta x) - 1 ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x + y).
Lemma double_round_plus_aux1_aux :
∀ k, (0 < k)%Z →
∀ (fexp : Z → Z),
∀ x y,
0 < x → 0 < y →
(ln_beta y ≤ fexp (ln_beta x) - k)%Z →
(ln_beta (x + y) = ln_beta x :> Z) →
generic_format beta fexp x →
0 < (x + y) - round beta fexp Zfloor (x + y) < bpow (fexp (ln_beta x) - k).
Lemma double_round_plus_aux1 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
(ln_beta y ≤ fexp1 (ln_beta x) - 2)%Z →
generic_format beta fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_aux2 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y → y ≤ x →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_aux :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 ≤ x → 0 ≤ y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_minus_aux0_aux :
∀ (fexp1 fexp2 : Z → Z),
∀ x y,
(fexp2 (ln_beta (x - y))%Z ≤ fexp1 (ln_beta x))%Z →
(fexp2 (ln_beta (x - y))%Z ≤ fexp1 (ln_beta y))%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_aux0 :
∀ (fexp1 fexp2 : Z → Z),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(fexp1 (ln_beta x) - 1 ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_aux1 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp1 (ln_beta x) - 2)%Z →
(fexp1 (ln_beta (x - y)) - 1 ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_aux2_aux :
∀ (fexp : Z → Z),
Valid_exp fexp →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp (ln_beta x) - 1)%Z →
generic_format beta fexp x →
generic_format beta fexp y →
round beta fexp Zceil (x - y) - (x - y) ≤ y.
Lemma double_round_minus_aux2 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp1 (ln_beta x) - 2)%Z →
(ln_beta y ≤ fexp1 (ln_beta (x - y)) - 2)%Z →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_minus_aux3 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 < y → y ≤ x →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_minus_aux :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
0 ≤ x → 0 ≤ y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_plus :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_minus :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_hyp fexp1 fexp2 →
∀ x y,
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Section Double_round_plus_FLX.
Require Import Fcore_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_double_round_plus_hyp :
(2 × prec + 1 ≤ prec')%Z →
double_round_plus_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_round_plus_FLX :
∀ choice1 choice2,
(2 × prec + 1 ≤ prec')%Z →
∀ x y,
FLX_format beta prec x → FLX_format beta prec y →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y).
Theorem double_round_minus_FLX :
∀ choice1 choice2,
(2 × prec + 1 ≤ prec')%Z →
∀ x y,
FLX_format beta prec x → FLX_format beta prec y →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y).
End Double_round_plus_FLX.
Section Double_round_plus_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_plus_hyp :
(emin' ≤ emin)%Z → (2 × prec + 1 ≤ prec')%Z →
double_round_plus_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x + y).
Theorem double_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x - y).
End Double_round_plus_FLT.
Section Double_round_plus_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_plus_hyp :
(emin' + prec' ≤ emin + 1)%Z → (2 × prec + 1 ≤ prec')%Z →
double_round_plus_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (x + y).
Theorem double_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (x - y).
End Double_round_plus_FTZ.
Section Double_round_plus_beta_ge_3.
Definition double_round_plus_beta_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 double_round_plus_beta_ge_3_aux0 :
∀ (fexp1 fexp2 : Z → Z), Valid_exp fexp1 →
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
(0 < y)%R → (y ≤ x)%R →
(fexp1 (ln_beta x) ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x + y).
Lemma double_round_plus_beta_ge_3_aux1 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
(ln_beta y ≤ fexp1 (ln_beta x) - 1)%Z →
generic_format beta fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_beta_ge_3_aux2 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y ≤ x →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_beta_ge_3_aux :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 ≤ x → 0 ≤ y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_minus_beta_ge_3_aux0 :
∀ (fexp1 fexp2 : Z → Z),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(fexp1 (ln_beta x) ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_beta_ge_3_aux1 :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta (x - y)) ≤ ln_beta y)%Z →
generic_format beta fexp1 x → generic_format beta fexp1 y →
generic_format beta fexp2 (x - y).
Lemma double_round_minus_beta_ge_3_aux2 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y < x →
(ln_beta y ≤ fexp1 (ln_beta x) - 1)%Z →
(ln_beta y ≤ fexp1 (ln_beta (x - y)) - 1)%Z →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_minus_beta_ge_3_aux3 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 < y → y ≤ x →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_minus_beta_ge_3_aux :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
0 ≤ x → 0 ≤ y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Lemma double_round_plus_beta_ge_3 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_minus_beta_ge_3 :
(3 ≤ beta)%Z →
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_plus_beta_ge_3_hyp fexp1 fexp2 →
∀ x y,
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x - y).
Section Double_round_plus_beta_ge_3_FLX.
Require Import Fcore_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_double_round_plus_beta_ge_3_hyp :
(2 × prec ≤ prec')%Z →
double_round_plus_beta_ge_3_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_round_plus_beta_ge_3_FLX :
(3 ≤ beta)%Z →
∀ choice1 choice2,
(2 × prec ≤ prec')%Z →
∀ x y,
FLX_format beta prec x → FLX_format beta prec y →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y).
Theorem double_round_minus_beta_ge_3_FLX :
(3 ≤ beta)%Z →
∀ choice1 choice2,
(2 × prec ≤ prec')%Z →
∀ x y,
FLX_format beta prec x → FLX_format beta prec y →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y).
End Double_round_plus_beta_ge_3_FLX.
Section Double_round_plus_beta_ge_3_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_plus_beta_ge_3_hyp :
(emin' ≤ emin)%Z → (2 × prec ≤ prec')%Z →
double_round_plus_beta_ge_3_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_round_plus_beta_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x + y).
Theorem double_round_minus_beta_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x - y).
End Double_round_plus_beta_ge_3_FLT.
Section Double_round_plus_beta_ge_3_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_plus_beta_ge_3_hyp :
(emin' + prec' ≤ emin + 1)%Z → (2 × prec ≤ prec')%Z →
double_round_plus_beta_ge_3_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_round_plus_beta_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (x + y).
Theorem double_round_minus_beta_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (x - y).
End Double_round_plus_beta_ge_3_FTZ.
End Double_round_plus_beta_ge_3.
End Double_round_plus.
Lemma double_round_mid_cases :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
(Rabs (x - midp fexp1 x) ≤ / 2 × (ulp beta fexp2 x) →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Section Double_round_sqrt.
Definition double_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 ln_beta_sqrt_disj :
∀ x,
0 < x →
(ln_beta x = 2 × ln_beta (sqrt x) - 1 :> Z)%Z
∨ (ln_beta x = 2 × ln_beta (sqrt x) :> Z)%Z.
Lemma double_round_sqrt_aux :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
double_round_sqrt_hyp fexp1 fexp2 →
∀ x,
0 < x →
(fexp2 (ln_beta (sqrt x)) ≤ fexp1 (ln_beta (sqrt x)) - 1)%Z →
generic_format beta fexp1 x →
/ 2 × ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)).
Lemma double_round_sqrt :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_sqrt_hyp fexp1 fexp2 →
∀ x,
generic_format beta fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).
Section Double_round_sqrt_FLX.
Require Import Fcore_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_double_round_sqrt_hyp :
(2 × prec + 2 ≤ prec')%Z →
double_round_sqrt_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_round_sqrt_FLX :
∀ choice1 choice2,
(2 × prec + 2 ≤ prec')%Z →
∀ x,
FLX_format beta prec x →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x).
End Double_round_sqrt_FLX.
Section Double_round_sqrt_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_sqrt_hyp :
(emin ≤ 0)%Z →
((emin' ≤ emin - prec - 2)%Z
∨ (2 × emin' ≤ emin - 4 × prec - 2)%Z) →
(2 × prec + 2 ≤ prec')%Z →
double_round_sqrt_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (sqrt x).
End Double_round_sqrt_FLT.
Section Double_round_sqrt_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_sqrt_hyp :
(2 × (emin' + prec') ≤ emin + prec ≤ 1)%Z →
(2 × prec + 2 ≤ prec')%Z →
double_round_sqrt_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (sqrt x).
End Double_round_sqrt_FTZ.
Section Double_round_sqrt_beta_ge_4.
Definition double_round_sqrt_beta_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 double_round_sqrt_beta_ge_4_aux :
(4 ≤ beta)%Z →
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
double_round_sqrt_beta_ge_4_hyp fexp1 fexp2 →
∀ x,
0 < x →
(fexp2 (ln_beta (sqrt x)) ≤ fexp1 (ln_beta (sqrt x)) - 1)%Z →
generic_format beta fexp1 x →
/ 2 × ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)).
Lemma double_round_sqrt_beta_ge_4 :
(4 ≤ beta)%Z →
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_sqrt_beta_ge_4_hyp fexp1 fexp2 →
∀ x,
generic_format beta fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).
Section Double_round_sqrt_beta_ge_4_FLX.
Require Import Fcore_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_double_round_sqrt_beta_ge_4_hyp :
(2 × prec + 1 ≤ prec')%Z →
double_round_sqrt_beta_ge_4_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_round_sqrt_beta_ge_4_FLX :
(4 ≤ beta)%Z →
∀ choice1 choice2,
(2 × prec + 1 ≤ prec')%Z →
∀ x,
FLX_format beta prec x →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x).
End Double_round_sqrt_beta_ge_4_FLX.
Section Double_round_sqrt_beta_ge_4_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_sqrt_beta_ge_4_hyp :
(emin ≤ 0)%Z →
((emin' ≤ emin - prec - 1)%Z
∨ (2 × emin' ≤ emin - 4 × prec)%Z) →
(2 × prec + 1 ≤ prec')%Z →
double_round_sqrt_beta_ge_4_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_round_sqrt_beta_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (sqrt x).
End Double_round_sqrt_beta_ge_4_FLT.
Section Double_round_sqrt_beta_ge_4_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_sqrt_beta_ge_4_hyp :
(2 × (emin' + prec') ≤ emin + prec ≤ 1)%Z →
(2 × prec + 1 ≤ prec')%Z →
double_round_sqrt_beta_ge_4_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_round_sqrt_beta_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 →
double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
choice1 choice2 (sqrt x).
End Double_round_sqrt_beta_ge_4_FTZ.
End Double_round_sqrt_beta_ge_4.
End Double_round_sqrt.
Section Double_round_div.
Lemma double_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 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
(fexp1 (ln_beta x) ≤ ln_beta x)%Z →
x = midp fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_really_zero :
∀ (fexp1 fexp2 : Z → Z),
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(ln_beta x ≤ fexp1 (ln_beta x) - 2)%Z →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_zero :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp1 (ln_beta x) = ln_beta x + 1 :> Z)%Z →
x < bpow (ln_beta x) - / 2 × ulp beta fexp2 x →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma double_round_all_mid_cases :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
∀ x,
0 < x →
(fexp2 (ln_beta x) ≤ fexp1 (ln_beta x) - 1)%Z →
((fexp1 (ln_beta x) = ln_beta x + 1 :> Z)%Z →
bpow (ln_beta x) - / 2 × ulp beta fexp2 x ≤ x →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
((fexp1 (ln_beta x) ≤ ln_beta x)%Z →
midp fexp1 x - / 2 × ulp beta fexp2 x ≤ x < midp fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
((fexp1 (ln_beta x) ≤ ln_beta x)%Z →
x = midp fexp1 x →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
((fexp1 (ln_beta x) ≤ ln_beta x)%Z →
midp fexp1 x < x ≤ midp fexp1 x + / 2 × ulp beta fexp2 x →
double_round_eq fexp1 fexp2 choice1 choice2 x) →
double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma ln_beta_div_disj :
∀ x y : R,
0 < x → 0 < y →
((ln_beta (x / y) = ln_beta x - ln_beta y :> Z)%Z
∨ (ln_beta (x / y) = ln_beta x - ln_beta y + 1 :> Z)%Z).
Definition double_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 double_round_div_aux0 :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_div_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
fexp1 (ln_beta (x / y)) = (ln_beta (x / y) + 1)%Z →
¬ (bpow (ln_beta (x / y)) - / 2 × ulp beta fexp2 (x / y) ≤ x / y).
Lemma double_round_div_aux1 :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_div_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
(fexp1 (ln_beta (x / y)) ≤ ln_beta (x / y))%Z →
¬ (midp fexp1 (x / y) - / 2 × ulp beta fexp2 (x / y)
≤ x / y
< midp fexp1 (x / y)).
Lemma double_round_div_aux2 :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
double_round_div_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
(fexp1 (ln_beta (x / y)) ≤ ln_beta (x / y))%Z →
¬ (midp fexp1 (x / y)
< x / y
≤ midp fexp1 (x / y) + / 2 × ulp beta fexp2 (x / y)).
Lemma double_round_div_aux :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
(∃ n, (beta = 2 × n :> Z)%Z) →
double_round_div_hyp fexp1 fexp2 →
∀ x y,
0 < x → 0 < y →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x / y).
Lemma double_round_div :
∀ fexp1 fexp2 : Z → Z,
Valid_exp fexp1 → Valid_exp fexp2 →
∀ (choice1 choice2 : Z → bool),
(∃ n, (beta = 2 × n :> Z)%Z) →
double_round_div_hyp fexp1 fexp2 →
∀ x y,
y ≠ 0 →
generic_format beta fexp1 x →
generic_format beta fexp1 y →
double_round_eq fexp1 fexp2 choice1 choice2 (x / y).
Section Double_round_div_FLX.
Require Import Fcore_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_double_round_div_hyp :
(2 × prec ≤ prec')%Z →
double_round_div_hyp (FLX_exp prec) (FLX_exp prec').
Theorem double_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 →
double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x / y).
End Double_round_div_FLX.
Section Double_round_div_FLT.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_div_hyp :
(emin' ≤ emin - prec - 2)%Z →
(2 × prec ≤ prec')%Z →
double_round_div_hyp (FLT_exp emin prec) (FLT_exp emin' prec').
Theorem double_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 →
double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
choice1 choice2 (x / y).
End Double_round_div_FLT.
Section Double_round_div_FTZ.
Require Import Fcore_FLX.
Require Import Fcore_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_double_round_div_hyp :
(emin' + prec' ≤ emin - 1)%Z →
(2 × prec ≤ prec')%Z →
double_round_div_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').
Theorem double_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 →
double_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.