Library Flocq.Core.Generic_fmt
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2009-2018 Sylvie Boldo
Copyright (C) 2009-2018 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Copyright (C) 2009-2018 Guillaume Melquiond
What is a real number belonging to a format, and many properties.
From Coq Require Import ZArith Reals Lia.
Require Import Zaux Raux Defs Round_pred Float_prop.
Section Generic.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Section Format.
Variable fexp : Z → Z.
To be a good fexp
Class Valid_exp :=
valid_exp :
∀ k : Z,
( (fexp k < k)%Z → (fexp (k + 1) ≤ k)%Z ) ∧
( (k ≤ fexp k)%Z →
(fexp (fexp k + 1) ≤ fexp k)%Z ∧
∀ l : Z, (l ≤ fexp k)%Z → fexp l = fexp k ).
Context { valid_exp_ : Valid_exp }.
Theorem valid_exp_large :
∀ k l,
(fexp k < k)%Z → (k ≤ l)%Z →
(fexp l < l)%Z.
Theorem valid_exp_large' :
∀ k l,
(fexp k < k)%Z → (l ≤ k)%Z →
(fexp l < k)%Z.
Definition cexp x :=
fexp (mag beta x).
Definition canonical (f : float beta) :=
Fexp f = cexp (F2R f).
Definition scaled_mantissa x :=
(x × bpow (- cexp x))%R.
Definition generic_format (x : R) :=
x = F2R (Float beta (Ztrunc (scaled_mantissa x)) (cexp x)).
Basic facts
Theorem generic_format_0 :
generic_format 0.
Theorem cexp_opp :
∀ x,
cexp (-x) = cexp x.
Theorem cexp_abs :
∀ x,
cexp (Rabs x) = cexp x.
Theorem canonical_generic_format :
∀ x,
generic_format x →
∃ f : float beta,
x = F2R f ∧ canonical f.
Theorem generic_format_bpow :
∀ e, (fexp (e + 1) ≤ e)%Z →
generic_format (bpow e).
Theorem generic_format_bpow' :
∀ e, (fexp e ≤ e)%Z →
generic_format (bpow e).
Theorem generic_format_F2R :
∀ m e,
( m ≠ 0 → cexp (F2R (Float beta m e)) ≤ e )%Z →
generic_format (F2R (Float beta m e)).
Lemma generic_format_F2R' :
∀ (x : R) (f : float beta),
F2R f = x →
(x ≠ 0%R → (cexp x ≤ Fexp f)%Z) →
generic_format x.
Theorem canonical_opp :
∀ m e,
canonical (Float beta m e) →
canonical (Float beta (-m) e).
Theorem canonical_abs :
∀ m e,
canonical (Float beta m e) →
canonical (Float beta (Z.abs m) e).
Theorem canonical_0 :
canonical (Float beta 0 (fexp (mag beta 0%R))).
Theorem canonical_unique :
∀ f1 f2,
canonical f1 →
canonical f2 →
F2R f1 = F2R f2 →
f1 = f2.
Theorem scaled_mantissa_generic :
∀ x,
generic_format x →
scaled_mantissa x = IZR (Ztrunc (scaled_mantissa x)).
Theorem scaled_mantissa_mult_bpow :
∀ x,
(scaled_mantissa x × bpow (cexp x))%R = x.
Theorem scaled_mantissa_0 :
scaled_mantissa 0 = 0%R.
Theorem scaled_mantissa_opp :
∀ x,
scaled_mantissa (-x) = (-scaled_mantissa x)%R.
Theorem scaled_mantissa_abs :
∀ x,
scaled_mantissa (Rabs x) = Rabs (scaled_mantissa x).
Theorem generic_format_opp :
∀ x, generic_format x → generic_format (-x).
Theorem generic_format_abs :
∀ x, generic_format x → generic_format (Rabs x).
Theorem generic_format_abs_inv :
∀ x, generic_format (Rabs x) → generic_format x.
Theorem cexp_fexp :
∀ x ex,
(bpow (ex - 1) ≤ Rabs x < bpow ex)%R →
cexp x = fexp ex.
Theorem cexp_fexp_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
cexp x = fexp ex.
generic_format 0.
Theorem cexp_opp :
∀ x,
cexp (-x) = cexp x.
Theorem cexp_abs :
∀ x,
cexp (Rabs x) = cexp x.
Theorem canonical_generic_format :
∀ x,
generic_format x →
∃ f : float beta,
x = F2R f ∧ canonical f.
Theorem generic_format_bpow :
∀ e, (fexp (e + 1) ≤ e)%Z →
generic_format (bpow e).
Theorem generic_format_bpow' :
∀ e, (fexp e ≤ e)%Z →
generic_format (bpow e).
Theorem generic_format_F2R :
∀ m e,
( m ≠ 0 → cexp (F2R (Float beta m e)) ≤ e )%Z →
generic_format (F2R (Float beta m e)).
Lemma generic_format_F2R' :
∀ (x : R) (f : float beta),
F2R f = x →
(x ≠ 0%R → (cexp x ≤ Fexp f)%Z) →
generic_format x.
Theorem canonical_opp :
∀ m e,
canonical (Float beta m e) →
canonical (Float beta (-m) e).
Theorem canonical_abs :
∀ m e,
canonical (Float beta m e) →
canonical (Float beta (Z.abs m) e).
Theorem canonical_0 :
canonical (Float beta 0 (fexp (mag beta 0%R))).
Theorem canonical_unique :
∀ f1 f2,
canonical f1 →
canonical f2 →
F2R f1 = F2R f2 →
f1 = f2.
Theorem scaled_mantissa_generic :
∀ x,
generic_format x →
scaled_mantissa x = IZR (Ztrunc (scaled_mantissa x)).
Theorem scaled_mantissa_mult_bpow :
∀ x,
(scaled_mantissa x × bpow (cexp x))%R = x.
Theorem scaled_mantissa_0 :
scaled_mantissa 0 = 0%R.
Theorem scaled_mantissa_opp :
∀ x,
scaled_mantissa (-x) = (-scaled_mantissa x)%R.
Theorem scaled_mantissa_abs :
∀ x,
scaled_mantissa (Rabs x) = Rabs (scaled_mantissa x).
Theorem generic_format_opp :
∀ x, generic_format x → generic_format (-x).
Theorem generic_format_abs :
∀ x, generic_format x → generic_format (Rabs x).
Theorem generic_format_abs_inv :
∀ x, generic_format (Rabs x) → generic_format x.
Theorem cexp_fexp :
∀ x ex,
(bpow (ex - 1) ≤ Rabs x < bpow ex)%R →
cexp x = fexp ex.
Theorem cexp_fexp_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
cexp x = fexp ex.
Properties when the real number is "small" (kind of subnormal)
Theorem mantissa_small_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
(0 < x × bpow (- fexp ex) < 1)%R.
Theorem scaled_mantissa_lt_1 :
∀ x ex,
(Rabs x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
(Rabs (scaled_mantissa x) < 1)%R.
Theorem scaled_mantissa_lt_bpow :
∀ x,
(Rabs (scaled_mantissa x) < bpow (mag beta x - cexp x))%R.
Theorem mag_generic_gt :
∀ x, (x ≠ 0)%R →
generic_format x →
(cexp x < mag beta x)%Z.
Lemma mantissa_DN_small_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
Zfloor (x × bpow (- fexp ex)) = Z0.
Lemma mantissa_UP_small_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
Zceil (x × bpow (- fexp ex)) = 1%Z.
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
(0 < x × bpow (- fexp ex) < 1)%R.
Theorem scaled_mantissa_lt_1 :
∀ x ex,
(Rabs x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
(Rabs (scaled_mantissa x) < 1)%R.
Theorem scaled_mantissa_lt_bpow :
∀ x,
(Rabs (scaled_mantissa x) < bpow (mag beta x - cexp x))%R.
Theorem mag_generic_gt :
∀ x, (x ≠ 0)%R →
generic_format x →
(cexp x < mag beta x)%Z.
Lemma mantissa_DN_small_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
Zfloor (x × bpow (- fexp ex)) = Z0.
Lemma mantissa_UP_small_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
Zceil (x × bpow (- fexp ex)) = 1%Z.
Generic facts about any format
Theorem generic_format_discrete :
∀ x m,
let e := cexp x in
(F2R (Float beta m e) < x < F2R (Float beta (m + 1) e))%R →
¬ generic_format x.
Theorem generic_format_canonical :
∀ f, canonical f →
generic_format (F2R f).
Theorem generic_format_ge_bpow :
∀ emin,
( ∀ e, (emin ≤ fexp e)%Z ) →
∀ x,
(0 < x)%R →
generic_format x →
(bpow emin ≤ x)%R.
Theorem abs_lt_bpow_prec:
∀ prec,
(∀ e, (e - prec ≤ fexp e)%Z) →
∀ x,
(Rabs x < bpow (prec + cexp x))%R.
Theorem generic_format_bpow_inv' :
∀ e,
generic_format (bpow e) →
(fexp (e + 1) ≤ e)%Z.
Theorem generic_format_bpow_inv :
∀ e,
generic_format (bpow e) →
(fexp e ≤ e)%Z.
Section Fcore_generic_round_pos.
∀ x m,
let e := cexp x in
(F2R (Float beta m e) < x < F2R (Float beta (m + 1) e))%R →
¬ generic_format x.
Theorem generic_format_canonical :
∀ f, canonical f →
generic_format (F2R f).
Theorem generic_format_ge_bpow :
∀ emin,
( ∀ e, (emin ≤ fexp e)%Z ) →
∀ x,
(0 < x)%R →
generic_format x →
(bpow emin ≤ x)%R.
Theorem abs_lt_bpow_prec:
∀ prec,
(∀ e, (e - prec ≤ fexp e)%Z) →
∀ x,
(Rabs x < bpow (prec + cexp x))%R.
Theorem generic_format_bpow_inv' :
∀ e,
generic_format (bpow e) →
(fexp (e + 1) ≤ e)%Z.
Theorem generic_format_bpow_inv :
∀ e,
generic_format (bpow e) →
(fexp e ≤ e)%Z.
Section Fcore_generic_round_pos.
Rounding functions: R -> Z
Variable rnd : R → Z.
Class Valid_rnd := {
Zrnd_le : ∀ x y, (x ≤ y)%R → (rnd x ≤ rnd y)%Z ;
Zrnd_IZR : ∀ n, rnd (IZR n) = n
}.
Context { valid_rnd : Valid_rnd }.
Theorem Zrnd_DN_or_UP :
∀ x, rnd x = Zfloor x ∨ rnd x = Zceil x.
Theorem Zrnd_ZR_or_AW :
∀ x, rnd x = Ztrunc x ∨ rnd x = Zaway x.
the most useful one: R -> F
Definition round x :=
F2R (Float beta (rnd (scaled_mantissa x)) (cexp x)).
Theorem round_bounded_large_pos :
∀ x ex,
(fexp ex < ex)%Z →
(bpow (ex - 1) ≤ x < bpow ex)%R →
(bpow (ex - 1) ≤ round x ≤ bpow ex)%R.
Theorem round_bounded_small_pos :
∀ x ex,
(ex ≤ fexp ex)%Z →
(bpow (ex - 1) ≤ x < bpow ex)%R →
round x = 0%R ∨ round x = bpow (fexp ex).
Lemma round_le_pos :
∀ x y, (0 < x)%R → (x ≤ y)%R → (round x ≤ round y)%R.
Theorem round_generic :
∀ x,
generic_format x →
round x = x.
Theorem round_0 :
round 0 = 0%R.
Theorem exp_small_round_0_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
round x = 0%R → (ex ≤ fexp ex)%Z .
Lemma generic_format_round_pos :
∀ x,
(0 < x)%R →
generic_format (round x).
End Fcore_generic_round_pos.
Theorem round_ext :
∀ rnd1 rnd2,
( ∀ x, rnd1 x = rnd2 x ) →
∀ x,
round rnd1 x = round rnd2 x.
Section Zround_opp.
Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.
Definition Zrnd_opp x := Z.opp (rnd (-x)).
Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.
Theorem round_opp :
∀ x,
round rnd (- x) = Ropp (round Zrnd_opp x).
End Zround_opp.
F2R (Float beta (rnd (scaled_mantissa x)) (cexp x)).
Theorem round_bounded_large_pos :
∀ x ex,
(fexp ex < ex)%Z →
(bpow (ex - 1) ≤ x < bpow ex)%R →
(bpow (ex - 1) ≤ round x ≤ bpow ex)%R.
Theorem round_bounded_small_pos :
∀ x ex,
(ex ≤ fexp ex)%Z →
(bpow (ex - 1) ≤ x < bpow ex)%R →
round x = 0%R ∨ round x = bpow (fexp ex).
Lemma round_le_pos :
∀ x y, (0 < x)%R → (x ≤ y)%R → (round x ≤ round y)%R.
Theorem round_generic :
∀ x,
generic_format x →
round x = x.
Theorem round_0 :
round 0 = 0%R.
Theorem exp_small_round_0_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
round x = 0%R → (ex ≤ fexp ex)%Z .
Lemma generic_format_round_pos :
∀ x,
(0 < x)%R →
generic_format (round x).
End Fcore_generic_round_pos.
Theorem round_ext :
∀ rnd1 rnd2,
( ∀ x, rnd1 x = rnd2 x ) →
∀ x,
round rnd1 x = round rnd2 x.
Section Zround_opp.
Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.
Definition Zrnd_opp x := Z.opp (rnd (-x)).
Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.
Theorem round_opp :
∀ x,
round rnd (- x) = Ropp (round Zrnd_opp x).
End Zround_opp.
IEEE-754 roundings: up, down and to zero
Global Instance valid_rnd_DN : Valid_rnd Zfloor.
Global Instance valid_rnd_UP : Valid_rnd Zceil.
Global Instance valid_rnd_ZR : Valid_rnd Ztrunc.
Global Instance valid_rnd_AW : Valid_rnd Zaway.
Section monotone.
Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem round_DN_or_UP :
∀ x,
round rnd x = round Zfloor x ∨ round rnd x = round Zceil x.
Theorem round_ZR_or_AW :
∀ x,
round rnd x = round Ztrunc x ∨ round rnd x = round Zaway x.
Theorem round_le :
∀ x y, (x ≤ y)%R → (round rnd x ≤ round rnd y)%R.
Theorem round_ge_generic :
∀ x y, generic_format x → (x ≤ y)%R → (x ≤ round rnd y)%R.
Theorem round_le_generic :
∀ x y, generic_format y → (x ≤ y)%R → (round rnd x ≤ y)%R.
End monotone.
Theorem round_abs_abs :
∀ P : R → R → Prop,
( ∀ rnd (Hr : Valid_rnd rnd) x, (0 ≤ x)%R → P x (round rnd x) ) →
∀ rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).
Theorem round_bounded_large :
∀ rnd {Hr : Valid_rnd rnd} x ex,
(fexp ex < ex)%Z →
(bpow (ex - 1) ≤ Rabs x < bpow ex)%R →
(bpow (ex - 1) ≤ Rabs (round rnd x) ≤ bpow ex)%R.
Theorem exp_small_round_0 :
∀ rnd {Hr : Valid_rnd rnd} x ex,
(bpow (ex - 1) ≤ Rabs x < bpow ex)%R →
round rnd x = 0%R → (ex ≤ fexp ex)%Z .
Section monotone_abs.
Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem abs_round_ge_generic :
∀ x y, generic_format x → (x ≤ Rabs y)%R → (x ≤ Rabs (round rnd y))%R.
Theorem abs_round_le_generic :
∀ x y, generic_format y → (Rabs x ≤ y)%R → (Rabs (round rnd x) ≤ y)%R.
End monotone_abs.
Theorem round_DN_opp :
∀ x,
round Zfloor (-x) = (- round Zceil x)%R.
Theorem round_UP_opp :
∀ x,
round Zceil (-x) = (- round Zfloor x)%R.
Theorem round_ZR_opp :
∀ x,
round Ztrunc (- x) = Ropp (round Ztrunc x).
Theorem round_ZR_abs :
∀ x,
round Ztrunc (Rabs x) = Rabs (round Ztrunc x).
Theorem round_AW_opp :
∀ x,
round Zaway (- x) = Ropp (round Zaway x).
Theorem round_AW_abs :
∀ x,
round Zaway (Rabs x) = Rabs (round Zaway x).
Theorem round_ZR_DN :
∀ x,
(0 ≤ x)%R →
round Ztrunc x = round Zfloor x.
Theorem round_ZR_UP :
∀ x,
(x ≤ 0)%R →
round Ztrunc x = round Zceil x.
Theorem round_AW_UP :
∀ x,
(0 ≤ x)%R →
round Zaway x = round Zceil x.
Theorem round_AW_DN :
∀ x,
(x ≤ 0)%R →
round Zaway x = round Zfloor x.
Theorem generic_format_round :
∀ rnd { Hr : Valid_rnd rnd } x,
generic_format (round rnd x).
Theorem round_DN_pt :
∀ x,
Rnd_DN_pt generic_format x (round Zfloor x).
Theorem generic_format_satisfies_any :
satisfies_any generic_format.
Theorem round_UP_pt :
∀ x,
Rnd_UP_pt generic_format x (round Zceil x).
Theorem round_ZR_pt :
∀ x,
Rnd_ZR_pt generic_format x (round Ztrunc x).
Lemma round_DN_small_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
round Zfloor x = 0%R.
Theorem round_DN_UP_lt :
∀ x, ¬ generic_format x →
(round Zfloor x < x < round Zceil x)%R.
Lemma round_UP_small_pos :
∀ x ex,
(bpow (ex - 1) ≤ x < bpow ex)%R →
(ex ≤ fexp ex)%Z →
round Zceil x = (bpow (fexp ex)).
Theorem generic_format_EM :
∀ x,
generic_format x ∨ ¬generic_format x.
Section round_large.
Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.
Lemma round_large_pos_ge_bpow :
∀ x e,
(0 < round rnd x)%R →
(bpow e ≤ x)%R →
(bpow e ≤ round rnd x)%R.
End round_large.
Theorem mag_round_ZR :
∀ x,
(round Ztrunc x ≠ 0)%R →
(mag beta (round Ztrunc x) = mag beta x :> Z).
Theorem mag_round :
∀ rnd {Hrnd : Valid_rnd rnd} x,
(round rnd x ≠ 0)%R →
(mag beta (round rnd x) = mag beta x :> Z) ∨
Rabs (round rnd x) = bpow (Z.max (mag beta x) (fexp (mag beta x))).
Theorem mag_DN :
∀ x,
(0 < round Zfloor x)%R →
(mag beta (round Zfloor x) = mag beta x :> Z).
Theorem cexp_DN :
∀ x,
(0 < round Zfloor x)%R →
cexp (round Zfloor x) = cexp x.
Theorem scaled_mantissa_DN :
∀ x,
(0 < round Zfloor x)%R →
scaled_mantissa (round Zfloor x) = IZR (Zfloor (scaled_mantissa x)).
Theorem generic_N_pt_DN_or_UP :
∀ x f,
Rnd_N_pt generic_format x f →
f = round Zfloor x ∨ f = round Zceil x.
Section not_FTZ.
Class Exp_not_FTZ :=
exp_not_FTZ : ∀ e, (fexp (fexp e + 1) ≤ fexp e)%Z.
Context { exp_not_FTZ_ : Exp_not_FTZ }.
Theorem subnormal_exponent :
∀ e x,
(e ≤ fexp e)%Z →
generic_format x →
x = F2R (Float beta (Ztrunc (x × bpow (- fexp e))) (fexp e)).
End not_FTZ.
Section monotone_exp.
Class Monotone_exp :=
monotone_exp : ∀ ex ey, (ex ≤ ey)%Z → (fexp ex ≤ fexp ey)%Z.
Context { monotone_exp_ : Monotone_exp }.
Global Instance monotone_exp_not_FTZ : Exp_not_FTZ.
Lemma cexp_le_bpow :
∀ (x : R) (e : Z),
x ≠ 0%R →
(Rabs x < bpow e)%R →
(cexp x ≤ fexp e)%Z.
Lemma cexp_ge_bpow :
∀ (x : R) (e : Z),
(bpow (e - 1) ≤ Rabs x)%R →
(fexp e ≤ cexp x)%Z.
Lemma lt_cexp_pos :
∀ x y,
(0 < y)%R →
(cexp x < cexp y)%Z →
(x < y)%R.
Theorem lt_cexp :
∀ x y,
(y ≠ 0)%R →
(cexp x < cexp y)%Z →
(Rabs x < Rabs y)%R.
Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem mag_round_ge :
∀ x,
round rnd x ≠ 0%R →
(mag beta x ≤ mag beta (round rnd x))%Z.
Theorem cexp_round_ge :
∀ x,
round rnd x ≠ 0%R →
(cexp x ≤ cexp (round rnd x))%Z.
End monotone_exp.
Section Znearest.
Roundings to nearest: when in the middle, use the choice function
Variable choice : Z → bool.
Definition Znearest x :=
match Rcompare (x - IZR (Zfloor x)) (/2) with
| Lt ⇒ Zfloor x
| Eq ⇒ if choice (Zfloor x) then Zceil x else Zfloor x
| Gt ⇒ Zceil x
end.
Theorem Znearest_DN_or_UP :
∀ x,
Znearest x = Zfloor x ∨ Znearest x = Zceil x.
Theorem Znearest_ge_floor :
∀ x,
(Zfloor x ≤ Znearest x)%Z.
Theorem Znearest_le_ceil :
∀ x,
(Znearest x ≤ Zceil x)%Z.
Global Instance valid_rnd_N : Valid_rnd Znearest.
Theorem Znearest_N_strict :
∀ x,
(x - IZR (Zfloor x) ≠ /2)%R →
(Rabs (x - IZR (Znearest x)) < /2)%R.
Theorem Znearest_half :
∀ x,
(Rabs (x - IZR (Znearest x)) ≤ /2)%R.
Theorem Znearest_imp :
∀ x n,
(Rabs (x - IZR n) < /2)%R →
Znearest x = n.
Theorem round_N_pt :
∀ x,
Rnd_N_pt generic_format x (round Znearest x).
Theorem round_N_middle :
∀ x,
(x - round Zfloor x = round Zceil x - x)%R →
round Znearest x = if choice (Zfloor (scaled_mantissa x)) then round Zceil x else round Zfloor x.
Lemma round_N_small_pos :
∀ x,
∀ ex,
(Raux.bpow beta (ex - 1) ≤ x < Raux.bpow beta ex)%R →
(ex < fexp ex)%Z →
(round Znearest x = 0)%R.
End Znearest.
Section rndNA.
Global Instance valid_rnd_NA : Valid_rnd (Znearest (Zle_bool 0)) := valid_rnd_N _.
Theorem round_NA_pt :
∀ x,
Rnd_NA_pt generic_format x (round (Znearest (Zle_bool 0)) x).
End rndNA.
Notation Znearest0 := (Znearest (fun x ⇒ (Zlt_bool x 0))).
Section rndN0.
Global Instance valid_rnd_N0 : Valid_rnd Znearest0 := valid_rnd_N _.
Theorem round_N0_pt :
∀ x,
Rnd_N0_pt generic_format x (round Znearest0 x).
End rndN0.
Section rndN_opp.
Theorem Znearest_opp :
∀ choice x,
Znearest choice (- x) = (- Znearest (fun t ⇒ negb (choice (- (t + 1))%Z)) x)%Z.
Theorem round_N_opp :
∀ choice,
∀ x,
round (Znearest choice) (-x) = (- round (Znearest (fun t ⇒ negb (choice (- (t + 1))%Z))) x)%R.
Lemma round_N0_opp :
∀ x,
(round Znearest0 (- x) = - round Znearest0 x)%R.
End rndN_opp.
Lemma round_N_small :
∀ choice,
∀ x,
∀ ex,
(Raux.bpow beta (ex - 1) ≤ Rabs x < Raux.bpow beta ex)%R →
(ex < fexp ex)%Z →
(round (Znearest choice) x = 0)%R.
End Format.
Definition Znearest x :=
match Rcompare (x - IZR (Zfloor x)) (/2) with
| Lt ⇒ Zfloor x
| Eq ⇒ if choice (Zfloor x) then Zceil x else Zfloor x
| Gt ⇒ Zceil x
end.
Theorem Znearest_DN_or_UP :
∀ x,
Znearest x = Zfloor x ∨ Znearest x = Zceil x.
Theorem Znearest_ge_floor :
∀ x,
(Zfloor x ≤ Znearest x)%Z.
Theorem Znearest_le_ceil :
∀ x,
(Znearest x ≤ Zceil x)%Z.
Global Instance valid_rnd_N : Valid_rnd Znearest.
Theorem Znearest_N_strict :
∀ x,
(x - IZR (Zfloor x) ≠ /2)%R →
(Rabs (x - IZR (Znearest x)) < /2)%R.
Theorem Znearest_half :
∀ x,
(Rabs (x - IZR (Znearest x)) ≤ /2)%R.
Theorem Znearest_imp :
∀ x n,
(Rabs (x - IZR n) < /2)%R →
Znearest x = n.
Theorem round_N_pt :
∀ x,
Rnd_N_pt generic_format x (round Znearest x).
Theorem round_N_middle :
∀ x,
(x - round Zfloor x = round Zceil x - x)%R →
round Znearest x = if choice (Zfloor (scaled_mantissa x)) then round Zceil x else round Zfloor x.
Lemma round_N_small_pos :
∀ x,
∀ ex,
(Raux.bpow beta (ex - 1) ≤ x < Raux.bpow beta ex)%R →
(ex < fexp ex)%Z →
(round Znearest x = 0)%R.
End Znearest.
Section rndNA.
Global Instance valid_rnd_NA : Valid_rnd (Znearest (Zle_bool 0)) := valid_rnd_N _.
Theorem round_NA_pt :
∀ x,
Rnd_NA_pt generic_format x (round (Znearest (Zle_bool 0)) x).
End rndNA.
Notation Znearest0 := (Znearest (fun x ⇒ (Zlt_bool x 0))).
Section rndN0.
Global Instance valid_rnd_N0 : Valid_rnd Znearest0 := valid_rnd_N _.
Theorem round_N0_pt :
∀ x,
Rnd_N0_pt generic_format x (round Znearest0 x).
End rndN0.
Section rndN_opp.
Theorem Znearest_opp :
∀ choice x,
Znearest choice (- x) = (- Znearest (fun t ⇒ negb (choice (- (t + 1))%Z)) x)%Z.
Theorem round_N_opp :
∀ choice,
∀ x,
round (Znearest choice) (-x) = (- round (Znearest (fun t ⇒ negb (choice (- (t + 1))%Z))) x)%R.
Lemma round_N0_opp :
∀ x,
(round Znearest0 (- x) = - round Znearest0 x)%R.
End rndN_opp.
Lemma round_N_small :
∀ choice,
∀ x,
∀ ex,
(Raux.bpow beta (ex - 1) ≤ Rabs x < Raux.bpow beta ex)%R →
(ex < fexp ex)%Z →
(round (Znearest choice) x = 0)%R.
End Format.
Inclusion of a format into an extended format
Section Inclusion.
Variables fexp1 fexp2 : Z → Z.
Context { valid_exp1 : Valid_exp fexp1 }.
Context { valid_exp2 : Valid_exp fexp2 }.
Theorem generic_inclusion_mag :
∀ x,
( x ≠ 0%R → (fexp2 (mag beta x) ≤ fexp1 (mag beta x))%Z ) →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion_lt_ge :
∀ e1 e2,
( ∀ e, (e1 < e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
∀ x,
(bpow e1 ≤ Rabs x < bpow e2)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion :
∀ e,
(fexp2 e ≤ fexp1 e)%Z →
∀ x,
(bpow (e - 1) ≤ Rabs x ≤ bpow e)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion_le_ge :
∀ e1 e2,
(e1 < e2)%Z →
( ∀ e, (e1 < e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
∀ x,
(bpow e1 ≤ Rabs x ≤ bpow e2)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion_le :
∀ e2,
( ∀ e, (e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
∀ x,
(Rabs x ≤ bpow e2)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion_ge :
∀ e1,
( ∀ e, (e1 < e)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
∀ x,
(bpow e1 ≤ Rabs x)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem generic_round_generic :
∀ x,
generic_format fexp1 x →
generic_format fexp1 (round fexp2 rnd x).
End Inclusion.
End Generic.
Notation ZnearestA := (Znearest (Zle_bool 0)).
Section rndNA_opp.
Lemma round_NA_opp :
∀ beta : radix,
∀ (fexp : Z → Z),
∀ x,
(round beta fexp ZnearestA (- x) = - round beta fexp ZnearestA x)%R.
End rndNA_opp.
Variables fexp1 fexp2 : Z → Z.
Context { valid_exp1 : Valid_exp fexp1 }.
Context { valid_exp2 : Valid_exp fexp2 }.
Theorem generic_inclusion_mag :
∀ x,
( x ≠ 0%R → (fexp2 (mag beta x) ≤ fexp1 (mag beta x))%Z ) →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion_lt_ge :
∀ e1 e2,
( ∀ e, (e1 < e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
∀ x,
(bpow e1 ≤ Rabs x < bpow e2)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion :
∀ e,
(fexp2 e ≤ fexp1 e)%Z →
∀ x,
(bpow (e - 1) ≤ Rabs x ≤ bpow e)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion_le_ge :
∀ e1 e2,
(e1 < e2)%Z →
( ∀ e, (e1 < e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
∀ x,
(bpow e1 ≤ Rabs x ≤ bpow e2)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion_le :
∀ e2,
( ∀ e, (e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
∀ x,
(Rabs x ≤ bpow e2)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Theorem generic_inclusion_ge :
∀ e1,
( ∀ e, (e1 < e)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
∀ x,
(bpow e1 ≤ Rabs x)%R →
generic_format fexp1 x →
generic_format fexp2 x.
Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem generic_round_generic :
∀ x,
generic_format fexp1 x →
generic_format fexp1 (round fexp2 rnd x).
End Inclusion.
End Generic.
Notation ZnearestA := (Znearest (Zle_bool 0)).
Section rndNA_opp.
Lemma round_NA_opp :
∀ beta : radix,
∀ (fexp : Z → Z),
∀ x,
(round beta fexp ZnearestA (- x) = - round beta fexp ZnearestA x)%R.
End rndNA_opp.
Notations for backward-compatibility with Flocq 1.4.