From 7ff41e564bcc2e01d33b26419d3039d2f393440a Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Wed, 12 Jan 2022 11:41:27 +0100
Subject: progress in proofs

---
 kvx/FPDivision64.v | 53 ++++++++---------------------------------------------
 1 file changed, 8 insertions(+), 45 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 425e11da..b1ba6938 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -407,54 +407,17 @@ Theorem rough_approx_inv_longu_correct1 :
     (Int64.unsigned b = 1%Z) ->
     exists f,
     (rough_approx_inv_longu (Vlong b)) = Vfloat f /\
-        is_finite _ _ f = true /\
         (B2R _ _ f) = 1%R /\
+        is_finite _ _ f = true /\
         Bsign _ _ f = false.
 Proof.
-  intros b ONE.
-  cbn.
-  unfold Float.of_single, ExtFloat32.inv, Float32.div, ExtFloat32.one, Float32.of_longu, Float32.of_int.
-  set (re := (@eq_refl Datatypes.comparison Lt)).
-  rewrite ONE.
-  change (Int.signed (Int.repr 1)) with 1%Z.
-  
-  econstructor.
-  split. reflexivity.
-  split. reflexivity.
-  split. 2: reflexivity.
-  destruct (BofZ_exact 24 128 re re 1%Z) as (C1R & C1F & C1S). lia.
-
-  pose proof (Bdiv_correct 24 128 re re Float32.binop_nan mode_NE 
-                           (BofZ 24 128 re re 1) (BofZ 24 128 re re 1)) as C2.
-  rewrite C1R in C2.
-  rewrite C1F in C2.
-  rewrite C1S in C2.
-  rewrite Rlt_bool_true in C2; cycle 1.
-  { clear C2.
-    apply Rabs_relax with (b := bpow radix2 0%Z).
-    { apply bpow_lt. lia. }
-    cbn.
-    gappa.
-  }
-  assert (1 <> 0)%R as OBVIOUS by lra.
-  destruct (C2 OBVIOUS) as (C2R & C2F & C2S).
-  clear C2.
-
-  pose proof (Bconv_correct 24 128 53 1024 re re Float.of_single_nan mode_NE
-       (Bdiv 24 128 re re Float32.binop_nan mode_NE 
-          (BofZ 24 128 re re 1) (BofZ 24 128 re re 1)) C2F) as C3.
-  rewrite Rlt_bool_true in C3; cycle 1.
-  { clear C3.
-    rewrite C2R.
-    apply Rabs_relax with (b := bpow radix2 0%Z).
-    { apply bpow_lt. lia. }
-    cbn.
-    gappa.
-  }
-  destruct C3 as (C3R & C3F & C3S).
-  rewrite C3R.
-  rewrite C2R.
-  cbn.
+  intros b EQ1.
+  assert (0 < Int64.unsigned b)%Z as b_RANGE by lia.
+  destruct (rough_approx_inv_longu_correct b b_RANGE) as (f & C1E & C1R & C1F & C1S).
+  rewrite EQ1 in C1R.
+  exists f.
+  repeat split; try assumption.
+  rewrite C1R.
   gappa.
 Qed.
 
-- 
cgit