-
Notifications
You must be signed in to change notification settings - Fork 2
/
BasicUtility.v
178 lines (148 loc) · 4.53 KB
/
BasicUtility.v
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
Require Import Coq.btauto.Btauto Coq.NArith.Nnat.
Require Import Dirac.
Definition var := nat.
Definition posi : Type := (var * nat).
Definition posi_eq (r1 r2 : posi) : bool :=
match r1 with (x1,y1)
=> match r2
with (x2,y2) => (x1 =? x2) && (y1 =? y2)
end
end.
Notation "i '==?' j" := (posi_eq i j) (at level 50).
Lemma posi_eqb_eq : forall a b, a ==? b = true -> a = b.
Proof.
intros. unfold posi_eq in H.
destruct a. destruct b.
apply andb_true_iff in H.
destruct H. apply Nat.eqb_eq in H.
apply Nat.eqb_eq in H0. subst. easy.
Qed.
Lemma posi_eqb_neq : forall a b, a ==? b = false -> a <> b.
Proof.
intros. unfold posi_eq in H.
destruct a. destruct b.
apply andb_false_iff in H.
destruct H. apply Nat.eqb_neq in H.
intros R. injection R as eq1.
rewrite eq1 in H. easy.
apply Nat.eqb_neq in H.
intros R. injection R as eq1.
rewrite H0 in H. easy.
Qed.
Lemma posi_eq_reflect : forall r1 r2, reflect (r1 = r2) (posi_eq r1 r2).
Proof.
intros.
destruct (r1 ==? r2) eqn:eq1.
apply ReflectT.
apply posi_eqb_eq in eq1.
assumption.
constructor.
apply posi_eqb_neq in eq1.
assumption.
Qed.
Hint Resolve posi_eq_reflect : bdestruct.
Lemma posi_eq_dec : forall x y : posi, {x = y}+{x <> y}.
Proof.
intros.
bdestruct (x ==? y). left. easy. right. easy.
Qed.
Definition rz_val : Type := (nat -> bool).
Inductive val := nval (b:bool) (r:rz_val) | qval (rc:rz_val) (r:rz_val).
(* Update the value at one index of a boolean function. *)
Definition eupdate {S} (f : posi -> S) (i : posi) (x : S) :=
fun j => if j ==? i then x else f j.
Lemma eupdate_index_eq {S} : forall (f : posi -> S) i b, (eupdate f i b) i = b.
Proof.
intros.
unfold eupdate.
bdestruct (i ==? i). easy.
contradiction.
Qed.
Lemma eupdate_index_neq {S}: forall (f : posi -> S) i j b, i <> j -> (eupdate f i b) j = f j.
Proof.
intros.
unfold eupdate.
bdestruct (j ==? i).
subst. contradiction.
reflexivity.
Qed.
Lemma eupdate_same {S}: forall (f : posi -> S) i b,
b = f i -> eupdate f i b = f.
Proof.
intros.
apply functional_extensionality.
intros.
unfold eupdate.
bdestruct (x ==? i); subst; reflexivity.
Qed.
Lemma eupdate_same_1 {S}: forall (f f': posi -> S) i b b',
f = f' -> b = b' -> eupdate f i b = eupdate f' i b'.
Proof.
intros.
apply functional_extensionality.
intros.
unfold eupdate.
bdestruct (x ==? i); subst; reflexivity.
Qed.
Lemma eupdate_twice_eq {S}: forall (f : posi -> S) i b b',
eupdate (eupdate f i b) i b' = eupdate f i b'.
Proof.
intros.
apply functional_extensionality.
intros.
unfold eupdate.
bdestruct (x ==? i); subst; reflexivity.
Qed.
Lemma eupdate_twice_neq {S}: forall (f : posi -> S) i j b b',
i <> j -> eupdate (eupdate f i b) j b' = eupdate (eupdate f j b') i b.
Proof.
intros.
apply functional_extensionality.
intros.
unfold eupdate.
bdestruct (x ==? i); bdestruct (x ==? j); subst; easy.
Qed.
Notation "f '[' i '|->' x ']'" := (eupdate f i x) (at level 10).
Lemma same_eupdate : forall (f f' : posi -> val) c v, f = f' -> f[c |-> v] = f'[c |-> v].
Proof.
intros.
apply functional_extensionality.
intros.
bdestruct (c ==? x).
subst.
rewrite eupdate_index_eq. easy.
rewrite eupdate_index_neq.
rewrite eupdate_index_neq. subst. easy.
assumption. assumption.
Qed.
Lemma same_eupdate_1 : forall (f f' : posi -> val) c v v', f = f' -> v = v' -> f[c |-> v] = f'[c |-> v'].
Proof.
intros.
apply functional_extensionality.
intros.
bdestruct (c ==? x).
subst.
rewrite eupdate_index_eq. easy.
rewrite eupdate_index_neq.
rewrite eupdate_index_neq. subst. easy.
assumption. assumption.
Qed.
(* Adds an equality in the context *)
Ltac ctx e1 e2 :=
let H := fresh "HCtx" in
assert (e1 = e2) as H by reflexivity.
(* Standard inversion/subst/clear abbrev. *)
Tactic Notation "inv" hyp(H) := inversion H; subst; clear H.
Tactic Notation "inv" hyp(H) "as" simple_intropattern(p) :=
inversion H as p; subst; clear H.
(*
Ltac fb_push_n_simpl := repeat (try rewrite fb_push_n_left by lia; try rewrite fb_push_n_right by lia).
Ltac update_simpl := repeat (try rewrite update_index_neq by lia); try rewrite update_index_eq by lia.
*)
Ltac BreakIfExpression :=
match goal with
| [ |- context[if ?X <? ?Y then _ else _] ] => bdestruct (X <? Y); try lia
| [ |- context[if ?X <=? ?Y then _ else _] ] => bdestruct (X <=? Y); try lia
| [ |- context[if ?X =? ?Y then _ else _] ] => bdestruct (X =? Y); try lia
end.
Ltac IfExpSimpl := repeat BreakIfExpression.