Library Flocq.Core.Fcore_generic_fmt

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

What is a real number belonging to a format, and many properties.

Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_float_prop.

Section Generic.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Section Format.

Variable fexp : ZZ.

To be a good fexp

Class Valid_exp :=
  valid_exp :
   k : Z,
  ( (fexp k < k)%Z → (fexp (k + 1) k)%Z )
  ( (k fexp k)%Z
    (fexp (fexp k + 1) fexp k)%Z
     l : Z, (l fexp k)%Zfexp l = fexp k ).

Context { valid_exp_ : Valid_exp }.

Theorem valid_exp_large :
   k l,
  (fexp k < k)%Z → (k l)%Z
  (fexp l < l)%Z.

Theorem valid_exp_large' :
   k l,
  (fexp k < k)%Z → (l k)%Z
  (fexp l < k)%Z.

Definition canonic_exp x :=
  fexp (ln_beta beta x).

Definition canonic (f : float beta) :=
  Fexp f = canonic_exp (F2R f).

Definition scaled_mantissa x :=
  (x × bpow (- canonic_exp x))%R.

Definition generic_format (x : R) :=
  x = F2R (Float beta (Ztrunc (scaled_mantissa x)) (canonic_exp x)).

Basic facts
Theorem generic_format_0 :
  generic_format 0.

Theorem canonic_exp_opp :
   x,
  canonic_exp (-x) = canonic_exp x.

Theorem canonic_exp_abs :
   x,
  canonic_exp (Rabs x) = canonic_exp x.

Theorem generic_format_bpow :
   e, (fexp (e + 1) e)%Z
  generic_format (bpow e).

Theorem generic_format_bpow' :
   e, (fexp e e)%Z
  generic_format (bpow e).

Theorem generic_format_F2R :
   m e,
  ( m 0 → canonic_exp (F2R (Float beta m e)) e )%Z
  generic_format (F2R (Float beta m e)).

Lemma generic_format_F2R': (x:R) (f:float beta),
       F2R f = x → ((x 0)%R
       (canonic_exp x Fexp f)%Z) →
       generic_format x.

Theorem canonic_opp :
   m e,
  canonic (Float beta m e) →
  canonic (Float beta (-m) e).

Theorem canonic_abs :
   m e,
  canonic (Float beta m e) →
  canonic (Float beta (Zabs m) e).

Theorem canonic_0: canonic (Float beta 0 (fexp (ln_beta beta 0%R))).

Theorem canonic_unicity :
   f1 f2,
  canonic f1
  canonic f2
  F2R f1 = F2R f2
  f1 = f2.

Theorem scaled_mantissa_generic :
   x,
  generic_format x
  scaled_mantissa x = Z2R (Ztrunc (scaled_mantissa x)).

Theorem scaled_mantissa_mult_bpow :
   x,
  (scaled_mantissa x × bpow (canonic_exp x))%R = x.

Theorem scaled_mantissa_0 :
  scaled_mantissa 0 = R0.

Theorem scaled_mantissa_opp :
   x,
  scaled_mantissa (-x) = (-scaled_mantissa x)%R.

Theorem scaled_mantissa_abs :
   x,
  scaled_mantissa (Rabs x) = Rabs (scaled_mantissa x).

Theorem generic_format_opp :
   x, generic_format xgeneric_format (-x).

Theorem generic_format_abs :
   x, generic_format xgeneric_format (Rabs x).

Theorem generic_format_abs_inv :
   x, generic_format (Rabs x) → generic_format x.

Theorem canonic_exp_fexp :
   x ex,
  (bpow (ex - 1) Rabs x < bpow ex)%R
  canonic_exp x = fexp ex.

Theorem canonic_exp_fexp_pos :
   x ex,
  (bpow (ex - 1) x < bpow ex)%R
  canonic_exp x = fexp ex.

Properties when the real number is "small" (kind of subnormal)
Theorem mantissa_small_pos :
   x ex,
  (bpow (ex - 1) x < bpow ex)%R
  (ex fexp ex)%Z
  (0 < x × bpow (- fexp ex) < 1)%R.

