From aa8f655361670b593f805b1e57a1089b8f924938 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Tue, 11 Jan 2022 15:31:02 +0100
Subject: progress in proofs

---
 kvx/FPDivision64.v | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 76e21e54..d16417fb 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -582,7 +582,9 @@ Proof.
   econstructor. split. reflexivity.
   rewrite C3R.
   rewrite C2R.
-  rewrite C3S.
+  rewrite C3S; cycle 1.
+  { apply is_finite_not_is_nan.
+    assumption. }
   rewrite C2S.
   rewrite C1S.
   rewrite C3F.
@@ -597,4 +599,12 @@ Proof.
    ((rd (rd (IZR a') * f_r) - (rd (IZR a') * f_r))
     + ((rd (IZR a') - IZR a') * f_r)
     + (IZR a') * (f_r - 1 / IZR b'))%R by (field ; lra).
+
+  assert (Rabs (rd (IZR a') - IZR a') <= 1024)%R as DELTA1.
+  { unfold rd. gappa. }
+  set (delta1 := (rd (IZR a') - IZR a')%R) in *.
+  
+  assert (Rabs (rd (rd (IZR a') * f_r) - rd (IZR a') * f_r) <= 1024)%R as DELTA2.
+  { unfold rd. gappa. }
+  set (delta2 := (rd (rd (IZR a') * f_r) - rd (IZR a') * f_r)%R) in *.
 Admitted.
-- 
cgit