Commit 3745486e authored by BOLDO Sylvie's avatar BOLDO Sylvie

eq_0_round_0_negligible_exp and friends (FLX)

parent 9e494218
......@@ -205,15 +205,46 @@ now apply FLXN_format_generic.
now apply generic_format_FLXN.
Qed.
Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
Lemma negligible_exp_FLX :
negligible_exp FLX_exp = None.
Proof.
unfold ulp; rewrite Req_bool_true; trivial.
case (negligible_exp_spec FLX_exp).
intros _; reflexivity.
intros n H2; contradict H2.
unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.
Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
Proof.
unfold ulp; rewrite Req_bool_true; trivial.
rewrite negligible_exp_FLX; easy.
Qed.
Theorem eq_0_round_0_FLX :
forall rnd {Vr: Valid_rnd rnd} x,
round beta FLX_exp rnd x = 0%R -> x = 0%R.
Proof.
intros rnd Hr x.
apply eq_0_round_0_negligible_exp; try assumption.
apply FLX_exp_valid.
apply negligible_exp_FLX.
Qed.
Theorem gt_0_round_gt_0_FLX :
forall rnd {Vr: Valid_rnd rnd} x,
(0 < x)%R -> (0 < round beta FLX_exp rnd x)%R.
Proof with auto with typeclass_instances.
intros rnd Hr x Hx.
assert (K: (0 <= round beta FLX_exp rnd x)%R).
rewrite <- (round_0 beta FLX_exp rnd).
apply round_le... now apply Rlt_le.
destruct K; try easy.
absurd (x = 0)%R.
now apply Rgt_not_eq.
apply eq_0_round_0_FLX with rnd...
Qed.
Theorem ulp_FLX_le :
forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R.
Proof.
......
......@@ -352,6 +352,30 @@ apply ulp_le_pos; trivial.
apply Rabs_pos.
Qed.
(** Properties when there is no minimal exponent *)
Theorem eq_0_round_0_negligible_exp :
negligible_exp = None -> forall rnd {Vr: Valid_rnd rnd} x,
round beta fexp rnd x = 0%R -> x = 0%R.
Proof.
intros H rnd Vr x Hx.
case (Req_dec x 0); try easy; intros Hx2.
absurd (Rabs (round beta fexp rnd x) = 0%R).
2: rewrite Hx, Rabs_R0; easy.
apply Rgt_not_eq.
apply Rlt_le_trans with (bpow (mag beta x - 1)).
apply bpow_gt_0.
apply abs_round_ge_generic; try assumption.
apply generic_format_bpow.
case negligible_exp_spec'; [intros (K1,K2)|idtac].
ring_simplify (mag beta x-1+1)%Z.
specialize (K2 (mag beta x)); now auto with zarith.
intros (n,(Hn1,Hn2)).
rewrite Hn1 in H; discriminate.
now apply bpow_mag_le.
Qed.
(** Definition and properties of pred and succ *)
Definition pred_pos x :=
......
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