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.
Copyright (C) 2009-2018 Guillaume Melquiond
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)).
∀ 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.
∀ 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)).
∀ 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.
∀ 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.