Library Flocq.Core.Fcore_float_prop

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 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...

Require Import Fcore_Raux.
Require Import Fcore_defs.

Section Float_prop.

Variable beta : radix.

Notation bpow e := (bpow beta e).

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

Basic facts
Theorem F2R_le_reg :
  forall e m1 m2 : Z,
  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R ->
  (m1 <= m2)%Z.

Theorem F2R_le_compat :
  forall m1 m2 e : Z,
  (m1 <= m2)%Z ->
  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R.

Theorem F2R_lt_reg :
  forall e m1 m2 : Z,
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R ->
  (m1 < m2)%Z.

Theorem F2R_lt_compat :
  forall e m1 m2 : Z,
  (m1 < m2)%Z ->
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R.

Theorem F2R_eq_compat :
  forall e m1 m2 : Z,
  (m1 = m2)%Z ->
  (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.

Theorem F2R_eq_reg :
  forall e m1 m2 : Z,
  F2R (Float beta m1 e) = F2R (Float beta m2 e) ->
  m1 = m2.

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

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

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

Theorem F2R_eq_0_reg :
  forall m e : Z,
  F2R (Float beta m e) = R0 ->
  m = Z0.

Theorem F2R_ge_0_reg :
  forall m e : Z,
  (0 <= F2R (Float beta m e))%R ->
  (0 <= m)%Z.

Theorem F2R_le_0_reg :
  forall m e : Z,
  (F2R (Float beta m e) <= 0)%R ->
  (m <= 0)%Z.

Theorem F2R_gt_0_reg :
  forall m e : Z,
  (0 < F2R (Float beta m e))%R ->
  (0 < m)%Z.

Theorem F2R_lt_0_reg :
  forall m e : Z,
  (F2R (Float beta m e) < 0)%R ->
  (m < 0)%Z.

Theorem F2R_ge_0_compat :
  forall f : float beta,
  (0 <= Fnum f)%Z ->
  (0 <= F2R f)%R.

Theorem F2R_le_0_compat :
  forall f : float beta,
  (Fnum f <= 0)%Z ->
  (F2R f <= 0)%R.

Theorem F2R_gt_0_compat :
  forall f : float beta,
  (0 < Fnum f)%Z ->
  (0 < F2R f)%R.

Theorem F2R_lt_0_compat :
  forall f : float beta,
  (Fnum f < 0)%Z ->
  (F2R f < 0)%R.

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

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

Theorem F2R_p1_le_bpow :
  forall 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 :
  forall 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 :
  forall f : float beta, forall e',
  (Zabs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
  (Rabs (F2R f) < bpow e')%R.

Theorem F2R_change_exp :
  forall 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 :
  forall m e e' p : Z,
  (Zabs 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 ln_beta
Theorem ln_beta_F2R_bounds :
  forall x m e, (0 < m)%Z ->
  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
  ln_beta beta x = ln_beta beta (F2R (Float beta m e)) :> Z.

Theorem ln_beta_F2R :
  forall m e : Z,
  m <> Z0 ->
  (ln_beta beta (F2R (Float beta m e)) = ln_beta beta (Z2R m) + e :> Z)%Z.

Theorem float_distribution_pos :
  forall 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 + ln_beta beta (Z2R m1) = e2 + ln_beta beta (Z2R m2))%Z.

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

End Float_prop.