blob: 98cf3cf9cddc4d2f23e4f96a60d740a67daa0fae (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.LegacyArithmetic.Interface.
Require Import Crypto.Util.ZUtil.Notations.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.Testbit.
Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.ZUtil.Tactics.Ztestbit.
Require Import Crypto.Util.Tactics.UniquePose.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Export Crypto.Util.ZUtil.ZSimplify.Autogenerated.
Require Export Crypto.Util.ZUtil.ZSimplify.Core.
Require Export Crypto.Util.ZUtil.ZSimplify.Simple.
Require Export Crypto.Util.ZUtil.LandLorShiftBounds.
Local Open Scope Z_scope.
Local Arguments Z.pow !_ !_.
Local Arguments Z.mul !_ !_.
Ltac shift_left_right_t :=
repeat match goal with
| [ |- ?x = ?x ] => reflexivity
| [ |- Z.testbit ?x ?n = Z.testbit ?x ?n' ] => apply f_equal; try omega
| [ |- orb (Z.testbit ?x _) (Z.testbit ?y _) = orb (Z.testbit ?x _) (Z.testbit ?y _) ]
=> apply f_equal2
| _ => progress Z.ltb_to_lt
| _ => progress subst
| _ => progress unfold AutoRewrite.rewrite_eq
| _ => progress intros
| _ => omega
| _ => solve [ trivial ]
| _ => progress break_match_step ltac:(fun _ => idtac)
| [ |- context[Z.lor (?x >> ?count) (Z.pow2_mod (?y << (?n - ?count)) ?n)] ]
=> unique assert (0 <= Z.lor (x >> count) (Z.pow2_mod (y << (n - count)) n) < 2 ^ n) by (autorewrite with Zshift_to_pow; auto with zarith nia)
| _ => progress push_decode
| [ |- context[Interface.decode (fst ?x)] ] => is_var x; destruct x; simpl in *
| [ |- context[@Interface.decode ?n ?W ?d ?x] ] => is_var x; generalize dependent (@Interface.decode n W d x); intros
| _ => progress Z.rewrite_mod_small
| _ => progress autorewrite with convert_to_Ztestbit
| _ => progress autorewrite with zsimplify_fast
| [ |- _ = _ :> Z ] => apply Z.bits_inj'; intros
| _ => progress autorewrite with Ztestbit_full
| _ => progress autorewrite with bool_congr
| [ |- Z.testbit _ (?x - ?y + (?y - ?z)) = false ]
=> autorewrite with zsimplify
| [ H : 0 <= ?x < 2^?n |- Z.testbit ?x ?n' = false ]
=> assert (n <= n') by auto with zarith; progress Ztestbit
| _ => progress Ztestbit_full
end.
|
