Library Flocq.Pff.Pff2FlocqAux

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.
Translation from Flocq to Pff

Require Import Pff Core Binary.

Section RND_Closest_c.
Variable b : Fbound.
Variable beta : radix.
Variable p : nat.

Coercion FtoRradix := FtoR beta.
Hypothesis pGreaterThanOne : 1 < p.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat beta p.

Variable choice: Z bool.

Definition RND_Closest (r : R) :=
   let ru := RND_Max b beta p r in
   let rd := RND_Min b beta p r in
  match Rle_dec (Rabs (ru - r)) (Rabs (rd - r)) with
  | left H
      match
        Rle_lt_or_eq_dec (Rabs (ru - r)) (Rabs (rd - r)) H
      with
      | left _ru
      | right _
          match choice (Zfloor (scaled_mantissa beta (FLT_exp (- dExp b) p) r)) with
          | trueru
          | falserd
          end
      end
  | right _rd
  end.

Theorem RND_Closest_canonic :
  r : R, Fcanonic beta b (RND_Closest r).

Theorem RND_Closest_correct :
  r : R, Closest b beta r (RND_Closest r).

End RND_Closest_c.

Section Bounds.

Variable beta : radix.
Variable p E:Z.
Hypothesis precisionNotZero : (1 < p)%Z.

Definition make_bound := Bound
      (Z.to_pos (Zpower beta p))
      (Z.abs_N E).

Lemma make_bound_Emin: (E 0)%Z
        ((Z_of_N (dExp (make_bound)))=-E)%Z.

Lemma make_bound_p:
        Zpos (vNum (make_bound))=(Zpower_nat beta (Zabs_nat p)).

Lemma FtoR_F2R: (f:Pff.float) (g: float beta), Pff.Fnum f = Fnum g Pff.Fexp f = Fexp g
  FtoR beta f = F2R g.

End Bounds.
Section b_Bounds.

Definition bsingle := make_bound radix2 24 (-149)%Z.

Lemma psGivesBound: Zpos (vNum bsingle) = Zpower_nat 2 24.

Definition bdouble := make_bound radix2 53 1074.

Lemma pdGivesBound: Zpos (vNum bdouble) = Zpower_nat 2 53.

End b_Bounds.
Section Equiv.

Variable beta: radix.
Variable b : Fbound.
Variable p : Z.

Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat beta (Zabs_nat p).
Hypothesis precisionNotZero : (1 < p)%Z.

Lemma pff_format_is_format: f, Fbounded b f
  (generic_format beta (FLT_exp (-dExp b) p) (FtoR beta f)).

Lemma format_is_pff_format': r,
   (generic_format beta (FLT_exp (-dExp b) p) r)
    Fbounded b (Pff.Float (Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) r))
                            (cexp beta (FLT_exp (-dExp b) p) r)).

Lemma format_is_pff_format: r,
  (generic_format beta (FLT_exp (-dExp b) p) r)
   f, FtoR beta f = r Fbounded b f.

Lemma format_is_pff_format_can: r,
  (generic_format beta (FLT_exp (-dExp b) p) r)
   f, FtoR beta f = r Fcanonic beta b f.

Lemma equiv_RNDs_aux: z, Z.even z = true Even z.

Lemma pff_canonic_is_canonic: f, Fcanonic beta b f FtoR beta f 0
  canonical beta (FLT_exp (- dExp b) p)
    (Float beta (Pff.Fnum f) (Pff.Fexp f)).

Lemma pff_round_NE_is_round: (r:R),
   (FtoR beta (RND_EvenClosest b beta (Zabs_nat p) r)
     = round beta (FLT_exp (-dExp b) p) rndNE r).

Lemma round_NE_is_pff_round: (r:R),
    f:Pff.float, (Fcanonic beta b f (EvenClosest b beta (Zabs_nat p) r f)
    FtoR beta f = round beta (FLT_exp (-dExp b) p) rndNE r).

Lemma pff_round_UP_is_round: (r:R),
  FtoR beta (RND_Max b beta (Z.abs_nat p) r)
             = round beta (FLT_exp (- dExp b) p) Zceil r.

Lemma pff_round_DN_is_round: (r:R),
  FtoR beta (RND_Min b beta (Z.abs_nat p) r)
             = round beta (FLT_exp (- dExp b) p) Zfloor r.

Lemma pff_round_N_is_round: choice, (r:R),
   (FtoR beta (RND_Closest b beta (Zabs_nat p) choice r)
     = round beta (FLT_exp (-dExp b) p) (Znearest choice) r).

Lemma round_N_is_pff_round: choice, (r:R),
    f:Pff.float, (Fcanonic beta b f (Closest b beta r f)
    FtoR beta f = round beta (FLT_exp (-dExp b) p) (Znearest choice) r).

Lemma pff_round_is_round_N: r f, Closest b beta r f
     (choice:Zbool),
      FtoR beta f = round beta (FLT_exp (-dExp b) p) (Znearest choice) r.

Lemma FloatFexp_gt: e f, Fbounded b f
  (bpow beta (e+p) Rabs (FtoR beta f))%R
       (e < Pff.Fexp f)%Z.

Lemma CanonicGeNormal: f, Fcanonic beta b f
  (bpow beta (-dExp b+p-1) Rabs (FtoR beta f))%R
       (Fnormal beta b f)%Z.

Lemma Fulp_ulp_aux: f, Fcanonic beta b f
   Fulp b beta (Z.abs_nat p) f
    = ulp beta (FLT_exp (-dExp b) p) (FtoR beta f).

Lemma Fulp_ulp: f, Fbounded b f
   Fulp b beta (Z.abs_nat p) f
    = ulp beta (FLT_exp (-dExp b) p) (FtoR beta f).

End Equiv.

Section Equiv_instanc.

Lemma round_NE_is_pff_round_b32: (r:R),
    f:Pff.float, (Fcanonic 2 bsingle f (EvenClosest bsingle 2 24 r f)
    FtoR 2 f = round radix2 (FLT_exp (-149) 24) rndNE r).

Lemma round_NE_is_pff_round_b64: (r:R),
    f:Pff.float, (Fcanonic 2 bdouble f (EvenClosest bdouble 2 53 r f)
    FtoR 2 f = round radix2 (FLT_exp (-1074) 53) rndNE r).

End Equiv_instanc.