Commit c429778c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added some Rabs versions of rewriting lemmas.

parent 7b301bb5
......@@ -1378,6 +1378,18 @@ apply ln_beta_unique.
now rewrite Rabs_Ropp.
Qed.
Theorem ln_beta_abs :
forall x,
projT1 (ln_beta (Rabs x)) = projT1 (ln_beta x).
Proof.
intros x.
set (m := projT1 (ln_beta x)).
unfold Rabs.
case Rcase_abs ; intros _.
now rewrite ln_beta_opp.
apply refl_equal.
Qed.
Theorem ln_beta_monotone_abs :
forall x y,
(x <> 0)%R -> (Rabs x <= Rabs y)%R ->
......
......@@ -82,6 +82,15 @@ now rewrite 2!Zfloor_Z2R.
Qed.
*)
Theorem canonic_exponent_abs :
forall x,
canonic_exponent (Rabs x) = canonic_exponent x.
Proof.
intros x.
unfold canonic_exponent.
now rewrite ln_beta_abs.
Qed.
Theorem generic_format_bpow :
forall e, (fexp (e + 1) <= e)%Z ->
generic_format (bpow e).
......
......@@ -18,6 +18,22 @@ Definition ulp x := bpow (canonic_exponent beta fexp x).
Definition F := generic_format beta fexp.
Theorem ulp_opp :
forall x, ulp (- x) = ulp x.
Proof.
intros x.
unfold ulp.
now rewrite canonic_exponent_opp.
Qed.
Theorem ulp_abs :
forall x, ulp (Rabs x) = ulp x.
Proof.
intros x.
unfold ulp.
now rewrite canonic_exponent_abs.
Qed.
Theorem ulp_DN_UP :
forall x, ~ F x ->
rounding beta fexp ZrndUP x = (rounding beta fexp ZrndDN x + ulp x)%R.
......
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