Commit 551cf217 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Removed exponent from Zrounding functions, as it was unneeded (if not harmful) for FTZ.

parent 97b0f3dc
......@@ -547,11 +547,11 @@ Qed.
Theorem inbetween_float_rounding :
forall rnd choice,
( forall x m e l, inbetween_int m x l -> Zrnd rnd x e = choice m e l ) ->
( forall x m l, inbetween_int m x l -> Zrnd rnd x = choice m l ) ->
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float m e x l ->
rounding beta fexp rnd x = F2R (Float beta (choice m e l) e).
rounding beta fexp rnd x = F2R (Float beta (choice m l) e).
Proof.
intros rnd choice Hc x m l e Hl.
unfold rounding, F2R. simpl.
......@@ -568,8 +568,8 @@ Theorem inbetween_float_DN :
inbetween_float m e x l ->
rounding beta fexp ZrndDN x = F2R (Float beta m e).
Proof.
apply inbetween_float_rounding with (choice := fun m e l => m).
intros x m e l Hl.
apply inbetween_float_rounding with (choice := fun m l => m).
intros x m l Hl.
refine (Zfloor_imp m _ _).
apply inbetween_bounds with (2 := Hl).
apply Z2R_lt.
......@@ -590,8 +590,8 @@ Theorem inbetween_float_UP :
inbetween_float m e x l ->
rounding beta fexp ZrndUP x = F2R (Float beta (cond_incr (round_UP l) m) e).
Proof.
apply inbetween_float_rounding with (choice := fun m e l => cond_incr (round_UP l) m).
intros x m e l Hl.
apply inbetween_float_rounding with (choice := fun m l => cond_incr (round_UP l) m).
intros x m l Hl.
assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)).
case l ; try (now left) ; now right ; split.
destruct Hl' as [Hl'|(Hl1, Hl2)].
......@@ -623,14 +623,14 @@ Theorem inbetween_float_NE :
inbetween_float m e x l ->
rounding beta fexp ZrndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e).
Proof.
apply inbetween_float_rounding with (choice := fun m e l => cond_incr (round_NE (Zeven m) l) m).
intros x m e l Hl.
apply inbetween_float_rounding with (choice := fun m l => cond_incr (round_NE (Zeven m) l) m).
intros x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
now rewrite Zrnd_Z2R.
(* not Exact *)
unfold Zrnd, ZrndNE, ZrndN, Znearest, mkZrounding2.
unfold Zrnd, ZrndNE, ZrndN, Znearest.
assert (Hm: Zfloor x = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
......
......@@ -219,13 +219,13 @@ Section FTZ_rounding.
Hypothesis rnd : Zrounding.
Definition Zrnd_FTZ x e :=
if Rle_bool R1 (Rabs x) then Zrnd rnd x e else Z0.
Definition Zrnd_FTZ x :=
if Rle_bool R1 (Rabs x) then Zrnd rnd x else Z0.
Theorem Z_FTZ_Z2R :
forall n e, Zrnd_FTZ (Z2R n) e = n.
forall n, Zrnd_FTZ (Z2R n) = n.
Proof.
intros n e.
intros n.
unfold Zrnd_FTZ.
rewrite Zrnd_Z2R.
case Rle_bool_spec.
......@@ -238,17 +238,17 @@ now case n ; trivial ; simpl ; intros [p|p|].
Qed.
Theorem Z_FTZ_monotone :
forall x y e, (x <= y)%R ->
(Zrnd_FTZ x e <= Zrnd_FTZ y e)%Z.
forall x y, (x <= y)%R ->
(Zrnd_FTZ x <= Zrnd_FTZ y)%Z.
Proof.
intros x y e Hxy.
intros x y Hxy.
unfold Zrnd_FTZ.
case Rle_bool_spec ; intros Hx ;
case Rle_bool_spec ; intros Hy.
4: easy.
(* 1 <= |x| *)
now apply Zrnd_monotone.
rewrite <- (Zrnd_Z2R rnd 0 e).
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone.
apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le.
destruct (Rabs_le_r_inv _ _ Hx) as [Hx1|Hx1].
......@@ -258,7 +258,7 @@ apply Rle_lt_trans with (2 := Hy).
apply Rle_trans with (1 := Hxy).
apply RRle_abs.
(* |x| < 1 *)
rewrite <- (Zrnd_Z2R rnd 0 e).
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone.
apply Rle_trans with (Z2R 1).
now apply Z2R_le.
......
......@@ -303,9 +303,9 @@ Qed.
Section Fcore_generic_rounding_pos.
Record Zrounding := mkZrounding {
Zrnd : R -> Z -> Z ;
Zrnd_monotone : forall x y e, (x <= y)%R -> (Zrnd x e <= Zrnd y e)%Z ;
Zrnd_Z2R : forall n e, Zrnd (Z2R n) e = n
Zrnd : R -> Z ;
Zrnd_monotone : forall x y, (x <= y)%R -> (Zrnd x <= Zrnd y)%Z ;
Zrnd_Z2R : forall n, Zrnd (Z2R n) = n
}.
Variable rnd : Zrounding.
......@@ -314,18 +314,18 @@ Let Zrnd_monotone := Zrnd_monotone rnd.
Let Zrnd_Z2R := Zrnd_Z2R rnd.
Theorem Zrnd_DN_or_UP :
forall x e, Zrnd x e = Zfloor x \/ Zrnd x e = Zceil x.
forall x, Zrnd x = Zfloor x \/ Zrnd x = Zceil x.
Proof.
intros x e.
destruct (Zle_or_lt (Zrnd x e) (Zfloor x)) as [Hx|Hx].
intros x.
destruct (Zle_or_lt (Zrnd x) (Zfloor x)) as [Hx|Hx].
left.
apply Zle_antisym with (1 := Hx).
rewrite <- (Zrnd_Z2R (Zfloor x) e).
rewrite <- (Zrnd_Z2R (Zfloor x)).
apply Zrnd_monotone.
apply Zfloor_lb.
right.
apply Zle_antisym.
rewrite <- (Zrnd_Z2R (Zceil x) e).
rewrite <- (Zrnd_Z2R (Zceil x)).
apply Zrnd_monotone.
apply Zceil_ub.
rewrite Zceil_floor_neq.
......@@ -337,7 +337,7 @@ apply Zlt_irrefl with (1 := Hx).
Qed.
Definition rounding x :=
F2R (Float beta (Zrnd (scaled_mantissa x) (canonic_exponent x)) (canonic_exponent x)).
F2R (Float beta (Zrnd (scaled_mantissa x)) (canonic_exponent x)).
Theorem rounding_monotone_pos :
forall x y, (0 < x)%R -> (x <= y)%R -> (rounding x <= rounding y)%R.
......@@ -374,14 +374,14 @@ apply Zrnd_monotone.
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hxy.
apply Rle_trans with (F2R (Float beta (Zrnd (bpow (ey - 1) * bpow (- fexp ey)) (fexp ey)) (fexp ey))).
apply Rle_trans with (F2R (Float beta (Zrnd (bpow (ey - 1) * bpow (- fexp ey))) (fexp ey))).
rewrite <- bpow_add.
rewrite <- (Z2R_Zpower beta (ey - 1 + -fexp ey)). 2: omega.
rewrite Zrnd_Z2R.
destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1].
apply Rle_trans with (F2R (Float beta 1 (fexp ex))).
apply F2R_le_compat.
rewrite <- (Zrnd_Z2R 1 (fexp ex)).
rewrite <- (Zrnd_Z2R 1).
apply Zrnd_monotone.
apply Rlt_le.
exact (proj2 (mantissa_small_pos _ _ Hex Hx1)).
......@@ -390,7 +390,7 @@ rewrite Z2R_Zpower. 2: omega.
rewrite <- bpow_add, Rmult_1_l.
apply -> bpow_le.
omega.
apply Rle_trans with (F2R (Float beta (Zrnd (bpow ex * bpow (- fexp ex)) (fexp ex)) (fexp ex))).
apply Rle_trans with (F2R (Float beta (Zrnd (bpow ex * bpow (- fexp ex))) (fexp ex))).
apply F2R_le_compat.
apply Zrnd_monotone.
apply Rmult_le_compat_r.
......@@ -450,7 +450,7 @@ intros x ex He Hx.
unfold rounding, scaled_mantissa.
rewrite (canonic_exponent_fexp_pos _ _ Hx).
unfold F2R. simpl.
destruct (Zrnd_DN_or_UP (x * bpow (- fexp ex)) (fexp ex)) as [Hr|Hr] ; rewrite Hr.
destruct (Zrnd_DN_or_UP (x * bpow (- fexp ex))) as [Hr|Hr] ; rewrite Hr.
(* DN *)
split.
replace (ex - 1)%Z with (ex - 1 + - fexp ex + fexp ex)%Z by ring.
......@@ -509,7 +509,7 @@ intros x ex He Hx.
unfold rounding, scaled_mantissa.
rewrite (canonic_exponent_fexp_pos _ _ Hx).
unfold F2R. simpl.
destruct (Zrnd_DN_or_UP (x * bpow (-fexp ex)) (fexp ex)) as [Hr|Hr] ; rewrite Hr.
destruct (Zrnd_DN_or_UP (x * bpow (-fexp ex))) as [Hr|Hr] ; rewrite Hr.
(* DN *)
left.
apply Rmult_eq_0_compat_r.
......@@ -563,7 +563,7 @@ End Fcore_generic_rounding_pos.
Theorem rounding_ext :
forall rnd1 rnd2,
( forall x e, Zrnd rnd1 x e = Zrnd rnd2 x e ) ->
( forall x, Zrnd rnd1 x = Zrnd rnd2 x ) ->
forall x,
rounding rnd1 x = rounding rnd2 x.
Proof.
......@@ -576,12 +576,12 @@ Section Zrounding_opp.
Variable rnd : Zrounding.
Definition Zrnd_opp x e := Zopp (Zrnd rnd (-x) e).
Definition Zrnd_opp x := Zopp (Zrnd rnd (-x)).
Lemma Zrnd_opp_le :
forall x y e, (x <= y)%R -> (Zrnd_opp x e <= Zrnd_opp y e)%Z.
forall x y, (x <= y)%R -> (Zrnd_opp x <= Zrnd_opp y)%Z.
Proof.
intros x y e Hxy.
intros x y Hxy.
unfold Zrnd_opp.
apply Zopp_le_cancel.
rewrite 2!Zopp_involutive.
......@@ -590,9 +590,9 @@ now apply Ropp_le_contravar.
Qed.
Lemma Zrnd_opp_Z2R :
forall n e, Zrnd_opp (Z2R n) e = n.
forall n, Zrnd_opp (Z2R n) = n.
Proof.
intros n e.
intros n.
unfold Zrnd_opp.
rewrite <- opp_Z2R, Zrnd_Z2R.
apply Zopp_involutive.
......@@ -614,13 +614,9 @@ Qed.
End Zrounding_opp.
Definition mkZrounding2 rnd (mono : forall x y, (x <= y)%R -> (rnd x <= rnd y)%Z) (z2r : forall n, rnd (Z2R n) = n) :=
mkZrounding (fun x _ => rnd x) (fun x y _ => mono x y) (fun n _ => z2r n).
Definition ZrndDN := mkZrounding2 Zfloor Zfloor_le Zfloor_Z2R.
Definition ZrndUP := mkZrounding2 Zceil Zceil_le Zceil_Z2R.
Definition ZrndTZ := mkZrounding2 Ztrunc Ztrunc_le Ztrunc_Z2R.
Definition ZrndDN := mkZrounding Zfloor Zfloor_le Zfloor_Z2R.
Definition ZrndUP := mkZrounding Zceil Zceil_le Zceil_Z2R.
Definition ZrndTZ := mkZrounding Ztrunc Ztrunc_le Ztrunc_Z2R.
Theorem rounding_DN_or_UP :
forall rnd x,
......@@ -629,7 +625,7 @@ Proof.
intros rnd x.
unfold rounding.
unfold Zrnd at 2 4. simpl.
destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x) (canonic_exponent x)) as [Hx|Hx].
destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x)) as [Hx|Hx].
left. now rewrite Hx.
right. now rewrite Hx.
Qed.
......@@ -656,7 +652,7 @@ now apply Ropp_le_contravar.
(* . 0 <= y *)
apply Rle_trans with R0.
apply F2R_le_0_compat. simpl.
rewrite <- (Zrnd_Z2R rnd 0 (canonic_exponent x)).
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone.
simpl.
rewrite <- (Rmult_0_l (bpow (- fexp (projT1 (ln_beta beta x))))).
......@@ -664,7 +660,7 @@ apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply Rlt_le.
apply F2R_ge_0_compat. simpl.
rewrite <- (Zrnd_Z2R rnd 0 (canonic_exponent y)).
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone.
apply Rmult_le_pos.
exact Hy.
......@@ -674,7 +670,7 @@ rewrite Hx.
rewrite rounding_0.
apply F2R_ge_0_compat.
simpl.
rewrite <- (Zrnd_Z2R rnd 0 (canonic_exponent y)).
rewrite <- (Zrnd_Z2R rnd 0).
apply Zrnd_monotone.
apply Rmult_le_pos.
now rewrite <- Hx.
......@@ -697,7 +693,6 @@ rewrite <- (rounding_generic rnd y Hy).
now apply rounding_monotone.
Qed.
Theorem rounding_abs_abs :
forall P : R -> R -> Prop,
( forall rnd x, P x (rounding rnd x) ) ->
......@@ -723,8 +718,6 @@ apply rounding_monotone.
now apply Rlt_le.
Qed.
Theorem rounding_monotone_abs_l :
forall rnd x y, generic_format x -> (x <= Rabs y)%R -> (x <= Rabs (rounding rnd y))%R.
Proof.
......@@ -1170,8 +1163,7 @@ apply Rmult_lt_compat_r with (2 := H1).
now apply (Z2R_lt 0 2).
Qed.
Definition ZrndN := mkZrounding2 Znearest Znearest_monotone Znearest_Z2R.
Definition ZrndN := mkZrounding Znearest Znearest_monotone Znearest_Z2R.
Theorem Znearest_N_strict :
forall x,
......@@ -1349,9 +1341,6 @@ rewrite opp_Z2R.
apply Rplus_comm.
Qed.
Theorem rounding_N_opp :
forall choice,
forall x,
......
......@@ -77,10 +77,10 @@ apply Hex.
apply Hey.
(* *)
assert (Hr: ((F2R (Float beta (- (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) *
Ztrunc (scaled_mantissa beta (FLX_exp prec) y)) + Zrnd rnd (scaled_mantissa beta (FLX_exp prec) (x * y)) (canonic_exponent beta (FLX_exp prec) (x * y)) *
Ztrunc (scaled_mantissa beta (FLX_exp prec) y)) + Zrnd rnd (scaled_mantissa beta (FLX_exp prec) (x * y)) *
radix_val beta ^ (cexp (x * y)%R - (cexp x + cexp y))) (cexp x + cexp y))) = f - x * y)%R).
rewrite Hx at 7.
rewrite Hy at 7.
rewrite Hx at 6.
rewrite Hy at 6.
rewrite <- mult_F2R.
simpl.
unfold f, rounding, Rminus.
......
......@@ -30,7 +30,7 @@ rewrite Z2R_Zpower. 2: omega.
rewrite <- bpow_add.
apply (f_equal (fun v => Z2R m * bpow v)%R).
ring.
exists ((Zrnd rnd (Z2R m * bpow (e - e')) e') * Zpower (radix_val beta) (e' - e))%Z.
exists ((Zrnd rnd (Z2R m * bpow (e - e'))) * Zpower (radix_val beta) (e' - e))%Z.
unfold F2R. simpl.
rewrite mult_Z2R.
rewrite Z2R_Zpower. 2: omega.
......
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