From d40d74c2a9d1fdd1438926527d16a6e0f3527022 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 2 Sep 2011 15:52:52 +0000
Subject: [PATCH] Add theorem generic_format_abs_inv.

---
 src/Core/Fcore_generic_fmt.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v
index 1e19797..4dc11fa 100644
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -222,6 +222,20 @@ rewrite <- abs_F2R.
 now apply f_equal.
 Qed.
 
+Theorem generic_format_abs_inv :
+  forall x, generic_format (Rabs x) -> generic_format x.
+Proof.
+intros x.
+unfold generic_format, Rabs.
+case Rcase_abs ; intros _.
+rewrite scaled_mantissa_opp, canonic_exponent_opp, Ztrunc_opp.
+intros H.
+rewrite <- (Ropp_involutive x) at 1.
+rewrite H, <- opp_F2R.
+apply Ropp_involutive.
+easy.
+Qed.
+
 Theorem canonic_exponent_fexp :
   forall x ex,
   (bpow (ex - 1) <= Rabs x < bpow ex)%R ->
-- 
GitLab