From 3abc81d25a5216037e51eca5a820d6d9fa4649d8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 15 Feb 2022 19:39:36 +0100 Subject: int_mods_modu --- kvx/FPDivision32.v | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) (limited to 'kvx') 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. -- cgit