From c429778c9abcec502c5f597893453bda5266e5a9 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 26 Aug 2010 11:44:22 +0000
Subject: [PATCH] Added some Rabs versions of rewriting lemmas.

---
 src/Core/Fcore_Raux.v        | 12 ++++++++++++
 src/Core/Fcore_generic_fmt.v |  9 +++++++++
 src/Core/Fcore_ulp.v         | 16 ++++++++++++++++
 3 files changed, 37 insertions(+)

diff --git a/src/Core/Fcore_Raux.v b/src/Core/Fcore_Raux.v
index 66f69ac..ebfa425 100644
--- a/src/Core/Fcore_Raux.v
+++ b/src/Core/Fcore_Raux.v
@@ -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 ->
diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v
index 9cd62b8..c9e6d6e 100644
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -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).
diff --git a/src/Core/Fcore_ulp.v b/src/Core/Fcore_ulp.v
index d93e58a..0820535 100644
--- a/src/Core/Fcore_ulp.v
+++ b/src/Core/Fcore_ulp.v
@@ -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.
-- 
GitLab