blob: 6486b2e000350d54f8db47135c82ea33481c06e1 (
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Psatz.
Require Import Crypto.Compilers.Z.Bounds.Interpretation.
Require Import Crypto.Util.ZUtil.Hints.
Require Import Crypto.Util.ZUtil.Hints.Core.
Require Import Crypto.Util.ZUtil.ZSimplify.Core.
Require Import Crypto.Util.ZUtil.Log2.
Require Import Crypto.Util.ZUtil.Shift.
Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.ZUtil.Notations.
Require Import Crypto.Util.ZRange.Operations.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.FixedWordSizesEquality.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.SplitInContext.
Require Import Crypto.Util.Tactics.UniquePose.
Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
Local Open Scope Z_scope.
Ltac break_t_step :=
first [ progress destruct_head'_and
| progress destruct_head'_or
| progress destruct_head'_prod
| progress split_andb
| break_innermost_match_step ].
Ltac fin_t :=
first [ reflexivity
| assumption
| match goal with
| [ |- and _ _ ]
=> first [ split; [ | solve [ fin_t ] ]
| split; [ solve [ fin_t ] | ] ];
try solve [ fin_t ]
end
| omega ].
Ltac specializer_t_step :=
first [ progress specialize_by_assumption
| progress specialize_by fin_t ].
Ltac Zarith_t_step :=
first [ match goal with
| [ H : (?x <= ?y)%Z, H' : (?y <= ?x)%Z |- _ ]
=> assert (x = y) by omega; clear H H'
end
| progress Z.ltb_to_lt_in_context ].
Ltac Zarith_land_lor_t_step :=
match goal with
| [ |- _ <= Z.lor _ _ <= _ ]
=> split; etransitivity; [ | apply Z.lor_bounds; omega | apply Z.lor_bounds; omega | ]
| [ |- 2^Z.log2_up (?x + 1) - 1 <= 2^Z.log2_up (?y + 1) - 1 ]
=> let H := fresh in assert (H : x <= y) by omega; rewrite H; reflexivity
end.
Ltac word_arith_t :=
match goal with
| [ |- (0 <= FixedWordSizes.wordToZ ?w <= 2^2^Z.of_nat ?logsz - 1)%Z ]
=> clear; pose proof (@wordToZ_range logsz w); autorewrite with push_Zof_nat zsimplify_const in *; try omega
end.
Ltac case_Zvar_nonneg_on x :=
is_var x;
lazymatch type of x with
| Z => lazymatch goal with
| [ H : (0 <= x)%Z |- _ ] => fail
| [ H : (x < 0)%Z |- _ ] => fail
| _ => destruct (Z_lt_le_dec x 0); try omega
end
end.
Ltac case_Zvar_nonneg_step :=
match goal with
| [ |- context[?x] ]
=> case_Zvar_nonneg_on x
end.
Ltac case_Zvar_nonneg := repeat case_Zvar_nonneg_step.
Ltac remove_binary_operation_le_hyps_step :=
match goal with
| [ H : (?f ?x ?y <= ?f ?x ?y')%Z |- _ ]
=> assert ((y = y') \/ (y < y' /\ 0 <= x))%Z by (assert (y <= y')%Z by omega; nia);
clear H
| [ H : (?f ?y ?x <= ?f ?y' ?x)%Z |- _ ]
=> assert ((y = y') \/ (y < y' /\ 0 <= x))%Z by (assert (y <= y')%Z by omega; nia);
clear H
| [ H : (?f ?x ?y <= ?f ?x ?y')%Z |- _ ]
=> assert ((y = y') \/ (y' < y /\ x <= 0))%Z by (assert (y' <= y)%Z by omega; nia);
clear H
| [ H : (?f ?y ?x <= ?f ?y' ?x)%Z |- _ ]
=> assert ((y = y') \/ (y' < y /\ x <= 0))%Z by (assert (y' <= y)%Z by omega; nia);
clear H
| [ H : ?T, H' : ?T |- _ ] => clear H'
| [ H : ?A \/ (~?A /\ ?B), H' : ?A \/ (~?A /\ ?C) |- _ ]
=> assert (A \/ (~A /\ (B /\ C))) by (clear -H H'; tauto); clear H H'
| _ => progress destruct_head' or; destruct_head' and; subst; try omega
| [ |- (_ <= _ <= _)%Z ] => split
| _ => case_Zvar_nonneg_step
end.
Ltac saturate_with_shift_facts :=
repeat match goal with
| [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x << ?x'] ]
=> unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
| [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y << ?y'] ]
=> unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
| [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x >> ?y'] ]
=> unique assert (x >> y' <= y >> x') by (Z.shiftr_le_mono; omega)
| [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y >> ?x'] ]
=> unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega)
end.
Ltac saturate_with_all_shift_facts :=
repeat match goal with
| _ => progress saturate_with_shift_facts
| [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftl _ _] ]
=> unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
| [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftr _ _] ]
=> unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega)
end.
Ltac preprocess_shift_min_max :=
repeat first [ rewrite (Z.min_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
| rewrite (Z.min_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
| rewrite (Z.max_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
| rewrite (Z.max_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
| rewrite (Z.min_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
| rewrite (Z.min_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
| rewrite (Z.max_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
| rewrite (Z.max_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) ].
Ltac saturate_land_lor_facts :=
repeat match goal with
| [ |- context[Z.land ?x ?y] ]
=> let H := fresh in
let H' := fresh in
assert (H : 0 <= x) by omega;
assert (H' : 0 <= y) by omega;
unique pose proof (Z.land_upper_bound_r x y H H');
unique pose proof (Z.land_upper_bound_l x y H H')
| [ |- context[Z.land ?x ?y] ]
=> unique assert (0 <= Z.land x y) by (apply Z.land_nonneg; omega)
| [ |- context[Z.land ?x ?y] ]
=> case_Zvar_nonneg_on x; case_Zvar_nonneg_on y
| [ |- context[Z.lor ?x ?y] ]
=> let H := fresh in
let H' := fresh in
assert (H : 0 <= x) by omega;
assert (H' : 0 <= y) by omega;
unique pose proof (proj1 (Z.lor_bounds x y H H'));
unique pose proof (proj2 (Z.lor_bounds x y H H'))
| [ |- context[Z.lor ?x ?y] ]
=> unique assert (0 <= Z.lor x y) by (apply Z.lor_nonneg; omega)
| [ |- context[Z.lor ?x ?y] ]
=> case_Zvar_nonneg_on x; case_Zvar_nonneg_on y
end.
Ltac handle_shift_neg :=
repeat first [ rewrite !Z.shiftr_opp_r
| rewrite !Z.shiftl_opp_r
| rewrite !Z.shiftr_opp_l
| rewrite !Z.shiftl_opp_l ].
Ltac handle_four_corners_step_fast :=
first [ progress destruct_head Bounds.t
| progress cbv [ZRange.four_corners] in *
| progress subst
| Zarith_t_step
| progress split_min_max
| omega
| nia ].
Ltac handle_four_corners_step :=
first [ handle_four_corners_step_fast
| remove_binary_operation_le_hyps_step ].
Ltac handle_four_corners :=
lazymatch goal with
| [ |- (ZRange.lower (ZRange.four_corners _ _ _) <= _ <= _)%Z ]
=> idtac
end;
repeat handle_four_corners_step.
Ltac rewriter_t :=
first [ rewrite !Bool.andb_true_iff
| rewrite !Bool.andb_false_iff
| rewrite !Bool.orb_true_iff
| rewrite !Bool.orb_false_iff
| rewrite !Z.abs_opp
| rewrite !Z.max_log2_up
| rewrite !Z.add_max_distr_r
| rewrite !Z.add_max_distr_l
| rewrite wordToZ_ZToWord by (autorewrite with push_Zof_nat zsimplify_const; omega)
| match goal with
| [ H : _ |- _ ]
=> first [ rewrite !Bool.andb_true_iff in H
| rewrite !Bool.andb_false_iff in H
| rewrite !Bool.orb_true_iff in H
| rewrite !Bool.orb_false_iff in H ]
end ].
|
