Library Flocq.Prop.Round_odd

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2013-2018 Sylvie Boldo
Copyright (C) 2013-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.

Rounding to odd and its properties, including the equivalence

between rnd_NE and double rounding with rnd_odd and then rnd_NE

Require Import Reals Psatz.
Require Import Core Operations.

Definition Zrnd_odd x := match Req_EM_T x (IZR (Zfloor x)) with
  | left _Zfloor x
  | right _match (Z.even (Zfloor x)) with
      | trueZceil x
      | falseZfloor x
     end
  end.

Global Instance valid_rnd_odd : Valid_rnd Zrnd_odd.

Lemma Zrnd_odd_Zodd: x, x (IZR (Zfloor x))
  (Z.even (Zrnd_odd x)) = false.

Lemma Zfloor_plus: (n:Z) y,
  (Zfloor (IZR n+y) = n + Zfloor y)%Z.

Lemma Zceil_plus: (n:Z) y,
  (Zceil (IZR n+y) = n + Zceil y)%Z.

Lemma Zeven_abs: z, Z.even (Zabs z) = Z.even z.

Lemma Zrnd_odd_plus: x y, (x = IZR (Zfloor x))
    Z.even (Zfloor x) = true
   (IZR (Zrnd_odd (x+y)) = x+IZR (Zrnd_odd y))%R.

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 canonical := (canonical beta fexp).
Notation cexp := (cexp 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 canonical g Z.even (Fnum g) = false)).

Definition Rnd_odd (rnd : R R) :=
   x : R, Rnd_odd_pt x (rnd x).

Theorem Rnd_odd_pt_opp_inv : 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).

Theorem Rnd_odd_pt_unique :
   x f1 f2 : R,
  Rnd_odd_pt x f1 Rnd_odd_pt x f2
  f1 = f2.

Theorem Rnd_odd_pt_monotone :
  round_pred_monotone (Rnd_odd_pt).

End Fcore_rnd_odd.

Section Odd_prop_aux.

Variable beta : radix.
Hypothesis Even_beta: Z.even (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:ZZ), (x:R),
      ( f:float beta, F2R f = x (c (mag beta x) < Fexp f)%Z)
       f:float beta, F2R f =x canonical beta c f Z.even (Fnum f) = true.

Variable choice:Zbool.
Variable x:R.

Variable d u: float beta.
Hypothesis Hd: Rnd_DN_pt (generic_format beta fexp) x (F2R d).
Hypothesis Cd: canonical beta fexp d.
Hypothesis Hu: Rnd_UP_pt (generic_format beta fexp) x (F2R u).
Hypothesis Cu: canonical 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 mag_d: (0< F2R d)%R
    (mag beta (F2R d) = mag beta x :>Z).

Lemma Fexp_d: (0 < F2R d)%R Fexp d =fexp (mag beta x).

Lemma format_bpow_x: (0 < F2R d)%R
     generic_format beta fexp (bpow (mag beta x)).

Lemma format_bpow_d: (0 < F2R d)%R
  generic_format beta fexp (bpow (mag beta (F2R d))).

Lemma d_le_m: (F2R d m)%R.

Lemma m_le_u: (m F2R u)%R.

Lemma mag_m: (0 < F2R d)%R (mag beta m =mag beta (F2R d) :>Z).

Lemma mag_m_0: (0 = F2R d)%R
     (mag beta m =mag 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 (mag beta x) - 1)%Z.

Lemma m_eq_0: (0 = F2R d)%R f:float beta,
   F2R f = m (Fexp f = fexp (mag beta (F2R u)) -1)%Z.

Lemma fexp_m_eq_0: (0 = F2R d)%R
  (fexp (mag beta (F2R u)-1) < fexp (mag beta (F2R u))+1)%Z.

Lemma Fm: generic_format beta fexpe m.

Lemma Zm:
    g : float beta, F2R g = m canonical beta fexpe g Z.even (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).

Lemma round_N_odd_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: Z.even (radix_val beta)=true.

Variable fexp : Z Z.
Variable fexpe : Z Z.
Variable choice:Zbool.

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 round_N_odd :
   x,
  round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
               round beta fexp (Znearest choice) x.

End Odd_prop.

Section Odd_propbis.

Variable beta : radix.
Hypothesis Even_beta: Z.even (radix_val beta)=true.

Variable emin prec:Z.
Variable choice:Zbool.

Hypothesis prec_gt_1: (1 < prec)%Z.

Notation format := (generic_format beta (FLT_exp emin prec)).
Notation round_flt :=(round beta (FLT_exp emin prec) (Znearest choice)).
Notation cexp_flt := (cexp beta (FLT_exp emin prec)).
Notation fexpe k := (FLT_exp (emin-k) (prec+k)).

Lemma Zrnd_odd_plus': x y,
  ( n:Z, e:Z, (x = IZR n×bpow beta e)%R (1 e)%Z)
   (IZR (Zrnd_odd (x+y)) = x+IZR (Zrnd_odd y))%R.

Theorem mag_round_odd: (x:R),
 (emin < mag beta x)%Z
  (mag_val beta _ (mag beta (round beta (FLT_exp emin prec) Zrnd_odd x))
      = mag_val beta x (mag beta x))%Z.

Theorem fexp_round_odd: (x:R),
  (cexp_flt (round beta (FLT_exp emin prec) Zrnd_odd x)
      = cexp_flt x)%Z.

End Odd_propbis.