Commit 6043f519 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix theorem naming.

parent cdda3e7b
......@@ -13,7 +13,7 @@ Context {Hprec : Prec_gt_0 prec}.
Notation fexp := (FLT_exp emin prec).
Definition Bmin := bpow radix2 (emin + prec).
Definition Bmin := bpow radix2 (emin + prec - 1).
Definition hombnd (m M u v : R) (b B : float radix2) :=
(0 <= F2R b)%R /\ (1 <= F2R B)%R /\
......
......@@ -257,48 +257,33 @@ apply Rle_lt_trans with (2:=Hx).
now apply He.
Qed.
Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R ->
(ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R.
Theorem ulp_FLT_le :
forall x, (bpow (emin + prec - 1) <= Rabs x)%R ->
(ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R.
Proof.
intros x Hx.
assert (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; try assumption.
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.
destruct (ln_beta beta x) as (e,He).
apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.
rewrite <- bpow_plus.
right; apply f_equal.
apply trans_eq with (e-prec)%Z;[idtac|ring].
simpl; apply Z.max_l.
assert (emin+prec <= e)%Z; try omega.
apply le_bpow with beta.
apply Rle_trans with (1:=Hx).
left; now apply He.
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring.
apply Z.max_l.
assert (emin+prec-1 < e)%Z; try omega.
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=Hx).
now apply He.
Qed.
Theorem ulp_FLT_le2: forall x, (bpow (emin+prec-1) <= Rabs x)%R ->
(ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R.
Proof.
intros x Hx.
case (Rle_or_lt (bpow (emin+prec)) (Rabs x)); intros Hx2.
now apply ulp_FLT_le.
rewrite ulp_FLT_small; try exact Hx2.
apply Rle_trans with (bpow (emin+prec-1)*bpow (1-prec))%R.
rewrite <- bpow_plus.
right; apply f_equal; ring.
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hx.
now apply He.
Qed.
Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
Theorem ulp_FLT_gt :
forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
Proof.
intros x; case (Req_dec x 0); intros Hx.
rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0.
......
......@@ -35,13 +35,13 @@ Variable fexp : Z -> Z.
(** Definition and basic properties about the minimal exponent, when it exists *)
Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z.
Proof.
intros.
destruct (Z_le_dec x y).
now left.
now right.
Qed.
(** [negligible_exp] is either none (as in FLX) or Some n such that n <= fexp n. *)
Definition negligible_exp: option Z :=
match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with
......
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