Library Flocq.Core.Float_prop

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

Basic properties of floating-point formats: lemmas about mantissa, exponent...


From Coq Require Import ZArith Reals Lia.

Require Import Zaux Raux Defs Digits.

Section Float_prop.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Theorem Rcompare_F2R :
   e m1 m2 : Z,
  Rcompare (F2R (Float beta m1 e)) (F2R (Float beta m2 e)) = Z.compare m1 m2.

Basic facts
Theorem le_F2R :
   e m1 m2 : Z,
  (F2R (Float beta m1 e) F2R (Float beta m2 e))%R
  (m1 m2)%Z.

Theorem F2R_le :
   m1 m2 e : Z,
  (m1 m2)%Z
  (F2R (Float beta m1 e) F2R (Float beta m2 e))%R.

Theorem lt_F2R :
   e m1 m2 : Z,
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R
  (m1 < m2)%Z.

Theorem F2R_lt :
   e m1 m2 : Z,
  (m1 < m2)%Z
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R.

Theorem F2R_eq :
   e m1 m2 : Z,
  (m1 = m2)%Z
  (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.

Theorem eq_F2R :
   e m1 m2 : Z,
  F2R (Float beta m1 e) = F2R (Float beta m2 e)
  m1 = m2.

Theorem F2R_Zabs:
   m e : Z,
   F2R (Float beta (Z.abs m) e) = Rabs (F2R (Float beta m e)).

Theorem F2R_Zopp :
   m e : Z,
  F2R (Float beta (Z.opp m) e) = Ropp (F2R (Float beta m e)).

Theorem F2R_cond_Zopp :
   b m e,
  F2R (Float beta (cond_Zopp b m) e) = cond_Ropp b (F2R (Float beta m e)).

Sign facts
Theorem F2R_0 :
   e : Z,
  F2R (Float beta 0 e) = 0%R.

Theorem eq_0_F2R :
   m e : Z,
  F2R (Float beta m e) = 0%R
  m = Z0.

Theorem ge_0_F2R :
   m e : Z,
  (0 F2R (Float beta m e))%R
  (0 m)%Z.

Theorem le_0_F2R :
   m e : Z,
  (F2R (Float beta m e) 0)%R
  (m 0)%Z.

Theorem gt_0_F2R :
   m e : Z,
  (0 < F2R (Float beta m e))%R
  (0 < m)%Z.

Theorem lt_0_F2R :
   m e : Z,
  (F2R (Float beta m e) < 0)%R
  (m < 0)%Z.

Theorem F2R_ge_0 :
   f : float beta,
  (0 Fnum f)%Z
  (0 F2R f)%R.

Theorem F2R_le_0 :
   f : float beta,
  (Fnum f 0)%Z
  (F2R f 0)%R.

Theorem F2R_gt_0 :
   f : float beta,
  (0 < Fnum f)%Z
  (0 < F2R f)%R.

Theorem F2R_lt_0 :
   f : float beta,
  (Fnum f < 0)%Z
  (F2R f < 0)%R.

Theorem F2R_neq_0 :
  f : float beta,
  (Fnum f 0)%Z
  (F2R f 0)%R.

Lemma Fnum_ge_0: (f : float beta),
  (0 F2R f)%R (0 Fnum f)%Z.

Lemma Fnum_le_0: (f : float beta),
  (F2R f 0)%R (Fnum f 0)%Z.

Floats and bpow
Theorem F2R_bpow :
   e : Z,
  F2R (Float beta 1 e) = bpow e.

Theorem bpow_le_F2R :
   m e : Z,
  (0 < m)%Z
  (bpow e F2R (Float beta m e))%R.

Theorem F2R_p1_le_bpow :
   m e1 e2 : Z,
  (0 < m)%Z
  (F2R (Float beta m e1) < bpow e2)%R
  (F2R (Float beta (m + 1) e1) bpow e2)%R.

Theorem bpow_le_F2R_m1 :
   m e1 e2 : Z,
  (1 < m)%Z
  (bpow e2 < F2R (Float beta m e1))%R
  (bpow e2 F2R (Float beta (m - 1) e1))%R.

Theorem F2R_lt_bpow :
   f : float beta, e',
  (Z.abs (Fnum f) < Zpower beta (e' - Fexp f))%Z
  (Rabs (F2R f) < bpow e')%R.

Theorem F2R_change_exp :
   e' m e : Z,
  (e' e)%Z
  F2R (Float beta m e) = F2R (Float beta (m × Zpower beta (e - e')) e').

Theorem F2R_prec_normalize :
   m e e' p : Z,
  (Z.abs m < Zpower beta p)%Z
  (bpow (e' - 1)%Z Rabs (F2R (Float beta m e)))%R
  F2R (Float beta m e) = F2R (Float beta (m × Zpower beta (e - e' + p)) (e' - p)).

Floats and mag
Theorem mag_F2R_bounds :
   x m e, (0 < m)%Z
  (F2R (Float beta m e) x < F2R (Float beta (m + 1) e))%R
  mag beta x = mag beta (F2R (Float beta m e)) :> Z.

Theorem mag_F2R :
   m e : Z,
  m Z0
  (mag beta (F2R (Float beta m e)) = mag beta (IZR m) + e :> Z)%Z.

Theorem Zdigits_mag :
   n,
  n Z0
  Zdigits beta n = mag beta (IZR n).

Theorem mag_F2R_Zdigits :
   m e, m Z0
  (mag beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.

Theorem mag_F2R_bounds_Zdigits :
   x m e, (0 < m)%Z
  (F2R (Float beta m e) x < F2R (Float beta (m + 1) e))%R
  mag beta x = (Zdigits beta m + e)%Z :> Z.

Theorem float_distribution_pos :
   m1 e1 m2 e2 : Z,
  (0 < m1)%Z
  (F2R (Float beta m1 e1) < F2R (Float beta m2 e2) < F2R (Float beta (m1 + 1) e1))%R
  (e2 < e1)%Z (e1 + mag beta (IZR m1) = e2 + mag beta (IZR m2))%Z.

End Float_prop.