Fix ldshiftexp

* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly

Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>

4 files changed, 19 insertions, 27 deletions

diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index dc637e50a6..8ca64aac42 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -51,8 +51,8 @@ Axiom sqrt_spec : forall x, Prim2SF (sqrt x) = SF64sqrt (Prim2SF x).
 Axiom of_int63_spec : forall n, Prim2SF (of_int63 n) = binary_normalize prec emax (to_Z n) 0%Z false.
 Axiom normfr_mantissa_spec : forall f, to_Z (normfr_mantissa f) = Z.of_N (SFnormfr_mantissa prec (Prim2SF f)).
 
-Axiom frshiftexp_spec : forall f, let (m,e) := frshiftexp f in (Prim2SF m, ((to_Z e) - (to_Z shift))%Z) = SFfrexp prec emax (Prim2SF f).
-Axiom ldshiftexp_spec : forall f e, Prim2SF (ldshiftexp f e) = SFldexp prec emax (Prim2SF f) ((to_Z e) - (to_Z shift)).
+Axiom frshiftexp_spec : forall f, let (m,e) := frshiftexp f in (Prim2SF m, ((to_Z e) - shift)%Z) = SFfrexp prec emax (Prim2SF f).
+Axiom ldshiftexp_spec : forall f e, Prim2SF (ldshiftexp f e) = SFldexp prec emax (Prim2SF f) ((to_Z e) - shift).
 
 Axiom next_up_spec : forall x, Prim2SF (next_up x) = SF64succ (Prim2SF x).
 Axiom next_down_spec : forall x, Prim2SF (next_down x) = SF64pred (Prim2SF x).
diff --git a/theories/Floats/FloatLemmas.v b/theories/Floats/FloatLemmas.v
index 4e1f14610d..81cb7120e0 100644
--- a/theories/Floats/FloatLemmas.v
+++ b/theories/Floats/FloatLemmas.v
@@ -3,7 +3,7 @@ Require Import Psatz.
 
 (** * Support results involving frexp and ldexp *)
 
-Lemma shift_value : [|shift|]%int63 = (2*emax + prec)%Z.
+Lemma shift_value : shift = (2*emax + prec)%Z.
   reflexivity.
 Qed.
 
@@ -24,23 +24,15 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
   destruct (Prim2SF f); auto.
   unfold SFldexp.
   unfold binary_round.
-  assert (Hmod_elim :  forall e, ([| of_Z (Z.max (Z.min e (emax - emin)) (emin - emax - 1)) + shift |]%int63 - [|shift|]%int63 = Z.max (Z.min e (emax - emin)) (emin - emax - 1))%Z).
+  assert (Hmod_elim :  forall e, ([| of_Z (Z.max (Z.min e (emax - emin)) (emin - emax - 1) + shift)|]%int63 - shift = Z.max (Z.min e (emax - emin)) (emin - emax - 1))%Z).
   {
-    intro.
-    rewrite Int63.add_spec.
-    rewrite of_Z_spec.
-    rewrite shift_value.
-    simpl.
-    unfold wB.
-    unfold size.
-    simpl.
-    unfold Z.pow_pos.
-    simpl.
+    intro e1.
+    rewrite of_Z_spec, shift_value.
+    unfold wB, size; simpl.
+    unfold Z.pow_pos; simpl.
     set (n := Z.max (Z.min _ _) _).
-    set (wB := 9223372036854775808%Z).
+    set (wB := 9223372036854775808%Z). (* Z.pow_pos 2 63 *)
     assert (-2099 <= n <= 2098)%Z by (unfold n; lia).
-    rewrite Z.add_mod_idemp_l by (unfold wB; lia).
-    destruct H as (H1, H2).
     rewrite Z.mod_small by (unfold wB; lia).
     now rewrite Z.add_simpl_r.
   }
@@ -79,17 +71,17 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
         assert (H' : forall p p', digits2_pos (shift_pos p p') = (digits2_pos p' + p)%positive).
         {
           induction p0.
-          intro.
+          intro p'.
           simpl.
           rewrite IHp0.
           rewrite IHp0.
           lia.
-          intro.
+          intro p'.
           simpl.
           rewrite IHp0.
           rewrite IHp0.
           lia.
-          intro.
+          intro p'.
           simpl.
           lia.
         }
@@ -161,7 +153,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
     {
       assert (Hshr1 : forall s, Zdigits2 (shr_m (shr_1 s)) = Z.max 0 (Zdigits2 (shr_m s) - 1)%Z).
       {
-        intro.
+        intro s0.
         destruct s0.
         unfold shr_1.
         destruct shr_m; try (simpl; lia).
@@ -170,7 +162,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       }
       induction p.
       simpl.
-      intro.
+      intro s0.
       do 2 rewrite IHp.
       rewrite Hshr1.
       lia.
@@ -183,7 +175,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
 
     assert (Hd0 : forall z, Zdigits2 z = 0%Z -> z = 0%Z).
     {
-      intro.
+      intro z.
       unfold Zdigits2.
       now destruct z.
     }
diff --git a/theories/Floats/FloatOps.v b/theories/Floats/FloatOps.v
index 5ffbfc7215..f0d3bcced9 100644
--- a/theories/Floats/FloatOps.v
+++ b/theories/Floats/FloatOps.v
@@ -6,13 +6,15 @@ Definition prec := 53%Z.
 Definition emax := 1024%Z.
 Notation emin := (emin prec emax).
 
+Definition shift := 2101%Z. (** [= 2*emax + prec] *)
+
 Definition frexp f :=
   let (m, se) := frshiftexp f in
-  (m, ([| se |] - [| shift |])%Z%int63).
+  (m, ([| se |] - shift)%Z%int63).
 
 Definition ldexp f e :=
   let e' := Z.max (Z.min e (emax - emin)) (emin - emax - 1) in
-  ldshiftexp f (of_Z e' + shift).
+  ldshiftexp f (of_Z (e' + shift)).
 
 Definition ulp f := ldexp one (fexp prec emax (snd (frexp f))).
 
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index 880252c2b9..bc1727469d 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -73,8 +73,6 @@ The sign bit is always ignored. *)
 Primitive normfr_mantissa := #float64_normfr_mantissa.
 
 (** ** Exponent manipulation functions *)
-Definition shift := 2101%int63. (** [= 2*emax + prec] *)
-
 (** [frshiftexp]: convert a float to fractional part in $[0.5, 1.)$#[0.5, 1.)#
 and integer part. *)
 Primitive frshiftexp := #float64_frshiftexp.