diff options
author | Jade Philipoom <jadep@google.com> | 2018-04-11 17:46:52 +0200 |
---|---|---|
committer | Jade Philipoom <jadep@google.com> | 2018-04-11 17:46:52 +0200 |
commit | 7390f15dc735997a846196390f402edda192ff34 (patch) | |
tree | 77932689b26e0e147572fc94366afaad6a72c3bd /src/Util/ZUtil/CC.v | |
parent | 0d2f18249f65211ad6fe318e193bfdf43d244303 (diff) |
Add new assembly-mimicking operations rshi, cc_m, and cc_l
Diffstat (limited to 'src/Util/ZUtil/CC.v')
-rw-r--r-- | src/Util/ZUtil/CC.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/src/Util/ZUtil/CC.v b/src/Util/ZUtil/CC.v new file mode 100644 index 000000000..fb2fb1b93 --- /dev/null +++ b/src/Util/ZUtil/CC.v @@ -0,0 +1,32 @@ +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Hints.PullPush. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Local Open Scope Z_scope. + +Module Z. + Hint Rewrite Z.log2_pow2 Z.pow_1_r using solve [auto using Z.log2_nonneg with zarith] : push_Zpow. + + Lemma cc_m_eq : forall s x, 2 < s -> Z.cc_m s x = x / (s / 2). + Proof. + intros; cbv [Z.cc_m]. + assert (1 <= Z.log2 s) by (rewrite <-Z.log2_2; auto using Z.log2_le_mono with lia). + break_match; [ | reflexivity ]. + match goal with H : _ = s |- _ => rewrite <-H end. + autorewrite with Zshift_to_pow push_Zpow. + reflexivity. + Qed. + + Lemma cc_m_small : forall s x, 2 < s -> s mod 2 = 0 -> 0 <= x < s -> 0 <= Z.cc_m s x < 2. + Proof. + intros. rewrite cc_m_eq by auto. + repeat match goal with + | _ => split + | _ => apply Z.div_lt_upper_bound + | _ => solve [Z.zero_bounds] + end. + Z.div_mod_to_quot_rem; lia. + Qed. +End Z.
\ No newline at end of file |