Library Flocq.Core.Generic_fmt

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

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

From Coq Require Import ZArith Reals Lia.

Require Import Zaux Raux Defs Round_pred Float_prop.

Section Generic.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Section Format.

Variable fexp : Z Z.

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)%Z fexp 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 cexp x :=
  fexp (mag beta x).

Definition canonical (f : float beta) :=
  Fexp f = cexp (F2R f).

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

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

Basic facts
Theorem generic_format_0 :
  generic_format 0.

Theorem cexp_opp :
  cexp (-x) = cexp x.

Theorem cexp_abs :
  cexp (Rabs x) = cexp x.

Theorem canonical_generic_format :
  generic_format x
   f : float beta,
  x = F2R f canonical f.

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 cexp (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 (cexp x Fexp f)%Z)
  generic_format x.

Theorem canonical_opp :
   m e,
  canonical (Float beta m e)
  canonical (Float beta (-m) e).

Theorem canonical_abs :
   m e,
  canonical (Float beta m e)
  canonical (Float beta (Z.abs m) e).

Theorem canonical_0 :
  canonical (Float beta 0 (fexp (mag beta 0%R))).

Theorem canonical_unique :
   f1 f2,
  canonical f1
  canonical f2
  F2R f1 = F2R f2
  f1 = f2.

Theorem scaled_mantissa_generic :
  generic_format x
  scaled_mantissa x = IZR (Ztrunc (scaled_mantissa x)).

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

Theorem scaled_mantissa_0 :
  scaled_mantissa 0 = 0%R.

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

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

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

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

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

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

Theorem cexp_fexp_pos :
   x ex,
  (bpow (ex - 1) x < bpow ex)%R
  cexp 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_lt_1 :
   x ex,
  (Rabs x < bpow ex)%R
  (ex fexp ex)%Z
  (Rabs (scaled_mantissa x) < 1)%R.

Theorem scaled_mantissa_lt_bpow :
  (Rabs (scaled_mantissa x) < bpow (mag beta x - cexp x))%R.

Theorem mag_generic_gt :
   x, (x 0)%R
  generic_format x
  (cexp x < mag beta x)%Z.

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

Lemma 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 := cexp x in
  (F2R (Float beta m e) < x < F2R (Float beta (m + 1) e))%R
  ¬ generic_format x.

Theorem generic_format_canonical :
   f, canonical f
  generic_format (F2R f).

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

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

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

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

Section Fcore_generic_round_pos.

Rounding functions: R -> Z

Variable rnd : R Z.

Class Valid_rnd := {
  Zrnd_le : x y, (x y)%R (rnd x rnd y)%Z ;
  Zrnd_IZR : n, rnd (IZR 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)) (cexp x)).

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 = 0%R round x = bpow (fexp ex).

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

Theorem round_generic :
  generic_format x
  round x = x.

Theorem round_0 :
  round 0 = 0%R.

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

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

End Fcore_generic_round_pos.

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

Section Zround_opp.

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

Definition Zrnd_opp x := Z.opp (rnd (-x)).

Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.

Theorem round_opp :
  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 : R Z.
Context { valid_rnd : Valid_rnd rnd }.

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

Theorem round_ZR_or_AW :
  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 : R R Prop,
  ( rnd (Hr : Valid_rnd rnd) x, (0 x)%R 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 = 0%R (ex fexp ex)%Z .

Section monotone_abs.

Variable rnd : R Z.
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 :
  round Zfloor (-x) = (- round Zceil x)%R.

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

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

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

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

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

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

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

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

Theorem round_AW_DN :
  (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 :
  Rnd_DN_pt generic_format x (round Zfloor x).

Theorem generic_format_satisfies_any :
  satisfies_any generic_format.

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

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

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

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

Lemma 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 :
  generic_format x ¬generic_format x.

Section round_large.

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

Lemma round_large_pos_ge_bpow :
   x e,
  (0 < round rnd x)%R
  (bpow e x)%R
  (bpow e round rnd x)%R.

End round_large.

Theorem mag_round_ZR :
  (round Ztrunc x 0)%R
  (mag beta (round Ztrunc x) = mag beta x :> Z).

Theorem mag_round :
   rnd {Hrnd : Valid_rnd rnd} x,
  (round rnd x 0)%R
  (mag beta (round rnd x) = mag beta x :> Z)
  Rabs (round rnd x) = bpow (Z.max (mag beta x) (fexp (mag beta x))).

Theorem mag_DN :
  (0 < round Zfloor x)%R
  (mag beta (round Zfloor x) = mag beta x :> Z).

Theorem cexp_DN :
  (0 < round Zfloor x)%R
  cexp (round Zfloor x) = cexp x.

Theorem scaled_mantissa_DN :
  (0 < round Zfloor x)%R
  scaled_mantissa (round Zfloor x) = IZR (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 cexp_le_bpow :
   (x : R) (e : Z),
  x 0%R
  (Rabs x < bpow e)%R
  (cexp x fexp e)%Z.

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

Lemma lt_cexp_pos :
   x y,
  (0 < y)%R
  (cexp x < cexp y)%Z
  (x < y)%R.

Theorem lt_cexp :
   x y,
  (y 0)%R
  (cexp x < cexp y)%Z
  (Rabs x < Rabs y)%R.

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem mag_round_ge :
  round rnd x 0%R
  (mag beta x mag beta (round rnd x))%Z.

Theorem cexp_round_ge :
  round rnd x 0%R
  (cexp x cexp (round rnd x))%Z.

End monotone_exp.

Section Znearest.

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

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

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

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

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

Global Instance valid_rnd_N : Valid_rnd Znearest.

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

Theorem Znearest_half :
  (Rabs (x - IZR (Znearest x)) /2)%R.

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

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

Theorem round_N_middle :
  (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.

Lemma round_N_small_pos :
  (Raux.bpow beta (ex - 1) x < Raux.bpow beta ex)%R
  (ex < fexp ex)%Z
  (round Znearest x = 0)%R.

End Znearest.

Section rndNA.

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

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

End rndNA.

Notation Znearest0 := (Znearest (fun x ⇒ (Zlt_bool x 0))).

Section rndN0.

Global Instance valid_rnd_N0 : Valid_rnd Znearest0 := valid_rnd_N _.

Theorem round_N0_pt :
  Rnd_N0_pt generic_format x (round Znearest0 x).

End rndN0.

Section rndN_opp.

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

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

Lemma round_N0_opp :
  (round Znearest0 (- x) = - round Znearest0 x)%R.

End rndN_opp.

Lemma round_N_small :
  (Raux.bpow beta (ex - 1) Rabs x < Raux.bpow beta ex)%R
  (ex < fexp ex)%Z
  (round (Znearest choice) x = 0)%R.

End Format.

Inclusion of a format into an extended format
Section Inclusion.

Variables fexp1 fexp2 : Z Z.

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

Theorem generic_inclusion_mag :
  ( x 0%R (fexp2 (mag beta x) fexp1 (mag 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 )
  (bpow e1 Rabs x < bpow e2)%R
  generic_format fexp1 x
  generic_format fexp2 x.

Theorem generic_inclusion :
  (fexp2 e fexp1 e)%Z
  (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 )
  (bpow e1 Rabs x bpow e2)%R
  generic_format fexp1 x
  generic_format fexp2 x.

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

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

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

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

End Inclusion.

End Generic.

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

Section rndNA_opp.

Lemma round_NA_opp :
   beta : radix,
   (fexp : Z Z),
  (round beta fexp ZnearestA (- x) = - round beta fexp ZnearestA x)%R.

End rndNA_opp.

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).