blob: 41234bf6ee992b1345d9ef47d4d6b1f0b614be49 (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.LegacyArithmetic.Interface.
Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.Tactics.UniquePose.
Require Import Crypto.Util.Tactics.BreakMatch.
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.
|