Theorem scaled_mantissa_small :
   x ex,
  (Rabs x < bpow ex)%R
  (ex fexp ex)%Z
  (Rabs (scaled_mantissa x) < 1)%R.

Theorem abs_scaled_mantissa_lt_bpow :
   x,
  (Rabs (scaled_mantissa x) < bpow (ln_beta beta x - canonic_exp x))%R.

Theorem ln_beta_generic_gt :
   x, (x 0)%R
  generic_format x
  (canonic_exp x < ln_beta beta x)%Z.

Theorem mantissa_DN_small_pos :
   x ex,
  (bpow (ex - 1) x < bpow ex)%R
  (ex fexp ex)%Z
  Zfloor (x × bpow (- fexp ex)) = Z0.

Theorem mantissa_UP_small_pos :
   x ex,
  (bpow (ex - 1) x < bpow ex)%R
  (ex fexp ex)%Z
  Zceil (x × bpow (- fexp ex)) = 1%Z.

Generic facts about any format
Theorem generic_format_discrete :
   x m,
  let e := canonic_exp x in
  (F2R (Float beta m e) < x < F2R (Float beta (m + 1) e))%R
  ¬ generic_format x.

Theorem generic_format_canonic :
   f, canonic f
  generic_format (F2R f).

Theorem generic_format_ge_bpow :
   emin,
  ( e, (emin fexp e)%Z ) →
   x,
  (0 < x)%R
  generic_format x
  (bpow emin x)%R.

Theorem abs_lt_bpow_prec:
   prec,
  ( e, (e - prec fexp e)%Z) →
  
   x,
  (Rabs x < bpow (prec + canonic_exp x))%R.

Theorem generic_format_bpow_inv' :
   e,
  generic_format (bpow e) →
  (fexp (e + 1) e)%Z.

Theorem generic_format_bpow_inv :
   e,
  generic_format (bpow e) →
  (fexp e e)%Z.

Section Fcore_generic_round_pos.

Rounding functions: R -> Z

Variable rnd : RZ.

Class Valid_rnd := {
  Zrnd_le : x y, (x y)%R → (rnd x rnd y)%Z ;
  Zrnd_Z2R : n, rnd (Z2R n) = n
}.

Context { valid_rnd : Valid_rnd }.

Theorem Zrnd_DN_or_UP :
   x, rnd x = Zfloor x rnd x = Zceil x.

Theorem Zrnd_ZR_or_AW :
   x, rnd x = Ztrunc x rnd x = Zaway x.

the most useful one: R -> F
Definition round x :=
  F2R (Float beta (rnd (scaled_mantissa x)) (canonic_exp x)).

Theorem round_le_pos :
   x y, (0 < x)%R → (x y)%R → (round x round y)%R.

Theorem round_generic :
   x,
  generic_format x
  round x = x.

Theorem round_0 :
  round 0 = R0.

Theorem round_bounded_large_pos :
   x ex,
  (fexp ex < ex)%Z
  (bpow (ex - 1) x < bpow ex)%R
  (bpow (ex - 1) round x bpow ex)%R.

Theorem round_bounded_small_pos :
   x ex,
  (ex fexp ex)%Z
  (bpow (ex - 1) x < bpow ex)%R
  round x = R0 round x = bpow (fexp ex).

Theorem exp_small_round_0_pos :
   x ex,
 (bpow (ex - 1) x < bpow ex)%R
   round x =R0 → (ex fexp ex)%Z .

Theorem generic_format_round_pos :
   x,
  (0 < x)%R
  generic_format (round x).

End Fcore_generic_round_pos.

Theorem round_ext :
   rnd1 rnd2,
  ( x, rnd1 x = rnd2 x ) →
   x,
  round rnd1 x = round rnd2 x.

Section Zround_opp.

Variable rnd : RZ.
Context { valid_rnd : Valid_rnd rnd }.

Definition Zrnd_opp x := Zopp (rnd (-x)).

Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.

Theorem round_opp :
   x,
  round rnd (- x) = Ropp (round Zrnd_opp x).

End Zround_opp.

IEEE-754 roundings: up, down and to zero

Global Instance valid_rnd_DN : Valid_rnd Zfloor.

