diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-13 10:46:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-13 10:46:17 -0400 |
| commit | 4ecdd6ca43af688e5cd36ec9ab2496c4e192477d (patch) | |
| tree | e67cd24bf8cd7de2dee68253a5a6db3b5f567241 /src/Util/ZUtil/Hints.v | |
| parent | facfba480b7ce797ecf70e9d128d0392d1250360 (diff) | |
Split off ZUtil initial hint databases
Diffstat (limited to 'src/Util/ZUtil/Hints.v')
| -rw-r--r-- | src/Util/ZUtil/Hints.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Hints.v b/src/Util/ZUtil/Hints.v new file mode 100644 index 000000000..6f554174e --- /dev/null +++ b/src/Util/ZUtil/Hints.v @@ -0,0 +1,13 @@ +(** * Hint Databases with lemmas about ℤ from the standard library *) +Require Import Coq.ZArith.ZArith. +Require Export Crypto.Util.ZUtil.Hints.Core. +Require Export Crypto.Util.ZUtil.Hints.ZArith. +Require Export Crypto.Util.ZUtil.Hints.Ztestbit. +Require Export Crypto.Util.ZUtil.Hints.PullPush. +Require Export Crypto.Util.ZUtil.ZSimplify.Core. + +Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2. +Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2. + +(** For the occasional lemma that can remove the use of [Z.div] *) +Hint Rewrite Z.div_small_iff using zutil_arith : zstrip_div. |