From 57c8f2b364e139898dd45968842c15c3e382d5e1 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 28 Sep 2018 17:41:18 -0400 Subject: Fix and prove bounds for fancymachine operations --- src/Util/ZUtil/Rshi.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ZUtil/Rshi.v b/src/Util/ZUtil/Rshi.v index fff2b68df..38d2ddb00 100644 --- a/src/Util/ZUtil/Rshi.v +++ b/src/Util/ZUtil/Rshi.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.ZUtil.ZSimplify. Require Import Crypto.Util.ZUtil.ZSimplify.Core. @@ -6,6 +7,7 @@ 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.Tactics.DivModToQuotRem. Require Import Crypto.Util.ZUtil.Hints.PullPush. Local Open Scope Z_scope. @@ -37,4 +39,17 @@ Module Z. 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. + + Lemma rshi_small s a b n : + (0 <= b < s) -> + (0 <= a < 2^ n) -> + (0 <= n) -> + Z.rshi s a b n = ((b + a * s) / 2 ^ n). + Proof. + intros. + rewrite Z.rshi_correct by auto with zarith. + apply Z.mod_small. + Z.div_mod_to_quot_rem; nia. + Qed. + End Z. -- cgit v1.2.3