Global Instance valid_rnd_UP : Valid_rnd Zceil.

Global Instance valid_rnd_ZR : Valid_rnd Ztrunc.

Global Instance valid_rnd_AW : Valid_rnd Zaway.

Section monotone.

Variable rnd : RZ.
Context { valid_rnd : Valid_rnd rnd }.

Theorem round_DN_or_UP :
   x,
  round rnd x = round Zfloor x round rnd x = round Zceil x.

Theorem round_ZR_or_AW :
   x,
  round rnd x = round Ztrunc x round rnd x = round Zaway x.

Theorem round_le :
   x y, (x y)%R → (round rnd x round rnd y)%R.

Theorem round_ge_generic :
   x y, generic_format x → (x y)%R → (x round rnd y)%R.

Theorem round_le_generic :
   x y, generic_format y → (x y)%R → (round rnd x y)%R.

End monotone.

Theorem round_abs_abs' :
   P : RRProp,
  ( rnd (Hr : Valid_rnd rnd) x, (0 x)%RP x (round rnd x) ) →
   rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).

Theorem round_abs_abs :
   P : RRProp,
  ( rnd (Hr : Valid_rnd rnd) x, P x (round rnd x) ) →
   rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).

Theorem round_bounded_large :
   rnd {Hr : Valid_rnd rnd} x ex,
  (fexp ex < ex)%Z
  (bpow (ex - 1) Rabs x < bpow ex)%R
  (bpow (ex - 1) Rabs (round rnd x) bpow ex)%R.

Theorem exp_small_round_0 :
   rnd {Hr : Valid_rnd rnd} x ex,
  (bpow (ex - 1) Rabs x < bpow ex)%R
   round rnd x =R0 → (ex fexp ex)%Z .

Section monotone_abs.

Variable rnd : RZ.
Context { valid_rnd : Valid_rnd rnd }.

Theorem abs_round_ge_generic :
   x y, generic_format x → (x Rabs y)%R → (x Rabs (round rnd y))%R.

Theorem abs_round_le_generic :
   x y, generic_format y → (Rabs x y)%R → (Rabs (round rnd x) y)%R.

End monotone_abs.

Theorem round_DN_opp :
   x,
  round Zfloor (-x) = (- round Zceil x)%R.

Theorem round_UP_opp :
   x,
  round Zceil (-x) = (- round Zfloor x)%R.

Theorem round_ZR_opp :
   x,
  round Ztrunc (- x) = Ropp (round Ztrunc x).

Theorem round_ZR_abs :
   x,
  round Ztrunc (Rabs x) = Rabs (round Ztrunc x).

Theorem round_AW_opp :
   x,
  round Zaway (- x) = Ropp (round Zaway x).

Theorem round_AW_abs :
   x,
  round Zaway (Rabs x) = Rabs (round Zaway x).

Theorem round_ZR_pos :
   x,
  (0 x)%R
  round Ztrunc x = round Zfloor x.

Theorem round_ZR_neg :
   x,
  (x 0)%R
  round Ztrunc x = round Zceil x.

Theorem round_AW_pos :
   x,
  (0 x)%R
  round Zaway x = round Zceil x.

Theorem round_AW_neg :
   x,
  (x 0)%R
  round Zaway x = round Zfloor x.

Theorem generic_format_round :
   rnd { Hr : Valid_rnd rnd } x,
  generic_format (round rnd x).

Theorem round_DN_pt :
   x,
  Rnd_DN_pt generic_format x (round Zfloor x).

Theorem generic_format_satisfies_any :
  satisfies_any generic_format.

Theorem round_UP_pt :
   x,
  Rnd_UP_pt generic_format x (round Zceil x).

Theorem round_ZR_pt :
   x,
  Rnd_ZR_pt generic_format x (round Ztrunc x).

Theorem round_DN_small_pos :
   x ex,
  (bpow (ex - 1) x < bpow ex)%R
  (ex fexp ex)%Z
  round Zfloor x = R0.

Theorem round_DN_UP_lt :
   x, ¬ generic_format x
  (round Zfloor x < x < round Zceil x)%R.

