Commit aa2b17eb authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added rounding for FIX formats.

parent 50542867
Require Import Fcore.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.
Section Fcalc_round_FIX.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable emin : Z.
Notation format := (generic_format beta (FIX_exp emin)).
Definition round_FIX t :=
let '(m, e, l) := t in
let k := (emin - e)%Z in
if Zlt_bool 0 k then
let p := Zpower (radix_val beta) k in
(Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l)
else t.
Theorem round_FIX_correct :
forall x m e l,
inbetween_float beta m e x l ->
(e <= emin)%Z \/ l = loc_Exact ->
let '(m', e', l') := round_FIX (m, e, l) in
inbetween_float beta m' e' x l' /\
(e' = canonic_exponent beta (FIX_exp emin) x \/ format x).
Proof.
intros x m e l H1 H2.
unfold round_FIX.
set (k := (emin - e)%Z).
set (p := Zpower (radix_val beta) k).
unfold canonic_exponent, FIX_exp.
generalize (Zlt_cases 0 k).
case (Zlt_bool 0 k) ; intros Hk.
(* shift *)
split.
now apply inbetween_float_new_location.
clear H2.
left.
unfold k.
ring.
(* no shift *)
split.
exact H1.
unfold k in Hk.
destruct H2 as [H2|H2].
left.
omega.
right.
rewrite H2 in H1.
inversion_clear H1.
rewrite H.
apply generic_format_canonic_exponent.
unfold canonic_exponent.
omega.
Qed.
End Fcalc_round_FIX.
......@@ -15,6 +15,7 @@ FILES = \
Calc/Fcalc_digits.v \
Calc/Fcalc_div.v \
Calc/Fcalc_ops.v \
Calc/Fcalc_round_FIX.v \
Calc/Fcalc_sqrt.v \
Prop/Fprop_nearest.v
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment