diff options
Diffstat (limited to 'src/Util/ZUtil/Rshi.v')
-rw-r--r-- | src/Util/ZUtil/Rshi.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Rshi.v b/src/Util/ZUtil/Rshi.v new file mode 100644 index 000000000..9a1d8a20b --- /dev/null +++ b/src/Util/ZUtil/Rshi.v @@ -0,0 +1,20 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Hints.PullPush. +Local Open Scope Z_scope. + +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. + cbv [Z.rshi]; intros. pose proof (Z.log2_nonneg s). + break_match; + repeat match goal with + | H : _ = s |- _ => rewrite H + | _ => rewrite Z.land_ones by auto with zarith + | _ => progress autorewrite with Zshift_to_pow push_Zpow + | _ => reflexivity + end. + Qed. +End Z.
\ No newline at end of file |