blob: 11ae2f87da6950a3c4ddddeede01d86843edd94a (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.ZUtil.Hints.Core.
Local Open Scope Z.
Module Z.
Ltac peel_le_step :=
match goal with
| [ |- ?x + _ <= ?x + _ ]
=> apply Z.add_le_mono_l
| [ |- _ + ?x <= _ + ?x ]
=> apply Z.add_le_mono_r
| [ |- ?x - _ <= ?x - _ ]
=> apply Z.sub_le_mono_l
| [ |- _ - ?x <= _ - ?x ]
=> apply Z.sub_le_mono_r
| [ |- ?x^_ <= ?x^_ ]
=> apply Z.pow_le_mono_r; [ zutil_arith | ]
| [ |- _^?x <= _^?x ]
=> apply Z.pow_le_mono_l; split; [ zutil_arith | ]
| [ |- Z.log2_up _ <= Z.log2_up _ ]
=> apply Z.log2_up_le_mono
| [ |- Z.log2 _ <= Z.log2 _ ]
=> apply Z.log2_le_mono
| [ |- Z.succ _ <= Z.succ _ ]
=> apply Zsucc_le_compat
| [ |- Z.pred _ <= Z.pred _ ]
=> apply Z.pred_le_mono
| [ |- ?x * _ <= ?x * _ ]
=> first [ apply Z.mul_le_mono_nonneg_l; [ zutil_arith | ]
| apply Z.mul_le_mono_nonpos_l; [ zutil_arith | ] ]
| [ |- _ * ?x <= _ * ?x ]
=> first [ apply Z.mul_le_mono_nonneg_r; [ zutil_arith | ]
| apply Z.mul_le_mono_nonpos_r; [ zutil_arith | ] ]
| [ |- -_ <= -_ ]
=> apply -> Z.opp_le_mono
| [ |- _ / ?x <= _ / ?x ]
=> apply Z.div_le_mono; [ zutil_arith | ]
| [ |- ?x / _ <= ?x / _ ]
=> apply Z.div_le_compat_l; [ zutil_arith | split; [ zutil_arith | ] ]
| [ |- Z.quot _ ?x <= Z.quot _ ?x ]
=> apply Z.quot_le_mono; [ zutil_arith | ]
| [ |- Z.quot ?x _ <= Z.quot ?x _ ]
=> apply Z.quot_le_compat_l; [ zutil_arith | split; [ zutil_arith | ] ]
| [ |- Z.max ?x _ <= Z.max ?x _ ]
=> apply Z.max_le_compat_l
| [ |- Z.max _ ?x <= Z.max _ ?x ]
=> apply Z.max_le_compat_r
| [ |- Z.min ?x _ <= Z.min ?x _ ]
=> apply Z.min_le_compat_l
| [ |- Z.min _ ?x <= Z.min _ ?x ]
=> apply Z.min_le_compat_r
end.
Ltac peel_le := repeat peel_le_step.
End Z.
|
