blob: d12de53306db31cf73cf340b5c7f6698f5748976 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.ZUtil.Testbit.
Require Import Crypto.Util.ZUtil.Hints.Core.
Ltac Ztestbit_full_step :=
match goal with
| _ => progress autorewrite with Ztestbit_full
| [ |- context[Z.testbit ?x ?y] ]
=> rewrite (Z.testbit_neg_r x y) by zutil_arith
| [ |- context[Z.testbit ?x ?y] ]
=> rewrite (Z.bits_above_pow2 x y) by zutil_arith
| [ |- context[Z.testbit ?x ?y] ]
=> rewrite (Z.bits_above_log2 x y) by zutil_arith
end.
Ltac Ztestbit_full := repeat Ztestbit_full_step.
Ltac Ztestbit_step :=
match goal with
| _ => progress autorewrite with Ztestbit
| _ => progress Ztestbit_full_step
end.
Ltac Ztestbit := repeat Ztestbit_step.
|
