Library Flocq.Core.Fcore_rnd_ne
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 nearest, ties to even: existence, unicity...
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_ulp.
Notation ZnearestE := (Znearest (fun x ⇒ negb (Zeven x))).
Section Fcore_rnd_NE.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable fexp : Z → Z.
Context { valid_exp : Valid_exp fexp }.
Notation format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Definition NE_prop (_ : R) f :=
∃ g : float beta, f = F2R g ∧ canonic g ∧ Zeven (Fnum g) = true.
Definition Rnd_NE_pt :=
Rnd_NG_pt format NE_prop.
Definition DN_UP_parity_pos_prop :=
∀ x xd xu,
(0 < x)%R →
¬ format x →
canonic xd →
canonic xu →
F2R xd = round beta fexp Zfloor x →
F2R xu = round beta fexp Zceil x →
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
Definition DN_UP_parity_prop :=
∀ x xd xu,
¬ format x →
canonic xd →
canonic xu →
F2R xd = round beta fexp Zfloor x →
F2R xu = round beta fexp Zceil x →
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
Lemma DN_UP_parity_aux :
DN_UP_parity_pos_prop →
DN_UP_parity_prop.
Class Exists_NE :=
exists_NE : Zeven beta = false ∨ ∀ e,
((fexp e < e)%Z → (fexp (e + 1) < e)%Z) ∧ ((e ≤ fexp e)%Z → fexp (fexp e + 1) = fexp e).
Context { exists_NE_ : Exists_NE }.
Theorem DN_UP_parity_generic_pos :
DN_UP_parity_pos_prop.
Theorem DN_UP_parity_generic :
DN_UP_parity_prop.
Theorem Rnd_NE_pt_total :
round_pred_total Rnd_NE_pt.
Theorem Rnd_NE_pt_monotone :
round_pred_monotone Rnd_NE_pt.
Theorem Rnd_NE_pt_round :
round_pred Rnd_NE_pt.
Lemma round_NE_pt_pos :
∀ x,
(0 < x)%R →
Rnd_NE_pt x (round beta fexp ZnearestE x).
Theorem round_NE_opp :
∀ x,
round beta fexp ZnearestE (-x) = (- round beta fexp ZnearestE x)%R.
Lemma round_NE_abs:
∀ x : R,
round beta fexp ZnearestE (Rabs x) = Rabs (round beta fexp ZnearestE x).
Theorem round_NE_pt :
∀ x,
Rnd_NE_pt x (round beta fexp ZnearestE x).
End Fcore_rnd_NE.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_ulp.
Notation ZnearestE := (Znearest (fun x ⇒ negb (Zeven x))).
Section Fcore_rnd_NE.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable fexp : Z → Z.
Context { valid_exp : Valid_exp fexp }.
Notation format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Definition NE_prop (_ : R) f :=
∃ g : float beta, f = F2R g ∧ canonic g ∧ Zeven (Fnum g) = true.
Definition Rnd_NE_pt :=
Rnd_NG_pt format NE_prop.
Definition DN_UP_parity_pos_prop :=
∀ x xd xu,
(0 < x)%R →
¬ format x →
canonic xd →
canonic xu →
F2R xd = round beta fexp Zfloor x →
F2R xu = round beta fexp Zceil x →
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
Definition DN_UP_parity_prop :=
∀ x xd xu,
¬ format x →
canonic xd →
canonic xu →
F2R xd = round beta fexp Zfloor x →
F2R xu = round beta fexp Zceil x →
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
Lemma DN_UP_parity_aux :
DN_UP_parity_pos_prop →
DN_UP_parity_prop.
Class Exists_NE :=
exists_NE : Zeven beta = false ∨ ∀ e,
((fexp e < e)%Z → (fexp (e + 1) < e)%Z) ∧ ((e ≤ fexp e)%Z → fexp (fexp e + 1) = fexp e).
Context { exists_NE_ : Exists_NE }.
Theorem DN_UP_parity_generic_pos :
DN_UP_parity_pos_prop.
Theorem DN_UP_parity_generic :
DN_UP_parity_prop.
Theorem Rnd_NE_pt_total :
round_pred_total Rnd_NE_pt.
Theorem Rnd_NE_pt_monotone :
round_pred_monotone Rnd_NE_pt.
Theorem Rnd_NE_pt_round :
round_pred Rnd_NE_pt.
Lemma round_NE_pt_pos :
∀ x,
(0 < x)%R →
Rnd_NE_pt x (round beta fexp ZnearestE x).
Theorem round_NE_opp :
∀ x,
round beta fexp ZnearestE (-x) = (- round beta fexp ZnearestE x)%R.
Lemma round_NE_abs:
∀ x : R,
round beta fexp ZnearestE (Rabs x) = Rabs (round beta fexp ZnearestE x).
Theorem round_NE_pt :
∀ x,
Rnd_NE_pt x (round beta fexp ZnearestE x).
End Fcore_rnd_NE.
Notations for backward-compatibility with Flocq 1.4.