From 0ed1016e3a072bc43461798863a6e811233e05fd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 24 Aug 2018 22:12:31 -0400 Subject: Minor rshi tweaks --- src/Util/ZUtil/Rshi.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src') diff --git a/src/Util/ZUtil/Rshi.v b/src/Util/ZUtil/Rshi.v index 132c7d8a6..fff2b68df 100644 --- a/src/Util/ZUtil/Rshi.v +++ b/src/Util/ZUtil/Rshi.v @@ -5,6 +5,7 @@ Require Import Crypto.Util.ZUtil.ZSimplify.Core. Require Import Crypto.Util.ZUtil.ZSimplify.Simple. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Hints.PullPush. Local Open Scope Z_scope. @@ -26,6 +27,13 @@ Module Z. | _ => omega end. Qed. + + Lemma rshi_correct_full_alt : forall s a b n, + Z.rshi s a b n = if (0 <=? n) + then ((b + a * s) / 2 ^ n) mod s + else (b * 2 ^ (-n)) mod s. + Proof. intros; rewrite rshi_correct_full; push_Zmod; pull_Zmod; autorewrite with zsimplify_const; reflexivity. Qed. + Lemma rshi_correct : forall s a b n, 0 <= n -> s <> 0 -> Z.rshi s a b n = ((b + a * s) / 2 ^ n) mod s. Proof. intros; rewrite rshi_correct_full; break_match; Z.ltb_to_lt; omega. Qed. -- cgit v1.2.3