Module Fcore_generic_fmt
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 :
Z ->
Z.
To be a good fexp
Class Valid_exp :=
valid_exp :
forall k :
Z,
( (
fexp k <
k)%
Z -> (
fexp (
k + 1) <=
k)%
Z ) /\
( (
k <=
fexp k)%
Z ->
(
fexp (
fexp k + 1) <=
fexp k)%
Z /\
forall l :
Z, (
l <=
fexp k)%
Z ->
fexp l =
fexp k ).
Context {
valid_exp_ :
Valid_exp }.
Theorem valid_exp_large :
forall k l,
(
fexp k <
k)%
Z -> (
k <=
l)%
Z ->
(
fexp l <
l)%
Z.
Proof.
Theorem valid_exp_large' :
forall k l,
(
fexp k <
k)%
Z -> (
l <=
k)%
Z ->
(
fexp l <
k)%
Z.
Proof.
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.
Proof.
Theorem canonic_exp_opp :
forall x,
canonic_exp (-
x) =
canonic_exp x.
Proof.
Theorem canonic_exp_abs :
forall x,
canonic_exp (
Rabs x) =
canonic_exp x.
Proof.
Theorem generic_format_bpow :
forall e, (
fexp (
e + 1) <=
e)%
Z ->
generic_format (
bpow e).
Proof.
Theorem generic_format_bpow' :
forall e, (
fexp e <=
e)%
Z ->
generic_format (
bpow e).
Proof.
Theorem generic_format_F2R :
forall m e,
(
m <> 0 ->
canonic_exp (
F2R (
Float beta m e)) <=
e )%
Z ->
generic_format (
F2R (
Float beta m e)).
Proof.
Lemma generic_format_F2R':
forall (
x:
R) (
f:
float beta),
F2R f =
x -> ((
x <> 0)%
R ->
(
canonic_exp x <=
Fexp f)%
Z) ->
generic_format x.
Proof.
intros x f H1 H2.
rewrite <-
H1;
destruct f as (
m,
e).
apply generic_format_F2R.
simpl in *;
intros H3.
rewrite H1;
apply H2.
intros Y;
apply H3.
apply F2R_eq_0_reg with beta e.
now rewrite H1.
Qed.
Theorem canonic_opp :
forall m e,
canonic (
Float beta m e) ->
canonic (
Float beta (-
m)
e).
Proof.
Theorem canonic_abs :
forall m e,
canonic (
Float beta m e) ->
canonic (
Float beta (
Zabs m)
e).
Proof.
Theorem canonic_0:
canonic (
Float beta 0 (
fexp (
ln_beta beta 0%
R))).
Proof.
Theorem canonic_unicity :
forall f1 f2,
canonic f1 ->
canonic f2 ->
F2R f1 =
F2R f2 ->
f1 =
f2.
Proof.
intros (
m1,
e1) (
m2,
e2).
unfold canonic.
simpl.
intros H1 H2 H.
rewrite H in H1.
rewrite <-
H2 in H1.
clear H2.
rewrite H1 in H |- *.
apply (
f_equal (
fun m =>
Float beta m e2)).
apply F2R_eq_reg with (1 :=
H).
Qed.
Theorem scaled_mantissa_generic :
forall x,
generic_format x ->
scaled_mantissa x =
Z2R (
Ztrunc (
scaled_mantissa x)).
Proof.
Theorem scaled_mantissa_mult_bpow :
forall x,
(
scaled_mantissa x *
bpow (
canonic_exp x))%
R =
x.
Proof.
Theorem scaled_mantissa_0 :
scaled_mantissa 0 =
R0.
Proof.
Theorem scaled_mantissa_opp :
forall x,
scaled_mantissa (-
x) = (-
scaled_mantissa x)%
R.
Proof.
Theorem scaled_mantissa_abs :
forall x,
scaled_mantissa (
Rabs x) =
Rabs (
scaled_mantissa x).
Proof.
Theorem generic_format_opp :
forall x,
generic_format x ->
generic_format (-
x).
Proof.
Theorem generic_format_abs :
forall x,
generic_format x ->
generic_format (
Rabs x).
Proof.
Theorem generic_format_abs_inv :
forall x,
generic_format (
Rabs x) ->
generic_format x.
Proof.
Theorem canonic_exp_fexp :
forall x ex,
(
bpow (
ex - 1) <=
Rabs x <
bpow ex)%
R ->
canonic_exp x =
fexp ex.
Proof.
Theorem canonic_exp_fexp_pos :
forall x ex,
(
bpow (
ex - 1) <=
x <
bpow ex)%
R ->
canonic_exp x =
fexp ex.
Proof.
Properties when the real number is "small" (kind of subnormal)
Theorem mantissa_small_pos :
forall x ex,
(
bpow (
ex - 1) <=
x <
bpow ex)%
R ->
(
ex <=
fexp ex)%
Z ->
(0 <
x *
bpow (-
fexp ex) < 1)%
R.
Proof.
Theorem scaled_mantissa_small :
forall x ex,
(
Rabs x <
bpow ex)%
R ->
(
ex <=
fexp ex)%
Z ->
(
Rabs (
scaled_mantissa x) < 1)%
R.
Proof.
Theorem abs_scaled_mantissa_lt_bpow :
forall x,
(
Rabs (
scaled_mantissa x) <
bpow (
ln_beta beta x -
canonic_exp x))%
R.
Proof.
Theorem ln_beta_generic_gt :
forall x, (
x <> 0)%
R ->
generic_format x ->
(
canonic_exp x <
ln_beta beta x)%
Z.
Proof.
Theorem mantissa_DN_small_pos :
forall x ex,
(
bpow (
ex - 1) <=
x <
bpow ex)%
R ->
(
ex <=
fexp ex)%
Z ->
Zfloor (
x *
bpow (-
fexp ex)) =
Z0.
Proof.
Theorem mantissa_UP_small_pos :
forall x ex,
(
bpow (
ex - 1) <=
x <
bpow ex)%
R ->
(
ex <=
fexp ex)%
Z ->
Zceil (
x *
bpow (-
fexp ex)) = 1%
Z.
Proof.
Generic facts about any format
Theorem generic_format_discrete :
forall x m,
let e :=
canonic_exp x in
(
F2R (
Float beta m e) <
x <
F2R (
Float beta (
m + 1)
e))%
R ->
~
generic_format x.
Proof.
Theorem generic_format_canonic :
forall f,
canonic f ->
generic_format (
F2R f).
Proof.
Theorem generic_format_ge_bpow :
forall emin,
(
forall e, (
emin <=
fexp e)%
Z ) ->
forall x,
(0 <
x)%
R ->
generic_format x ->
(
bpow emin <=
x)%
R.
Proof.
Theorem abs_lt_bpow_prec:
forall prec,
(
forall e, (
e -
prec <=
fexp e)%
Z) ->
forall x,
(
Rabs x <
bpow (
prec +
canonic_exp x))%
R.
intros prec Hp x.
case (
Req_dec x 0);
intros Hxz.
rewrite Hxz,
Rabs_R0.
apply bpow_gt_0.
unfold canonic_exp.
destruct (
ln_beta beta x)
as (
ex,
Ex) ;
simpl.
specialize (
Ex Hxz).
apply Rlt_le_trans with (1 :=
proj2 Ex).
apply bpow_le.
specialize (
Hp ex).
omega.
Qed.
Theorem generic_format_bpow_inv' :
forall e,
generic_format (bpow e) ->
(fexp (e + 1) <= e)%Z.
Proof.
Theorem generic_format_bpow_inv :
forall e,
generic_format (bpow e) ->
(fexp e <= e)%Z.
Proof.
intros e He.
apply generic_format_bpow_inv' in He.
assert (H := valid_exp_large' (e + 1) e).
omega.
Qed.
Section Fcore_generic_round_pos.
Rounding functions: R -> Z
Variable rnd : R -> Z.
Class Valid_rnd := {
Zrnd_le : forall x y, (x <= y)%R -> (rnd x <= rnd y)%Z ;
Zrnd_Z2R : forall n, rnd (Z2R n) = n
}.
Context { valid_rnd : Valid_rnd }.
Theorem Zrnd_DN_or_UP :
forall x, rnd x = Zfloor x \/ rnd x = Zceil x.
Proof.
Theorem Zrnd_ZR_or_AW :
forall x, rnd x = Ztrunc x \/ rnd x = Zaway x.
Proof.
the most useful one: R -> F
Definition round x :=
F2R (Float beta (rnd (scaled_mantissa x)) (canonic_exp x)).
Theorem round_bounded_large_pos :
forall x ex,
(fexp ex < ex)%Z ->
(bpow (ex - 1) <= x < bpow ex)%R ->
(bpow (ex - 1) <= round x <= bpow ex)%R.
Proof.
Theorem round_bounded_small_pos :
forall x ex,
(ex <= fexp ex)%Z ->
(bpow (ex - 1) <= x < bpow ex)%R ->
round x = R0 \/ round x = bpow (fexp ex).
Proof.
Theorem round_le_pos :
forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R.
Proof.
Theorem round_generic :
forall x,
generic_format x ->
round x = x.
Proof.
Theorem round_0 :
round 0 = R0.
Proof.
Theorem exp_small_round_0_pos :
forall x ex,
(bpow (ex - 1) <= x < bpow ex)%R ->
round x =R0 -> (ex <= fexp ex)%Z .
Proof.
Theorem generic_format_round_pos :
forall x,
(0 < x)%R ->
generic_format (round x).
Proof.
End Fcore_generic_round_pos.
Theorem round_ext :
forall rnd1 rnd2,
( forall x, rnd1 x = rnd2 x ) ->
forall x,
round rnd1 x = round rnd2 x.
Proof.
intros rnd1 rnd2 Hext x.
unfold round.
now rewrite Hext.
Qed.
Section Zround_opp.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Definition Zrnd_opp x := Zopp (rnd (-x)).
Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.
Proof with
Theorem round_opp :
forall x,
round rnd (- x) = Ropp (round Zrnd_opp x).
Proof.
End Zround_opp.
IEEE-754 roundings: up, down and to zero
Global Instance valid_rnd_DN : Valid_rnd Zfloor.
Proof.
Global Instance valid_rnd_UP : Valid_rnd Zceil.
Proof.
Global Instance valid_rnd_ZR : Valid_rnd Ztrunc.
Proof.
Global Instance valid_rnd_AW : Valid_rnd Zaway.
Proof.
Section monotone.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem round_DN_or_UP :
forall x,
round rnd x = round Zfloor x \/ round rnd x = round Zceil x.
Proof.
Theorem round_ZR_or_AW :
forall x,
round rnd x = round Ztrunc x \/ round rnd x = round Zaway x.
Proof.
Theorem round_le :
forall x y, (x <= y)%R -> (round rnd x <= round rnd y)%R.
Proof with
Theorem round_ge_generic :
forall x y, generic_format x -> (x <= y)%R -> (x <= round rnd y)%R.
Proof.
Theorem round_le_generic :
forall x y, generic_format y -> (x <= y)%R -> (round rnd x <= y)%R.
Proof.
End monotone.
Theorem round_abs_abs :
forall P : R -> R -> Prop,
( forall rnd (Hr : Valid_rnd rnd) x, (0 <= x)%R -> P x (round rnd x) ) ->
forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).
Proof with
Theorem round_bounded_large :
forall 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.
Proof with
Theorem exp_small_round_0 :
forall rnd {Hr : Valid_rnd rnd} x ex,
(bpow (ex - 1) <= Rabs x < bpow ex)%R ->
round rnd x =R0 -> (ex <= fexp ex)%Z .
Proof.
Section monotone_abs.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem abs_round_ge_generic :
forall x y, generic_format x -> (x <= Rabs y)%R -> (x <= Rabs (round rnd y))%R.
Proof with
Theorem abs_round_le_generic :
forall x y, generic_format y -> (Rabs x <= y)%R -> (Rabs (round rnd x) <= y)%R.
Proof with
End monotone_abs.
Theorem round_DN_opp :
forall x,
round Zfloor (-x) = (- round Zceil x)%R.
Proof.
Theorem round_UP_opp :
forall x,
round Zceil (-x) = (- round Zfloor x)%R.
Proof.
Theorem round_ZR_opp :
forall x,
round Ztrunc (- x) = Ropp (round Ztrunc x).
Proof.
Theorem round_ZR_abs :
forall x,
round Ztrunc (Rabs x) = Rabs (round Ztrunc x).
Proof with
Theorem round_AW_opp :
forall x,
round Zaway (- x) = Ropp (round Zaway x).
Proof.
Theorem round_AW_abs :
forall x,
round Zaway (Rabs x) = Rabs (round Zaway x).
Proof with
Theorem round_ZR_pos :
forall x,
(0 <= x)%R ->
round Ztrunc x = round Zfloor x.
Proof.
Theorem round_ZR_neg :
forall x,
(x <= 0)%R ->
round Ztrunc x = round Zceil x.
Proof.
Theorem round_AW_pos :
forall x,
(0 <= x)%R ->
round Zaway x = round Zceil x.
Proof.
Theorem round_AW_neg :
forall x,
(x <= 0)%R ->
round Zaway x = round Zfloor x.
Proof.
Theorem generic_format_round :
forall rnd { Hr : Valid_rnd rnd } x,
generic_format (round rnd x).
Proof with
Theorem round_DN_pt :
forall x,
Rnd_DN_pt generic_format x (round Zfloor x).
Proof with
Theorem generic_format_satisfies_any :
satisfies_any generic_format.
Proof.
Theorem round_UP_pt :
forall x,
Rnd_UP_pt generic_format x (round Zceil x).
Proof.
Theorem round_ZR_pt :
forall x,
Rnd_ZR_pt generic_format x (round Ztrunc x).
Proof.
Theorem round_DN_small_pos :
forall x ex,
(bpow (ex - 1) <= x < bpow ex)%R ->
(ex <= fexp ex)%Z ->
round Zfloor x = R0.
Proof.
Theorem round_DN_UP_lt :
forall x, ~ generic_format x ->
(round Zfloor x < x < round Zceil x)%R.
Proof with
Theorem round_UP_small_pos :
forall x ex,
(bpow (ex - 1) <= x < bpow ex)%R ->
(ex <= fexp ex)%Z ->
round Zceil x = (bpow (fexp ex)).
Proof.
Theorem generic_format_EM :
forall x,
generic_format x \/ ~generic_format x.
Proof with
Section round_large.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem round_large_pos_ge_pow :
forall x e,
(0 < round rnd x)%R ->
(bpow e <= x)%R ->
(bpow e <= round rnd x)%R.
Proof.
End round_large.
Theorem ln_beta_round_ZR :
forall x,
(round Ztrunc x <> 0)%R ->
(ln_beta beta (round Ztrunc x) = ln_beta beta x :> Z).
Proof with
Theorem ln_beta_round :
forall 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))).
Proof with
Theorem ln_beta_DN :
forall x,
(0 < round Zfloor x)%R ->
(ln_beta beta (round Zfloor x) = ln_beta beta x :> Z).
Proof.
Theorem canonic_exp_DN :
forall x,
(0 < round Zfloor x)%R ->
canonic_exp (round Zfloor x) = canonic_exp x.
Proof.
Theorem scaled_mantissa_DN :
forall x,
(0 < round Zfloor x)%R ->
scaled_mantissa (round Zfloor x) = Z2R (Zfloor (scaled_mantissa x)).
Proof.
Theorem generic_N_pt_DN_or_UP :
forall x f,
Rnd_N_pt generic_format x f ->
f = round Zfloor x \/ f = round Zceil x.
Proof.
Section not_FTZ.
Class Exp_not_FTZ :=
exp_not_FTZ : forall e, (fexp (fexp e + 1) <= fexp e)%Z.
Context { exp_not_FTZ_ : Exp_not_FTZ }.
Theorem subnormal_exponent :
forall e x,
(e <= fexp e)%Z ->
generic_format x ->
x = F2R (Float beta (Ztrunc (x * bpow (- fexp e))) (fexp e)).
Proof.
End not_FTZ.
Section monotone_exp.
Class Monotone_exp :=
monotone_exp : forall ex ey, (ex <= ey)%Z -> (fexp ex <= fexp ey)%Z.
Context { monotone_exp_ : Monotone_exp }.
Global Instance monotone_exp_not_FTZ : Exp_not_FTZ.
Proof.
Lemma canonic_exp_le_bpow :
forall (x : R) (e : Z),
x <> R0 ->
(Rabs x < bpow e)%R ->
(canonic_exp x <= fexp e)%Z.
Proof.
Lemma canonic_exp_ge_bpow :
forall (x : R) (e : Z),
(bpow (e - 1) <= Rabs x)%R ->
(fexp e <= canonic_exp x)%Z.
Proof.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem ln_beta_round_ge :
forall x,
round rnd x <> R0 ->
(ln_beta beta x <= ln_beta beta (round rnd x))%Z.
Proof with
Theorem canonic_exp_round_ge :
forall x,
round rnd x <> R0 ->
(canonic_exp x <= canonic_exp (round rnd x))%Z.
Proof with
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 - Z2R (Zfloor x)) (/2) with
| Lt => Zfloor x
| Eq => if choice (Zfloor x) then Zceil x else Zfloor x
| Gt => Zceil x
end.
Theorem Znearest_DN_or_UP :
forall x,
Znearest x = Zfloor x \/ Znearest x = Zceil x.
Proof.
Theorem Znearest_ge_floor :
forall x,
(Zfloor x <= Znearest x)%Z.
Proof.
Theorem Znearest_le_ceil :
forall x,
(Znearest x <= Zceil x)%Z.
Proof.
Global Instance valid_rnd_N : Valid_rnd Znearest.
Proof.
Theorem Rcompare_floor_ceil_mid :
forall x,
Z2R (Zfloor x) <> x ->
Rcompare (x - Z2R (Zfloor x)) (/ 2) = Rcompare (x - Z2R (Zfloor x)) (Z2R (Zceil x) - x).
Proof.
Theorem Rcompare_ceil_floor_mid :
forall x,
Z2R (Zfloor x) <> x ->
Rcompare (Z2R (Zceil x) - x) (/ 2) = Rcompare (Z2R (Zceil x) - x) (x - Z2R (Zfloor x)).
Proof.
Theorem Znearest_N_strict :
forall x,
(x - Z2R (Zfloor x) <> /2)%R ->
(Rabs (x - Z2R (Znearest x)) < /2)%R.
Proof.
Theorem Znearest_N :
forall x,
(Rabs (x - Z2R (Znearest x)) <= /2)%R.
Proof.
Theorem Znearest_imp :
forall x n,
(Rabs (x - Z2R n) < /2)%R ->
Znearest x = n.
Proof.
Theorem round_N_pt :
forall x,
Rnd_N_pt generic_format x (round Znearest x).
Proof.
Theorem round_N_middle :
forall 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.
Proof.
Lemma round_N_really_small_pos :
forall x,
forall ex,
(Fcore_Raux.bpow beta (ex - 1) <= x < Fcore_Raux.bpow beta ex)%R ->
(ex < fexp ex)%Z ->
(round Znearest x = 0)%R.
Proof.
End Znearest.
Section rndNA.
Global Instance valid_rnd_NA : Valid_rnd (Znearest (Zle_bool 0)) := valid_rnd_N _.
Theorem round_NA_pt :
forall x,
Rnd_NA_pt generic_format x (round (Znearest (Zle_bool 0)) x).
Proof.
End rndNA.
Section rndN_opp.
Theorem Znearest_opp :
forall choice x,
Znearest choice (- x) = (- Znearest (fun t => negb (choice (- (t + 1))%Z)) x)%Z.
Proof with
Theorem round_N_opp :
forall choice,
forall x,
round (Znearest choice) (-x) = (- round (Znearest (fun t => negb (choice (- (t + 1))%Z))) x)%R.
Proof.
End rndN_opp.
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_ln_beta :
forall x,
( x <> R0 -> (fexp2 (ln_beta beta x) <= fexp1 (ln_beta beta x))%Z ) ->
generic_format fexp1 x ->
generic_format fexp2 x.
Proof.
Theorem generic_inclusion_lt_ge :
forall e1 e2,
( forall e, (e1 < e <= e2)%Z -> (fexp2 e <= fexp1 e)%Z ) ->
forall x,
(bpow e1 <= Rabs x < bpow e2)%R ->
generic_format fexp1 x ->
generic_format fexp2 x.
Proof.
Theorem generic_inclusion :
forall e,
(fexp2 e <= fexp1 e)%Z ->
forall x,
(bpow (e - 1) <= Rabs x <= bpow e)%R ->
generic_format fexp1 x ->
generic_format fexp2 x.
Proof with
Theorem generic_inclusion_le_ge :
forall e1 e2,
(e1 < e2)%Z ->
( forall e, (e1 < e <= e2)%Z -> (fexp2 e <= fexp1 e)%Z ) ->
forall x,
(bpow e1 <= Rabs x <= bpow e2)%R ->
generic_format fexp1 x ->
generic_format fexp2 x.
Proof.
Theorem generic_inclusion_le :
forall e2,
( forall e, (e <= e2)%Z -> (fexp2 e <= fexp1 e)%Z ) ->
forall x,
(Rabs x <= bpow e2)%R ->
generic_format fexp1 x ->
generic_format fexp2 x.
Proof.
Theorem generic_inclusion_ge :
forall e1,
( forall e, (e1 < e)%Z -> (fexp2 e <= fexp1 e)%Z ) ->
forall x,
(bpow e1 <= Rabs x)%R ->
generic_format fexp1 x ->
generic_format fexp2 x.
Proof.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Theorem generic_round_generic :
forall x,
generic_format fexp1 x ->
generic_format fexp1 (round fexp2 rnd x).
Proof with
End Inclusion.
End Generic.
Notation ZnearestA := (Znearest (Zle_bool 0)).
Section rndNA_opp.
Lemma round_NA_opp :
forall beta : radix,
forall (fexp : Z -> Z),
forall x,
(round beta fexp ZnearestA (- x) = - round beta fexp ZnearestA x)%R.
Proof.
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).