int_mods_modu

1 files changed, 58 insertions, 0 deletions

diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v
index edbcbe12..4e9b2fb2 100644
--- a/kvx/FPDivision32.v
+++ b/kvx/FPDivision32.v
@@ -753,3 +753,61 @@ Proof.
   repeat rewrite Z.sub_0_r.
   destruct zlt; destruct zlt; reflexivity.
 Qed.
+
+Lemma int_mods_modu :
+  forall a b
+    (b_NOT0 : Int.signed b <> 0),
+    Int.mods a b = if Int.lt a Int.zero
+                   then Int.neg (Int.modu (ExtValues.int_abs a)
+                                          (ExtValues.int_abs b))
+                   else Int.modu (ExtValues.int_abs a) (ExtValues.int_abs b).
+Proof.
+  intros.
+  unfold Int.mods, Int.modu, Int.lt, ExtValues.int_abs.
+  pose proof (Int.signed_range a) as a_RANGE.
+  pose proof (Int.signed_range b) as b_RANGE.
+  change (Int.signed Int.zero) with 0%Z.
+  destruct zlt.
+  - cbn. rewrite (Z.abs_neq (Int.signed a)) by lia.
+    rewrite (Int.unsigned_repr (- Int.signed a)); cycle 1.
+    { pose proof int_min_signed_unsigned. lia. }
+
+    destruct (zlt (Int.signed b) 0%Z).
+    + rewrite (Z.abs_neq (Int.signed b)) by lia.
+      rewrite Int.unsigned_repr ; cycle 1.
+      { pose proof int_min_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int.signed b)) at 1.
+      rewrite Z.rem_opp_r by lia.
+      rewrite <- (Z.opp_involutive (Int.signed a)) at 1.
+      rewrite Z.rem_opp_l by lia.
+      rewrite Z.rem_mod_nonneg by lia.
+      rewrite Int.neg_repr.
+      reflexivity.
+      
+    + rewrite (Z.abs_eq (Int.signed b)) by lia.
+      rewrite Int.unsigned_repr ; cycle 1.
+      { pose proof Int.max_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int.signed a)) at 1.
+      rewrite Z.rem_opp_l by lia.
+      rewrite Z.rem_mod_nonneg by lia.
+      rewrite Int.neg_repr.
+      reflexivity.
+    
+  - cbn. rewrite (Z.abs_eq (Int.signed a)) by lia.
+    rewrite (Int.unsigned_repr (Int.signed a)); cycle 1.
+    { pose proof Int.max_signed_unsigned. lia. }
+    destruct (zlt (Int.signed b) 0%Z).
+    + rewrite (Z.abs_neq (Int.signed b)) by lia.
+      rewrite Int.unsigned_repr ; cycle 1.
+      { pose proof int_min_signed_unsigned. lia. }
+      rewrite <- (Z.opp_involutive (Int.signed b)) at 1.
+      rewrite Z.rem_opp_r by lia.
+      rewrite Z.rem_mod_nonneg by lia.
+      reflexivity.
+      
+    + rewrite (Z.abs_eq (Int.signed b)) by lia.
+      rewrite Int.unsigned_repr ; cycle 1.
+      { pose proof Int.max_signed_unsigned. lia. }
+      rewrite Z.rem_mod_nonneg by lia.
+      reflexivity.
+Qed.