Library Flocq.Core.Round_NE

This file is part of the Flocq formalization of floating-point arithmetic in Coq: https://flocq.gitlabpages.inria.fr/

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.

Rounding to nearest, ties to even: existence, unicity...

From Coq Require Import ZArith Reals Lia.

Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp.

Notation ZnearestE := (Znearest (fun x ⇒ negb (Z.even 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 canonical := (canonical beta fexp).

Definition NE_prop (_ : R) f :=
  ∃ g : float beta , f = F2R g ∧ canonical g ∧ Z.even (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 →
  canonical xd →
  canonical xu →
  F2R xd = round beta fexp Zfloor x →
  F2R xu = round beta fexp Zceil x →
  Z.even (Fnum xu) = negb (Z.even (Fnum xd)).

Definition DN_UP_parity_prop :=
  ∀ x xd xu,
  ¬ format x →
  canonical xd →
  canonical xu →
  F2R xd = round beta fexp Zfloor x →
  F2R xu = round beta fexp Zceil x →
  Z.even (Fnum xu) = negb (Z.even (Fnum xd)).

Lemma DN_UP_parity_aux :
  DN_UP_parity_pos_prop →
  DN_UP_parity_prop.

Class Exists_NE :=
  exists_NE : Z.even 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.

Notation rndNE := ZnearestE (only parsing).