Theorem round_UP_small_pos :
   x ex,
  (bpow (ex - 1) x < bpow ex)%R
  (ex fexp ex)%Z
  round Zceil x = (bpow (fexp ex)).

Theorem generic_format_EM :
   x,
  generic_format x ¬generic_format x.

Section round_large.

Variable rnd : RZ.
Context { valid_rnd : Valid_rnd rnd }.

Theorem round_large_pos_ge_pow :
   x e,
  (0 < round rnd x)%R
  (bpow e x)%R
  (bpow e round rnd x)%R.

End round_large.

Theorem ln_beta_round_ZR :
   x,
  (round Ztrunc x 0)%R
  (ln_beta beta (round Ztrunc x) = ln_beta beta x :> Z).

Theorem ln_beta_round :
   rnd {Hrnd : Valid_rnd rnd} x,
  (round rnd x 0)%R
  (ln_beta beta (round rnd x) = ln_beta beta x :> Z)
  Rabs (round rnd x) = bpow (Zmax (ln_beta beta x) (fexp (ln_beta beta x))).

Theorem ln_beta_round_DN :
   x,
  (0 < round Zfloor x)%R
  (ln_beta beta (round Zfloor x) = ln_beta beta x :> Z).

Theorem canonic_exp_DN :
   x,
  (0 < round Zfloor x)%R
  canonic_exp (round Zfloor x) = canonic_exp x.

Theorem scaled_mantissa_DN :
   x,
  (0 < round Zfloor x)%R
  scaled_mantissa (round Zfloor x) = Z2R (Zfloor (scaled_mantissa x)).

Theorem generic_N_pt_DN_or_UP :
   x f,
  Rnd_N_pt generic_format x f
  f = round Zfloor x f = round Zceil x.

Section not_FTZ.

Class Exp_not_FTZ :=
  exp_not_FTZ : e, (fexp (fexp e + 1) fexp e)%Z.

Context { exp_not_FTZ_ : Exp_not_FTZ }.

Theorem subnormal_exponent :
   e x,
  (e fexp e)%Z
  generic_format x
  x = F2R (Float beta (Ztrunc (x × bpow (- fexp e))) (fexp e)).

End not_FTZ.

Section monotone_exp.

Class Monotone_exp :=
  monotone_exp : ex ey, (ex ey)%Z → (fexp ex fexp ey)%Z.

Context { monotone_exp_ : Monotone_exp }.

Global Instance monotone_exp_not_FTZ : Exp_not_FTZ.

Lemma canonic_exp_le_bpow :
   (x : R) (e : Z),
  x R0
  (Rabs x < bpow e)%R
  (canonic_exp x fexp e)%Z.

Lemma canonic_exp_ge_bpow :
   (x : R) (e : Z),
  (bpow (e - 1) Rabs x)%R
  (fexp e canonic_exp x)%Z.

Variable rnd : RZ.
Context { valid_rnd : Valid_rnd rnd }.

Theorem ln_beta_round_ge :
   x,
  round rnd x R0
  (ln_beta beta x ln_beta beta (round rnd x))%Z.

Theorem canonic_exp_round_ge :
   x,
  round rnd x R0
  (canonic_exp x canonic_exp (round rnd x))%Z.

End monotone_exp.

Section Znearest.

Roundings to nearest: when in the middle, use the choice function
Variable choice : Zbool.

Definition Znearest x :=
  match Rcompare (x - Z2R (Zfloor x)) (/2) with
  | LtZfloor x
  | Eqif choice (Zfloor x) then Zceil x else Zfloor x
  | GtZceil x
  end.

Theorem Znearest_DN_or_UP :
   x,
  Znearest x = Zfloor x Znearest x = Zceil x.

Theorem Znearest_ge_floor :
   x,
  (Zfloor x Znearest x)%Z.

Theorem Znearest_le_ceil :
   x,
  (Znearest x Zceil x)%Z.

Global Instance valid_rnd_N : Valid_rnd Znearest.

Theorem Rcompare_floor_ceil_mid :
   x,
  Z2R (Zfloor x) x
  Rcompare (x - Z2R (Zfloor x)) (/ 2) = Rcompare (x - Z2R (Zfloor x)) (Z2R (Zceil x) - x).

