From 5b5c74d4ea6af4555b2abf804afe77559a337702 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 7 Dec 2010 16:49:32 +0000
Subject: [PATCH] Added F2R_eq_compat.

---
 src/Core/Fcore_float_prop.v  | 9 +++++++++
 src/Core/Fcore_generic_fmt.v | 8 ++++----
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/Core/Fcore_float_prop.v b/src/Core/Fcore_float_prop.v
index 077413b..a78ef6b 100644
--- a/src/Core/Fcore_float_prop.v
+++ b/src/Core/Fcore_float_prop.v
@@ -87,6 +87,15 @@ apply bpow_gt_0.
 now apply Z2R_lt.
 Qed.
 
+Theorem F2R_eq_compat :
+  forall e m1 m2 : Z,
+  (m1 = m2)%Z ->
+  (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.
+Proof.
+intros e m1 m2 H.
+now apply (f_equal (fun m => F2R (Float beta m e))).
+Qed.
+
 Theorem F2R_eq_reg :
   forall e m1 m2 : Z,
   F2R (Float beta m1 e) = F2R (Float beta m2 e) ->
diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v
index 8dfa2d7..3da4ec3 100644
--- a/src/Core/Fcore_generic_fmt.v
+++ b/src/Core/Fcore_generic_fmt.v
@@ -341,7 +341,7 @@ intros (m, e) Hf.
 unfold canonic in Hf. simpl in Hf.
 unfold generic_format, scaled_mantissa.
 rewrite <- Hf.
-apply (f_equal (fun m => F2R (Float beta m e))).
+apply F2R_eq_compat.
 unfold F2R. simpl.
 rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
 now rewrite Ztrunc_Z2R.
@@ -710,7 +710,7 @@ Proof.
 intros x.
 unfold round.
 rewrite opp_F2R, canonic_exponent_opp, scaled_mantissa_opp.
-apply (f_equal (fun m => F2R (Float beta m _))).
+apply F2R_eq_compat.
 apply sym_eq.
 exact (Zopp_involutive _).
 Qed.
@@ -942,7 +942,7 @@ split ; intros Hx.
 (* *)
 replace (round rndZR x) with (round rndDN x).
 apply round_DN_pt.
-apply (f_equal (fun v => F2R (Float beta v _))).
+apply F2R_eq_compat.
 apply sym_eq.
 apply Ztrunc_floor.
 rewrite <- (Rmult_0_l (bpow (- canonic_exponent x))).
@@ -951,7 +951,7 @@ apply bpow_ge_0.
 (* *)
 replace (round rndZR x) with (round rndUP x).
 apply round_UP_pt.
-apply (f_equal (fun v => F2R (Float beta v _))).
+apply F2R_eq_compat.
 apply sym_eq.
 apply Ztrunc_ceil.
 rewrite <- (Rmult_0_l (bpow (- canonic_exponent x))).
-- 
GitLab