Commit a9aaa6ed authored by Guillaume Melquiond's avatar Guillaume Melquiond

Rename canonic_exp into cexp.

parent bfecafc1
Version 3.0.0:
- stripped prefix from all the file names, renamed some files
- renamed canonic_exp into cexp, canonic into canonical
Version 2.5.2:
- ensured compatibility from Coq 8.4 to 8.6
......
......@@ -43,7 +43,7 @@ Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format radix2 (FLT_exp emin prec)).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation ulp_flt :=(ulp radix2 (FLT_exp emin prec)).
Notation cexp := (canonic_exp radix2 (FLT_exp emin prec)).
Notation cexp := (cexp radix2 (FLT_exp emin prec)).
Notation pred_flt := (pred radix2 (FLT_exp emin prec)).
Lemma FLT_format_double: forall u, format u -> format (2*u).
......@@ -112,7 +112,7 @@ apply lt_bpow with radix2.
destruct ln_beta as (e,He); simpl.
apply Rle_lt_trans with (1:=Hz).
now apply He.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
replace ((ln_beta radix2 (z/2))-prec)%Z with ((ln_beta radix2 z -1) -prec)%Z.
rewrite Z.max_l; try omega.
rewrite Z.max_l; try omega.
......@@ -157,8 +157,8 @@ intros u H.
rewrite ulp_neq_0.
2: apply Rgt_not_eq, Rlt_le_trans with (2:=H), bpow_gt_0.
case (Rle_or_lt (bpow (emin+prec-1)) u); intros Hu.
unfold ulp; rewrite canonic_exp_FLT_FLX.
unfold canonic_exp, FLX_exp.
unfold ulp; rewrite cexp_FLT_FLX.
unfold cexp, FLX_exp.
destruct (ln_beta radix2 u) as (e,He); simpl.
apply Rle_trans with (bpow (e-1)).
apply bpow_le.
......@@ -172,7 +172,7 @@ apply Rle_ge, Rle_trans with (2:=Hu), bpow_ge_0.
rewrite Rabs_right.
assumption.
apply Rle_ge, Rle_trans with (2:=Hu), bpow_ge_0.
unfold ulp; rewrite canonic_exp_FLT_FIX.
unfold ulp; rewrite cexp_FLT_FIX.
apply H.
apply Rgt_not_eq, Rlt_gt.
apply Rlt_le_trans with (2:=H).
......@@ -202,9 +202,9 @@ rewrite <- bpow_plus.
apply bpow_le.
case (Rle_or_lt (bpow (emin+prec-1)) (Rabs u)); intros Hu.
(* *)
rewrite canonic_exp_FLT_FLX.
rewrite canonic_exp_FLT_FLX; trivial.
unfold canonic_exp, FLX_exp.
rewrite cexp_FLT_FLX.
rewrite cexp_FLT_FLX; trivial.
unfold cexp, FLX_exp.
replace 2 with (bpow 1) by reflexivity.
rewrite Rmult_comm, ln_beta_mult_bpow.
omega.
......@@ -223,9 +223,9 @@ apply Rle_ge; now auto with real.
case (Req_dec u 0); intros K.
rewrite K, Rmult_0_r.
omega.
rewrite canonic_exp_FLT_FIX.
rewrite canonic_exp_FLT_FIX; trivial.
unfold FIX_exp, canonic_exp; omega.
rewrite cexp_FLT_FIX.
rewrite cexp_FLT_FIX; trivial.
unfold FIX_exp, cexp; omega.
apply Rlt_le_trans with (1:=Hu).
apply bpow_le; omega.
apply Rmult_integral_contrapositive_currified; trivial.
......@@ -310,7 +310,7 @@ right; split; try assumption.
rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
apply trans_eq with (bpow (ln_beta radix2 f- prec -1)).
apply f_equal.
unfold canonic_exp.
unfold cexp.
apply trans_eq with (FLT_exp emin prec (ln_beta radix2 f -1)%Z).
apply f_equal.
unfold FLT_exp.
......@@ -346,7 +346,7 @@ replace (/2) with (bpow (-1)) by reflexivity.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
rewrite <- bpow_plus.
apply f_equal.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
rewrite Z.max_l;[ring|omega].
(**)
left.
......@@ -371,7 +371,7 @@ rewrite Z.max_l in H4.
replace (ln_beta radix2 f - 1 + 1 - prec)%Z with (ln_beta radix2 f - prec)%Z in H4 by ring.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
rewrite ulp_neq_0 at 2; try now apply Rgt_not_eq.
unfold canonic_exp.
unfold cexp.
apply f_equal; apply f_equal.
replace (ulp_flt f) with (bpow (ln_beta radix2 f -prec)).
apply ln_beta_unique.
......@@ -393,7 +393,7 @@ left; apply Rle_lt_trans with (2:=H0).
apply bpow_le.
unfold Prec_gt_0 in prec_gt_0_;omega.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
rewrite Z.max_l.
reflexivity.
omega.
......@@ -803,7 +803,7 @@ rewrite ulp_neq_0; trivial.
replace (/4) with (bpow (-2)) by reflexivity.
rewrite <- bpow_plus.
apply bpow_le.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
assert (emin+prec+prec+1 -1 < ln_beta radix2 (x/2))%Z.
destruct (ln_beta radix2 (x/2)) as (e,He).
simpl.
......@@ -847,7 +847,7 @@ Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format radix2 (FLT_exp emin prec)).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation ulp_flt :=(ulp radix2 (FLT_exp emin prec)).
Notation cexp := (canonic_exp radix2 (FLT_exp emin prec)).
Notation cexp := (cexp radix2 (FLT_exp emin prec)).
Definition average3 (x y : R) :=round_flt(x+round_flt(round_flt(y-x)/2)).
......@@ -1023,7 +1023,7 @@ apply FLT_format_bpow...
omega.
now left.
replace (bpow emin /2) with (bpow (emin-1)).
unfold round, scaled_mantissa, canonic_exp, FLT_exp.
unfold round, scaled_mantissa, cexp, FLT_exp.
rewrite ln_beta_bpow.
replace (emin - 1 + 1 - prec)%Z with (emin-prec)%Z by ring.
rewrite Z.max_r.
......@@ -1181,7 +1181,7 @@ rewrite <- bpow_plus.
ring_simplify (-emin+emin)%Z.
simpl; ring.
ring.
apply sym_eq, canonic_exp_FLT_FIX.
apply sym_eq, cexp_FLT_FIX.
apply Rgt_not_eq, Rlt_gt.
unfold Rdiv; apply Rmult_lt_0_compat; try assumption.
auto with real.
......@@ -1356,8 +1356,8 @@ omega.
assert (G1:(round_flt (bpow emin/2) = 0)).
replace (bpow emin /2) with (bpow (emin-1)).
unfold round, scaled_mantissa.
rewrite canonic_exp_FLT_FIX.
unfold canonic_exp, FIX_exp; simpl.
rewrite cexp_FLT_FIX.
unfold cexp, FIX_exp; simpl.
rewrite <- bpow_plus.
replace (bpow (emin - 1 + - emin)) with (/2).
replace (ZnearestE (/ 2)) with 0%Z.
......@@ -1417,7 +1417,7 @@ rewrite ulp_neq_0.
2: apply Rgt_not_eq, bpow_gt_0.
2: apply Rinv_neq_0_compat, Rgt_not_eq; fourier.
apply bpow_le.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
apply Z.le_max_r.
unfold b, average3.
rewrite J1,J3,J2,J4,T1,T2; unfold F2R; simpl.
......@@ -1455,15 +1455,13 @@ rewrite ulp_neq_0.
2: apply Rgt_not_eq, bpow_gt_0.
2: apply Rinv_neq_0_compat, Rgt_not_eq; fourier.
apply bpow_le.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
apply Z.le_max_r.
apply Rle_ge, Rmult_le_pos.
apply bpow_ge_0.
now auto with real.
Qed.
Lemma average3_correct_aux2: forall u v, format u -> format v -> u <= v ->
(0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) ->
Rabs (average3 u v -((u+v)/2)) <= 3/2 * ulp_flt ((u+v)/2).
......@@ -1524,7 +1522,7 @@ rewrite 2!ulp_neq_0; trivial.
replace 2 with (bpow 1) by reflexivity.
rewrite <- bpow_plus.
apply bpow_le.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
rewrite Rmult_comm, ln_beta_mult_bpow; trivial.
rewrite <- Z.add_max_distr_l.
replace (ln_beta radix2 b + 1 - prec)%Z with (1 + (ln_beta radix2 b - prec))%Z by ring.
......@@ -1751,7 +1749,7 @@ Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format radix2 (FLT_exp emin prec)).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation ulp_flt :=(ulp radix2 (FLT_exp emin prec)).
Notation cexp := (canonic_exp radix2 (FLT_exp emin prec)).
Notation cexp := (cexp radix2 (FLT_exp emin prec)).
Definition average (x y : R) :=
let samesign := match (Rle_bool 0 x), (Rle_bool 0 y) with
......
This diff is collapsed.
......@@ -38,7 +38,7 @@ Theorem inbetween_float_round :
forall rnd choice,
( forall x m l, inbetween_int m x l -> rnd x = choice m l ) ->
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp rnd x = F2R (Float beta (choice m l) e).
Proof.
......@@ -58,7 +58,7 @@ Theorem inbetween_float_round_sign :
( forall x m l, inbetween_int m (Rabs x) l ->
rnd x = cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l) ) ->
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e (Rabs x) l ->
round beta fexp rnd x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l)) e).
Proof.
......@@ -102,7 +102,7 @@ Qed.
Theorem inbetween_float_DN :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp Zfloor x = F2R (Float beta m e).
Proof.
......@@ -154,7 +154,7 @@ Qed.
Theorem inbetween_float_DN_sign :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e (Rabs x) l ->
round beta fexp Zfloor x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_sign_DN (Rlt_bool x 0) l) m)) e).
Proof.
......@@ -195,7 +195,7 @@ Qed.
Theorem inbetween_float_UP :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp Zceil x = F2R (Float beta (cond_incr (round_UP l) m) e).
Proof.
......@@ -245,7 +245,7 @@ Qed.
Theorem inbetween_float_UP_sign :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e (Rabs x) l ->
round beta fexp Zceil x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_sign_UP (Rlt_bool x 0) l) m)) e).
Proof.
......@@ -296,7 +296,7 @@ Qed.
Theorem inbetween_float_ZR :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp Ztrunc x = F2R (Float beta (cond_incr (round_ZR (Zlt_bool m 0) l) m) e).
Proof.
......@@ -335,7 +335,7 @@ Qed.
Theorem inbetween_float_ZR_sign :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e (Rabs x) l ->
round beta fexp Ztrunc x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) m) e).
Proof.
......@@ -455,7 +455,7 @@ Qed.
Theorem inbetween_float_NE :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp ZnearestE x = F2R (Float beta (cond_incr (round_N (negb (Zeven m)) l) m) e).
Proof.
......@@ -480,7 +480,7 @@ Qed.
Theorem inbetween_float_NE_sign :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e (Rabs x) l ->
round beta fexp ZnearestE x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (negb (Zeven m)) l) m)) e).
Proof.
......@@ -501,7 +501,7 @@ Qed.
Theorem inbetween_float_NA :
forall x m l,
let e := canonic_exp beta fexp x in
let e := cexp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp ZnearestA x = F2R (Float beta (cond_incr (round_N (Zle_bool 0 m) l) m) e).
Proof.
......@@ -594,7 +594,7 @@ case Zlt_bool_spec ; intros Hk.
unfold truncate_aux.
apply generic_format_F2R.
intros Hd.
unfold canonic_exp.
unfold cexp.
rewrite ln_beta_F2R_Zdigits with (1 := Hd).
rewrite Zdigits_div_Zpower with (1 := Hm).
replace (Zdigits beta m - k + (e + k))%Z with (Zdigits beta m + e)%Z by ring.
......@@ -614,7 +614,7 @@ now apply Zgt_lt.
(* *)
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
apply generic_format_F2R.
unfold canonic_exp.
unfold cexp.
rewrite ln_beta_F2R_Zdigits.
2: now apply Zgt_not_eq.
unfold k in Hk. clear -Hk.
......@@ -630,20 +630,20 @@ Theorem truncate_correct_format :
generic_format beta fexp x ->
(e <= fexp (Zdigits beta m + e))%Z ->
let '(m', e', l') := truncate (m, e, loc_Exact) in
x = F2R (Float beta m' e') /\ e' = canonic_exp beta fexp x.
x = F2R (Float beta m' e') /\ e' = cexp beta fexp x.
Proof.
intros m e Hm x Fx He.
assert (Hc: canonic_exp beta fexp x = fexp (Zdigits beta m + e)).
unfold canonic_exp, x.
assert (Hc: cexp beta fexp x = fexp (Zdigits beta m + e)).
unfold cexp, x.
now rewrite ln_beta_F2R_Zdigits.
unfold truncate.
rewrite <- Hc.
set (k := (canonic_exp beta fexp x - e)%Z).
set (k := (cexp beta fexp x - e)%Z).
case Zlt_bool_spec ; intros Hk.
(* *)
unfold truncate_aux.
rewrite Fx at 1.
assert (H: (e + k)%Z = canonic_exp beta fexp x).
assert (H: (e + k)%Z = cexp beta fexp x).
unfold k. ring.
refine (conj _ H).
rewrite <- H.
......@@ -677,7 +677,7 @@ Theorem truncate_correct_partial :
inbetween_float beta m e x l ->
(e <= fexp (Zdigits beta m + e))%Z ->
let '(m', e', l') := truncate (m, e, l) in
inbetween_float beta m' e' x l' /\ e' = canonic_exp beta fexp x.
inbetween_float beta m' e' x l' /\ e' = cexp beta fexp x.
Proof.
intros x m e l Hx H1 H2.
unfold truncate.
......@@ -693,9 +693,9 @@ apply F2R_lt_reg with beta e.
rewrite F2R_0.
apply Rlt_trans with (1 := Hx).
apply Hx'.
assert (He: (e + k = canonic_exp beta fexp x)%Z).
assert (He: (e + k = cexp beta fexp x)%Z).
(* . *)
unfold canonic_exp.
unfold cexp.
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
(* .. 0 < m *)
rewrite ln_beta_F2R_bounds with (1 := Hm') (2 := Hx').
......@@ -747,7 +747,7 @@ Theorem truncate_correct :
(e <= fexp (Zdigits beta m + e))%Z \/ l = loc_Exact ->
let '(m', e', l') := truncate (m, e, l) in
inbetween_float beta m' e' x l' /\
(e' = canonic_exp beta fexp x \/ (l' = loc_Exact /\ format x)).
(e' = cexp beta fexp x \/ (l' = loc_Exact /\ format x)).
Proof.
intros x m e l [Hx|Hx] H1 H2.
(* 0 < x *)
......@@ -780,7 +780,7 @@ inversion_clear H1.
rewrite H.
apply generic_format_F2R.
intros Zm.
unfold canonic_exp.
unfold cexp.
rewrite ln_beta_F2R_Zdigits with (1 := Zm).
now apply Zlt_le_weak.
(* x = 0 *)
......@@ -835,7 +835,7 @@ Hypothesis inbetween_int_valid :
Theorem round_any_correct :
forall x m e l,
inbetween_float beta m e x l ->
(e = canonic_exp beta fexp x \/ (l = loc_Exact /\ format x)) ->
(e = cexp beta fexp x \/ (l = loc_Exact /\ format x)) ->
round beta fexp rnd x = F2R (Float beta (choice m l) e).
Proof with auto with typeclass_instances.
intros x m e l Hin [He|(Hl,Hf)].
......@@ -885,7 +885,7 @@ Hypothesis inbetween_int_valid :
Theorem round_sign_any_correct :
forall x m e l,
inbetween_float beta m e (Rabs x) l ->
(e = canonic_exp beta fexp x \/ (l = loc_Exact /\ format x)) ->
(e = cexp beta fexp x \/ (l = loc_Exact /\ format x)) ->
round beta fexp rnd x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l)) e).
Proof with auto with typeclass_instances.
intros x m e l Hin [He|(Hl,Hf)].
......@@ -959,7 +959,7 @@ apply round_sign_any_correct.
exact H1.
destruct H2 as [H2|(H2,H3)].
left.
now rewrite <- canonic_exp_abs.
now rewrite <- cexp_abs.
right.
split.
exact H2.
......@@ -1054,13 +1054,13 @@ Theorem truncate_FIX_correct :
(e <= emin)%Z \/ l = loc_Exact ->
let '(m', e', l') := truncate_FIX (m, e, l) in
inbetween_float beta m' e' x l' /\
(e' = canonic_exp beta (FIX_exp emin) x \/ (l' = loc_Exact /\ generic_format beta (FIX_exp emin) x)).
(e' = cexp beta (FIX_exp emin) x \/ (l' = loc_Exact /\ generic_format beta (FIX_exp emin) x)).
Proof.
intros x m e l H1 H2.
unfold truncate_FIX.
set (k := (emin - e)%Z).
set (p := Zpower beta k).
unfold canonic_exp, FIX_exp.
unfold cexp, FIX_exp.
generalize (Zlt_cases 0 k).
case (Zlt_bool 0 k) ; intros Hk.
(* shift *)
......@@ -1084,7 +1084,7 @@ rewrite H2 in H1.
inversion_clear H1.
rewrite H.
apply generic_format_F2R.
unfold canonic_exp.
unfold cexp.
omega.
Qed.
......
......@@ -53,7 +53,7 @@ Theorem generic_format_FIX :
Proof.
intros x ((xm, xe), (Hx1, Hx2)).
rewrite Hx1.
now apply generic_format_canonic.
now apply generic_format_canonical.
Qed.
Theorem FIX_format_generic :
......
......@@ -57,7 +57,7 @@ simpl in H2, H3.
rewrite H1.
apply generic_format_F2R.
intros Zmx.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
rewrite ln_beta_F2R with (1 := Zmx).
apply Zmax_lub with (2 := H3).
apply Zplus_le_reg_r with (prec - ex)%Z.
......@@ -70,7 +70,7 @@ Theorem FLT_format_generic :
Proof.
intros x.
unfold generic_format.
set (ex := canonic_exp beta FLT_exp x).
set (ex := cexp beta FLT_exp x).
set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)).
intros Hx.
rewrite Hx.
......@@ -86,7 +86,7 @@ rewrite <- Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0, Rabs_R0.
apply bpow_gt_0.
unfold canonic_exp in ex.
unfold cexp in ex.
destruct (ln_beta beta x) as (ex', He).
simpl in ex.
specialize (He Hx0).
......@@ -121,16 +121,16 @@ apply FLT_format_generic.
apply generic_format_FLT.
Qed.
Theorem canonic_exp_FLT_FLX :
Theorem cexp_FLT_FLX :
forall x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x.
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x.
Proof.
intros x Hx.
assert (Hx0: x <> 0%R).
intros H1; rewrite H1, Rabs_R0 in Hx.
contradict Hx; apply Rlt_not_le, bpow_gt_0.
unfold canonic_exp.
unfold cexp.
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
unfold FLX_exp. simpl.
......@@ -153,7 +153,7 @@ destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
apply generic_format_0.
unfold generic_format, scaled_mantissa.
now rewrite canonic_exp_FLT_FLX.
now rewrite cexp_FLT_FLX.
Qed.
Theorem generic_format_FLX_FLT :
......@@ -166,26 +166,27 @@ unfold generic_format in Hx; rewrite Hx.
apply generic_format_F2R.
intros _.
rewrite <- Hx.
unfold canonic_exp, FLX_exp, FLT_exp.
unfold cexp, FLX_exp, FLT_exp.
apply Zle_max_l.
Qed.
Theorem round_FLT_FLX : forall rnd x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
Proof.
intros rnd x Hx.
unfold round, scaled_mantissa.
rewrite canonic_exp_FLT_FLX ; trivial.
rewrite cexp_FLT_FLX ; trivial.
Qed.
(** Links between FLT and FIX (underflow) *)
Theorem canonic_exp_FLT_FIX :
Theorem cexp_FLT_FIX :
forall x, x <> R0 ->
(Rabs x < bpow (emin + prec))%R ->
canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x.
cexp beta FLT_exp x = cexp beta (FIX_exp emin) x.
Proof.
intros x Hx0 Hx.
unfold canonic_exp.
unfold cexp.
apply Zmax_right.
unfold FIX_exp.
destruct (ln_beta beta x) as (ex, Hex).
......@@ -241,7 +242,7 @@ intros n H2; rewrite <-V.
apply f_equal, fexp_negligible_exp_eq...
omega.
(* x <> 0 *)
apply f_equal; unfold canonic_exp, FLT_exp.
apply f_equal; unfold cexp, FLT_exp.
apply Z.max_r.
assert (ln_beta beta x-1 < emin+prec)%Z;[idtac|omega].
destruct (ln_beta beta x) as (e,He); simpl.
......@@ -259,7 +260,7 @@ assert (Zx : (x <> 0)%R).
intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt.
rewrite Z, Rabs_R0; apply bpow_gt_0.
rewrite ulp_neq_0 with (1 := Zx).
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
destruct (ln_beta beta x) as (e,He).
apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.
rewrite <- bpow_plus.
......@@ -282,7 +283,7 @@ intros x; case (Req_dec x 0); intros Hx.
rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0.
rewrite Rabs_R0; apply bpow_gt_0.
rewrite ulp_neq_0; try exact Hx.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
apply Rlt_le_trans with (bpow (ln_beta beta x)*bpow (-prec))%R.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
......
......@@ -77,12 +77,12 @@ apply lt_Z2R.
rewrite Z2R_abs.
rewrite <- scaled_mantissa_generic with (1 := H).
rewrite <- scaled_mantissa_abs.
apply Rmult_lt_reg_r with (bpow (canonic_exp beta FLX_exp (Rabs x))).
apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp (Rabs x))).
apply bpow_gt_0.
rewrite scaled_mantissa_mult_bpow.
rewrite Z2R_Zpower, <- bpow_plus.
2: now apply Zlt_le_weak.
unfold canonic_exp, FLX_exp.
unfold cexp, FLX_exp.
ring_simplify (prec + (ln_beta beta (Rabs x) - prec))%Z.
rewrite ln_beta_abs.
destruct (Req_dec x 0) as [Hx|Hx].
......@@ -101,7 +101,7 @@ simpl in H2.
rewrite H1.
apply generic_format_F2R.
intros Zmx.
unfold canonic_exp, FLX_exp.
unfold cexp, FLX_exp.
rewrite ln_beta_F2R with (1 := Zmx).
apply Zplus_le_reg_r with (prec - ex)%Z.
ring_simplify.
......@@ -168,13 +168,13 @@ apply le_Z2R.
rewrite Z2R_Zpower.
2: now apply Zlt_0_le_0_pred.
rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx).
apply Rmult_le_reg_r with (bpow (canonic_exp beta FLX_exp x)).
apply Rmult_le_reg_r with (bpow (cexp beta FLX_exp x)).
apply bpow_gt_0.
rewrite <- bpow_plus.
rewrite <- scaled_mantissa_abs.
rewrite <- canonic_exp_abs.
rewrite <- cexp_abs.
rewrite scaled_mantissa_mult_bpow.
unfold canonic_exp, FLX_exp.
unfold cexp, FLX_exp.
rewrite ln_beta_abs.
ring_simplify (prec - 1 + (ln_beta beta x - prec))%Z.
destruct (ln_beta beta x) as (ex,Ex).
......@@ -184,13 +184,13 @@ apply lt_Z2R.
rewrite Z2R_Zpower.
2: now apply Zlt_le_weak.
rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx).
apply Rmult_lt_reg_r with (bpow (canonic_exp beta FLX_exp x)).
apply Rmult_lt_reg_r with (bpow (cexp beta FLX_exp x)).
apply bpow_gt_0.
rewrite <- bpow_plus.
rewrite <- scaled_mantissa_abs.
rewrite <- canonic_exp_abs.
rewrite <- cexp_abs.
rewrite scaled_mantissa_mult_bpow.
unfold canonic_exp, FLX_exp.
unfold cexp, FLX_exp.
rewrite ln_beta_abs.
ring_simplify (prec + (ln_beta beta x - prec))%Z.
destruct (ln_beta beta x) as (ex,Ex).
......@@ -215,13 +215,14 @@ intros n H2; contradict H2.
unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.
Theorem ulp_FLX_le: forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R.
Theorem ulp_FLX_le :
forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R.
Proof.
intros x; case (Req_dec x 0); intros Hx.
rewrite Hx, ulp_FLX_0, Rabs_R0.
right; ring.
rewrite ulp_neq_0; try exact Hx.
unfold canonic_exp, FLX_exp.
unfold cexp, FLX_exp.
replace (ln_beta beta x - prec)%Z with ((ln_beta beta x - 1) + (1-prec))%Z by ring.
rewrite bpow_plus.
apply Rmult_le_compat_r.
......@@ -229,14 +230,14 @@ apply bpow_ge_0.
now apply bpow_ln_beta_le.
Qed.
Theorem ulp_FLX_ge: forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R.
Theorem ulp_FLX_ge :
forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R.
Proof.
intros x; case (Req_dec x 0); intros Hx.
rewrite Hx, ulp_FLX_0, Rabs_R0.
right; ring.
rewrite ulp_neq_0; try exact Hx.
unfold canonic_exp, FLX_exp.
unfold cexp, FLX_exp.
unfold Zminus; rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
......
......@@ -112,7 +112,7 @@ split.
intros H.
now elim H.
apply Zle_refl.
unfold generic_format, scaled_mantissa, canonic_exp, FTZ_exp in Hx.
unfold generic_format, scaled_mantissa, cexp, FTZ_exp in Hx.
destruct (ln_beta beta x) as (ex, Hx4).
simpl in Hx.
specialize (Hx4 Hx3).
......@@ -263,7 +263,7 @@ Theorem round_FTZ_FLX :
round beta FTZ_exp Zrnd_FTZ x = round beta (FLX_exp prec) rnd x.
Proof.
intros x Hx.
unfold round, scaled_mantissa, canonic_exp.
unfold round, scaled_mantissa, cexp.
destruct (ln_beta beta x) as (ex, He). simpl.
assert (Hx0: x <> R0).
intros Hx0.
......@@ -307,7 +307,7 @@ intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
apply round_0...
unfold round, scaled_mantissa, canonic_exp.
unfold round, scaled_mantissa, cexp.
destruct (ln_beta beta x) as (ex, He). simpl.
specialize (He Hx0).
unfold Zrnd_FTZ.
......
This diff is collapsed.
......@@ -33,10 +33,10 @@ Variable fexp : Z -> Z.
Context { valid_exp : Valid_exp fexp }.
Notation format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Notation canonical := (canonical beta fexp).
Definition NE_prop (_ : R) f :=
exists g : float beta, f = F2R g /\ canonic g /\ Zeven (Fnum g) = true.
exists g : float beta, f = F2R g /\ canonical g /\ Zeven (Fnum g) = true.
Definition Rnd_NE_pt :=
Rnd_NG_pt format NE_prop.
......@@ -45,8 +45,8 @@ Definition DN_UP_parity_pos_prop :=
forall x xd xu,
(0 < x)%R ->
~ format x ->
canonic xd ->
canonic xu ->
canonical xd ->
canonical xu ->
F2R xd = round beta fexp Zfloor x ->
F2R xu = round beta fexp Zceil x ->
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
......@@ -54,8 +54,8 @@ Definition DN_UP_parity_pos_prop :=
Definition DN_UP_parity_prop :=
forall x xd xu,
~ format x ->
canonic xd ->
canonic xu ->
canonical xd ->
canonical xu ->
F2R xd = round beta fexp Zfloor x ->
F2R xu = round beta fexp Zceil x ->
Zeven (Fnum xu) = negb (Zeven (Fnum xd)).
......@@ -88,8 +88,8 @@ intros H.
apply Hfx.
rewrite <- Ropp_involutive.
now apply generic_format_opp.
now apply canonic_opp.
now apply canonic_opp.
now apply canonical_opp.
now apply canonical_opp.
rewrite round_DN_opp, F2R_Zopp.
now apply f_equal.
rewrite round_UP_opp, F2R_Zopp.
......@@ -118,7 +118,7 @@ change (F2R xd = R0).
rewrite Hxd.
apply round_DN_small_pos with (1 := Hex) (2 := Hxe).
assert (Hu3 : xu = Float beta (1 * Zpower beta (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))).
apply canonic_unicity with (1 := Hu).
apply canonical_unicity with (1 := Hu).
apply (f_equal fexp).
rewrite <- F2R_change_exp.
now rewrite F2R_bpow, ln_beta_bpow.
......@@ -167,7 +167,7 @@ rewrite Hxu.
apply round_bounded_large_pos...
(* - xu = bpow ex *)
assert (Hu3: xu = Float beta (1 * Zpower beta (ex - fexp (ex + 1))) (fexp (ex + 1))).
apply canonic_unicity with (1 := Hu).
apply canonical_unicity with (1 := Hu).
apply (f_equal fexp).
rewrite <- F2R_change_exp.
now rewrite F2R_bp