Theorem Rcompare_ceil_floor_mid :
   x,
  Z2R (Zfloor x) x
  Rcompare (Z2R (Zceil x) - x) (/ 2) = Rcompare (Z2R (Zceil x) - x) (x - Z2R (Zfloor x)).

Theorem Znearest_N_strict :
   x,
  (x - Z2R (Zfloor x) /2)%R
  (Rabs (x - Z2R (Znearest x)) < /2)%R.

Theorem Znearest_N :
   x,
  (Rabs (x - Z2R (Znearest x)) /2)%R.

Theorem Znearest_imp :
   x n,
  (Rabs (x - Z2R n) < /2)%R
  Znearest x = n.

Theorem round_N_pt :
   x,
  Rnd_N_pt generic_format x (round Znearest x).

Theorem round_N_middle :
   x,
  (x - round Zfloor x = round Zceil x - x)%R
  round Znearest x = if choice (Zfloor (scaled_mantissa x)) then round Zceil x else round Zfloor x.

End Znearest.

Section rndNA.

Global Instance valid_rnd_NA : Valid_rnd (Znearest (Zle_bool 0)) := valid_rnd_N _.

Theorem round_NA_pt :
   x,
  Rnd_NA_pt generic_format x (round (Znearest (Zle_bool 0)) x).

End rndNA.

Section rndN_opp.

Theorem Znearest_opp :
   choice x,
  Znearest choice (- x) = (- Znearest (fun tnegb (choice (- (t + 1))%Z)) x)%Z.

Theorem round_N_opp :
   choice,
   x,
  round (Znearest choice) (-x) = (- round (Znearest (fun tnegb (choice (- (t + 1))%Z))) x)%R.

End rndN_opp.

End Format.

Inclusion of a format into an extended format
Section Inclusion.

Variables fexp1 fexp2 : ZZ.

Context { valid_exp1 : Valid_exp fexp1 }.
Context { valid_exp2 : Valid_exp fexp2 }.

Theorem generic_inclusion_ln_beta :
   x,
  ( x R0 → (fexp2 (ln_beta beta x) fexp1 (ln_beta beta x))%Z ) →
  generic_format fexp1 x
  generic_format fexp2 x.

Theorem generic_inclusion_lt_ge :
   e1 e2,
  ( e, (e1 < e e2)%Z → (fexp2 e fexp1 e)%Z ) →
   x,
  (bpow e1 Rabs x < bpow e2)%R
  generic_format fexp1 x
  generic_format fexp2 x.

Theorem generic_inclusion :
   e,
  (fexp2 e fexp1 e)%Z
   x,
  (bpow (e - 1) Rabs x bpow e)%R
  generic_format fexp1 x
  generic_format fexp2 x.

Theorem generic_inclusion_le_ge :
   e1 e2,
  (e1 < e2)%Z
  ( e, (e1 < e e2)%Z → (fexp2 e fexp1 e)%Z ) →
   x,
  (bpow e1 Rabs x bpow e2)%R
  generic_format fexp1 x
  generic_format fexp2 x.

Theorem generic_inclusion_le :
   e2,
  ( e, (e e2)%Z → (fexp2 e fexp1 e)%Z ) →
   x,
  (Rabs x bpow e2)%R
  generic_format fexp1 x
  generic_format fexp2 x.

Theorem generic_inclusion_ge :
   e1,
  ( e, (e1 < e)%Z → (fexp2 e fexp1 e)%Z ) →
   x,
  (bpow e1 Rabs x)%R
  generic_format fexp1 x
  generic_format fexp2 x.

Variable rnd : RZ.
Context { valid_rnd : Valid_rnd rnd }.

Theorem generic_round_generic :
   x,
  generic_format fexp1 x
  generic_format fexp1 (round fexp2 rnd x).

End Inclusion.

End Generic.

Notation ZnearestA := (Znearest (Zle_bool 0)).

Notations for backward-compatibility with Flocq 1.4.
Notation rndDN := Zfloor (only parsing).
Notation rndUP := Zceil (only parsing).
Notation rndZR := Ztrunc (only parsing).
Notation rndNA := ZnearestA (only parsing).