blob: b8f9c7c66cd10c1d2d31d9b6bf22c1f331a15678 (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.omega.Omega.
Require Import Coq.micromega.Lia.
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.ZRange.Operations.
Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.SpecializeAllWays.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.Tactics.DestructHead.
Module ZRange.
Import Operations.ZRange.
Local Open Scope zrange_scope.
Local Notation eta v := r[ lower v ~> upper v ].
Local Ltac t_step :=
first [ reflexivity
| progress destruct_head' zrange
| progress cbv -[Z.min Z.max Z.le Z.lt Z.ge Z.gt andb Z.leb Z.geb] in *
| progress split_min_max
| match goal with
| [ |- _ = _ :> zrange ] => apply f_equal2
end
| omega
| solve [ auto ] ].
Local Ltac t := repeat t_step.
Lemma flip_flip v : flip (flip v) = v.
Proof. destruct v; reflexivity. Qed.
Lemma normalize_flip v : normalize (flip v) = normalize v.
Proof. t. Qed.
Lemma normalize_idempotent v : normalize (normalize v) = normalize v.
Proof. t. Qed.
Definition normalize_or v : normalize v = v \/ normalize v = flip v.
Proof. t. Qed.
Local Ltac t2_step :=
first [ t_step
| rewrite !Bool.andb_true_iff
| rewrite !Z.leb_le
| rewrite !Z.leb_gt
| rewrite Bool.andb_true_iff in *
| rewrite Z.leb_le in *
| rewrite Z.leb_gt in *
| progress intros
| match goal with
| [ H : context[andb _ _ = true] |- _ ] => setoid_rewrite Bool.andb_true_iff in H
| [ |- context[andb _ _ = true] ] => setoid_rewrite Bool.andb_true_iff
| [ H : context[Z.leb _ _ = true] |- _ ] => setoid_rewrite Z.leb_le in H
| [ |- context[Z.leb _ _ = true] ] => setoid_rewrite Z.leb_le
| [ H : context[Z.leb _ _ = false] |- _ ] => setoid_rewrite Z.leb_gt in H
| [ |- context[Z.leb _ _ = false] ] => setoid_rewrite Z.leb_gt
| [ |- and _ _ ] => apply conj
| [ |- or _ (true = false) ] => left
| [ |- or _ (false = true) ] => left
| [ |- or _ (?x = ?x) ] => right
| [ H : true = false |- _ ] => exfalso; clear -H; discriminate
end
| progress specialize_by omega
| progress destruct_head'_or ].
Lemma is_bounded_by_iff_is_tighter_than r1 r2
: (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true)
<-> (is_tighter_than_bool r1 r2 = true \/ goodb r1 = false).
Proof. repeat t2_step; specialize_all_ways; repeat t2_step. Qed.
Lemma is_bounded_by_iff_is_tighter_than_good r1 r2 (Hgood : goodb r1 = true)
: (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true)
<-> (is_tighter_than_bool r1 r2 = true).
Proof. rewrite is_bounded_by_iff_is_tighter_than; intuition (congruence || auto). Qed.
End ZRange.
|
