From 3cb1d2813f8ff6ac9cbad44974fee00b8a0236c9 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Thu, 10 Feb 2022 11:01:38 +0100
Subject: Cgt / Clt

---
 kvx/FPDivision64.v | 27 ++++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 572df195..34dc108b 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1321,7 +1321,7 @@ Definition step2_div_long' a b :=
 
 Definition step2_div_long a b :=
   let q := step2_div_long' a b in
-  Val.select (Val.cmpl_bool Cgt (Val.subl (Val.mull q b) a) (Vlong Int64.zero))
+  Val.select (Val.cmpl_bool Clt (Val.subl a (Val.mull q b)) (Vlong Int64.zero))
              (Val.addl q (Vlong Int64.mone)) q Tlong.
 
 Lemma function_ite :
@@ -1377,6 +1377,19 @@ Proof.
     apply int64_eqm_signed_repr.
   - apply Int64.eqm_refl.
 Qed.
+
+Lemma signed_repr_sub2:
+  forall x y,
+    Int64.repr (x - Int64.signed (Int64.repr y)) =
+    Int64.repr (x - y).
+Proof.
+  intros.
+  apply Int64.eqm_samerepr.
+  apply Int64.eqm_sub.
+  - apply Int64.eqm_refl.
+  - apply Int64.eqm_sym.
+    apply int64_eqm_signed_repr.
+Qed.
                                                                         
 Lemma step2_div_long_smalla_correct :
     forall a b
@@ -1454,7 +1467,7 @@ Proof.
 
   rewrite Int64.sub_signed.
   fold a'.
-  rewrite signed_repr_sub.
+  rewrite signed_repr_sub2.
 
   assert ((Rabs (IZR a' / IZR b' - q') < / 2)%R) as HALF.
   { replace (IZR a' / IZR b' - q')%R with
@@ -1473,8 +1486,8 @@ Proof.
   destruct (Z_lt_dec a' (b' * q'')) as [LT | GE].
   { replace (b' * q'' >? a')%Z with true in QUOTIENT by lia.
     replace q'' with (1 + (a' / b'))%Z by lia.
-    replace ((1 + a' / b') * b' - a')%Z
-      with (-(a' - a' / b' * b')+b')%Z by ring.
+    replace (a' - (1 + a' / b') * b')%Z
+      with ((a' - a' / b' * b')-b')%Z by ring.
     rewrite <- MOD.
     rewrite Int64.signed_repr; cycle 1.
     { change Int64.min_signed with (-9223372036854775808)%Z in *.
@@ -1731,7 +1744,7 @@ Proof.
 
   rewrite Int64.sub_signed.
   fold a'.
-  rewrite signed_repr_sub.
+  rewrite signed_repr_sub2.
 
   assert ((Rabs (IZR a' / IZR b' - q') < / 2)%R) as HALF.
   { replace (IZR a' / IZR b' - q')%R with
@@ -1750,8 +1763,8 @@ Proof.
   destruct (Z_lt_dec a' (b' * q'')) as [LT | GE].
   { replace (b' * q'' >? a')%Z with true in QUOTIENT by lia.
     replace q'' with (1 + (a' / b'))%Z by lia.
-    replace ((1 + a' / b') * b' - a')%Z
-      with (-(a' - a' / b' * b')+b')%Z by ring.
+    replace (a' - (1 + a' / b') * b')%Z
+      with ((a' - a' / b' * b')-b')%Z by ring.
     rewrite <- MOD.
     rewrite Int64.signed_repr; cycle 1.
     { change Int64.min_signed with (-9223372036854775808)%Z in *.
-- 
cgit