Library Flocq.Appli.Fappli_rnd_odd
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010-2013 Sylvie Boldo
Copyright (C) 2010-2013 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) 2010-2013 Guillaume Melquiond
Rounding to odd and its properties, including the equivalence
between rnd_NE and double rounding with rnd_odd and then rnd_NERequire Import Fcore.
Require Import Fcalc_ops.
Definition Zrnd_odd x := match Req_EM_T x (Z2R (Zfloor x)) with
| left _ ⇒ Zfloor x
| right _ ⇒ match (Zeven (Zfloor x)) with
| true ⇒ Zceil x
| false ⇒ Zfloor x
end
end.
Global Instance valid_rnd_odd : Valid_rnd Zrnd_odd.
Lemma Zrnd_odd_Zodd: ∀ x, x ≠ (Z2R (Zfloor x)) →
(Zeven (Zrnd_odd x)) = false.
Section Fcore_rnd_odd.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable fexp : Z → Z.
Context { valid_exp : Valid_exp fexp }.
Context { exists_NE_ : Exists_NE beta fexp }.
Notation format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Notation cexp := (canonic_exp beta fexp).
Definition Rnd_odd_pt (x f : R) :=
format f ∧ ((f = x)%R ∨
((Rnd_DN_pt format x f ∨ Rnd_UP_pt format x f) ∧
∃ g : float beta, f = F2R g ∧ canonic g ∧ Zeven (Fnum g) = false)).
Definition Rnd_odd (rnd : R → R) :=
∀ x : R, Rnd_odd_pt x (rnd x).
Theorem Rnd_odd_pt_sym : ∀ x f : R,
Rnd_odd_pt (-x) (-f) → Rnd_odd_pt x f.
Theorem round_odd_opp :
∀ x,
(round beta fexp Zrnd_odd (-x) = (- round beta fexp Zrnd_odd x))%R.
Theorem round_odd_pt :
∀ x,
Rnd_odd_pt x (round beta fexp Zrnd_odd x).
End Fcore_rnd_odd.
Section Odd_prop_aux.
Variable beta : radix.
Hypothesis Even_beta: Zeven (radix_val beta)=true.
Notation bpow e := (bpow beta e).
Variable fexp : Z → Z.
Variable fexpe : Z → Z.
Context { valid_exp : Valid_exp fexp }.
Context { exists_NE_ : Exists_NE beta fexp }. Context { valid_expe : Valid_exp fexpe }.
Context { exists_NE_e : Exists_NE beta fexpe }.
Hypothesis fexpe_fexp: ∀ e, (fexpe e ≤ fexp e -2)%Z.
Lemma generic_format_fexpe_fexp: ∀ x,
generic_format beta fexp x → generic_format beta fexpe x.
Lemma exists_even_fexp_lt: ∀ (c:Z→Z), ∀ (x:R),
(∃ f:float beta, F2R f = x ∧ (c (ln_beta beta x) < Fexp f)%Z) →
∃ f:float beta, F2R f =x ∧ canonic beta c f ∧ Zeven (Fnum f) = true.
Variable choice:Z→bool.
Variable x:R.
Variable d u: float beta.
Hypothesis Hd: Rnd_DN_pt (generic_format beta fexp) x (F2R d).
Hypothesis Cd: canonic beta fexp d.
Hypothesis Hu: Rnd_UP_pt (generic_format beta fexp) x (F2R u).
Hypothesis Cu: canonic beta fexp u.
Hypothesis xPos: (0 < x)%R.
Let m:= ((F2R d+F2R u)/2)%R.
Lemma d_eq: F2R d= round beta fexp Zfloor x.
Lemma u_eq: F2R u= round beta fexp Zceil x.
Lemma d_ge_0: (0 ≤ F2R d)%R.
Lemma ln_beta_d: (0< F2R d)%R →
(ln_beta beta (F2R d) = ln_beta beta x :>Z).
Lemma Fexp_d: (0 < F2R d)%R → Fexp d =fexp (ln_beta beta x).
Lemma format_bpow_x: (0 < F2R d)%R
→ generic_format beta fexp (bpow (ln_beta beta x)).
Lemma format_bpow_d: (0 < F2R d)%R →
generic_format beta fexp (bpow (ln_beta beta (F2R d))).
Lemma d_le_m: (F2R d ≤ m)%R.
Lemma m_le_u: (m ≤ F2R u)%R.
Lemma ln_beta_m: (0 < F2R d)%R → (ln_beta beta m =ln_beta beta (F2R d) :>Z).
Lemma ln_beta_m_0: (0 = F2R d)%R
→ (ln_beta beta m =ln_beta beta (F2R u)-1:>Z)%Z.
Lemma u'_eq: (0 < F2R d)%R → ∃ f:float beta, F2R f = F2R u ∧ (Fexp f = Fexp d)%Z.
Lemma m_eq: (0 < F2R d)%R → ∃ f:float beta,
F2R f = m ∧ (Fexp f = fexp (ln_beta beta x) -1)%Z.
Lemma m_eq_0: (0 = F2R d)%R → ∃ f:float beta,
F2R f = m ∧ (Fexp f = fexp (ln_beta beta (F2R u)) -1)%Z.
Lemma fexp_m_eq_0: (0 = F2R d)%R →
(fexp (ln_beta beta (F2R u)-1) < fexp (ln_beta beta (F2R u))+1)%Z.
Lemma Fm: generic_format beta fexpe m.
Lemma Zm:
∃ g : float beta, F2R g = m ∧ canonic beta fexpe g ∧ Zeven (Fnum g) = true.
Lemma DN_odd_d_aux: ∀ z, (F2R d≤ z< F2R u)%R →
Rnd_DN_pt (generic_format beta fexp) z (F2R d).
Lemma UP_odd_d_aux: ∀ z, (F2R d< z ≤ F2R u)%R →
Rnd_UP_pt (generic_format beta fexp) z (F2R u).
Theorem round_odd_prop_pos:
round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
round beta fexp (Znearest choice) x.
End Odd_prop_aux.
Section Odd_prop.
Variable beta : radix.
Hypothesis Even_beta: Zeven (radix_val beta)=true.
Variable fexp : Z → Z.
Variable fexpe : Z → Z.
Variable choice:Z→bool.
Context { valid_exp : Valid_exp fexp }.
Context { exists_NE_ : Exists_NE beta fexp }. Context { valid_expe : Valid_exp fexpe }.
Context { exists_NE_e : Exists_NE beta fexpe }.
Hypothesis fexpe_fexp: ∀ e, (fexpe e ≤ fexp e -2)%Z.
Theorem canonizer: ∀ f, generic_format beta fexp f
→ ∃ g : float beta, f = F2R g ∧ canonic beta fexp g.
Theorem round_odd_prop: ∀ x,
round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
round beta fexp (Znearest choice) x.
End Odd_prop.