Library Flocq.Pff.Pff2FlocqAux

This file is part of the Flocq formalization of floating-point arithmetic in Coq: https://flocq.gitlabpages.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

From Coq Require Import Lia.
Require Import Pff Core.

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
          | true ⇒ ru
          | false ⇒ rd
          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 (Z.abs_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 (Z.abs_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 (Z.abs_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 (Z.abs_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 (Z.abs_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:Z →bool ),
      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.