blob: d57577210a0a25c13a0dec2dbdd71d12f8a65101 (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.ZRange.Operations.
Require Import Crypto.Util.ZRange.BasicLemmas.
Require Import Crypto.Util.ZRange.CornersMonotoneBounds.
Require Import Crypto.Util.ZRange.LandLorBounds.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.Morphisms.
Require Import Crypto.Util.Notations.
Module ZRange.
Local Ltac t :=
lazymatch goal with
| [ |- is_bounded_by_bool (?f _) (ZRange.two_corners ?f _) = true ]
=> apply (@ZRange.monotoneb_two_corners_gen f)
| [ |- is_bounded_by_bool (?f _ _) (ZRange.four_corners ?f _ _) = true ]
=> apply (@ZRange.monotoneb_four_corners_gen f)
| [ |- is_bounded_by_bool (?f _ _) (ZRange.four_corners_and_zero ?f _ _) = true ]
=> apply (@ZRange.monotoneb_four_corners_and_zero_gen f)
end;
eauto with zarith;
repeat match goal with
| [ |- forall x : Z, _ ] => let x := fresh "x" in intro x; destruct x
end;
eauto with zarith.
Lemma is_bounded_by_bool_log2
x x_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
: is_bounded_by_bool (Z.log2 x) (ZRange.log2 x_bs) = true.
Proof. t. Qed.
Lemma is_bounded_by_bool_log2_up
x x_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
: is_bounded_by_bool (Z.log2_up x) (ZRange.log2_up x_bs) = true.
Proof. t. Qed.
Lemma is_bounded_by_bool_add
x x_bs y y_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
(Hboundedy : is_bounded_by_bool y y_bs = true)
: is_bounded_by_bool (Z.add x y) (ZRange.add x_bs y_bs) = true.
Proof. t. Qed.
Lemma is_bounded_by_bool_sub
x x_bs y y_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
(Hboundedy : is_bounded_by_bool y y_bs = true)
: is_bounded_by_bool (Z.sub x y) (ZRange.sub x_bs y_bs) = true.
Proof. t. Qed.
Lemma is_bounded_by_bool_mul
x x_bs y y_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
(Hboundedy : is_bounded_by_bool y y_bs = true)
: is_bounded_by_bool (Z.mul x y) (ZRange.mul x_bs y_bs) = true.
Proof. t. Qed.
Lemma is_bounded_by_bool_div
x x_bs y y_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
(Hboundedy : is_bounded_by_bool y y_bs = true)
: is_bounded_by_bool (Z.div x y) (ZRange.div x_bs y_bs) = true.
Proof. t. Qed.
Lemma is_bounded_by_bool_shiftr
x x_bs y y_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
(Hboundedy : is_bounded_by_bool y y_bs = true)
: is_bounded_by_bool (Z.shiftr x y) (ZRange.shiftr x_bs y_bs) = true.
Proof. t. Qed.
Lemma is_bounded_by_bool_shiftl
x x_bs y y_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
(Hboundedy : is_bounded_by_bool y y_bs = true)
: is_bounded_by_bool (Z.shiftl x y) (ZRange.shiftl x_bs y_bs) = true.
Proof. t. Qed.
Lemma is_bounded_by_bool_land
x x_bs y y_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
(Hboundedy : is_bounded_by_bool y y_bs = true)
: is_bounded_by_bool (Z.land x y) (ZRange.land x_bs y_bs) = true.
Proof. now apply ZRange.is_bounded_by_bool_land_bounds. Qed.
Lemma is_bounded_by_bool_lor
x x_bs y y_bs
(Hboundedx : is_bounded_by_bool x x_bs = true)
(Hboundedy : is_bounded_by_bool y y_bs = true)
: is_bounded_by_bool (Z.lor x y) (ZRange.lor x_bs y_bs) = true.
Proof. now apply ZRange.is_bounded_by_bool_lor_bounds. Qed.
End ZRange.
|
