-
Notifications
You must be signed in to change notification settings - Fork 3
/
EquivalenceLemmas.v
197 lines (172 loc) · 5 KB
/
EquivalenceLemmas.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
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
Require Export SystemFR.Equivalence.
Require Export SystemFR.CBVNormalizingLemmas.
Lemma equivalent_refl:
forall t,
is_erased_term t ->
wf t 0 ->
pfv t term_var = nil ->
[ t ≡ t ].
Proof.
unfold equivalent_terms; steps.
Qed.
Ltac equivalent_refl :=
match goal with
| |- [ ?a ≡ ?a ] => apply equivalent_refl
end.
Lemma equivalent_sym:
forall t1 t2, [ t1 ≡ t2 ] -> [ t2 ≡ t1 ].
Proof.
unfold equivalent_terms; steps; eauto with eapply_any.
Qed.
Lemma equivalent_trans:
forall t1 t2 t3,
[ t1 ≡ t2 ] ->
[ t2 ≡ t3 ] ->
[ t1 ≡ t3 ]
.
Proof.
unfold equivalent_terms; steps; eauto 3 with apply_any.
- apply H13; auto; apply H12; auto.
Qed.
Lemma equivalent_square:
forall t1 t2 t3 t4,
[ t1 ≡ t3 ] ->
[ t1 ≡ t2 ] ->
[ t3 ≡ t4 ] ->
[ t2 ≡ t4 ].
Proof.
eauto using equivalent_trans, equivalent_sym.
Qed.
Lemma equivalent_open:
forall t1 k1 a1 t2 k2 a2,
[ t1 ≡ t2 ] ->
[ open k1 t1 a1 ≡ open k2 t2 a2 ].
Proof.
unfold equivalent_terms;
repeat step ||
(rewrite (open_none t1) in * by eauto with wf lia) ||
(rewrite (open_none t2) in * by eauto with wf lia);
eauto with apply_any.
Qed.
Lemma equivalent_star_true:
forall t1 t2,
[ t1 ≡ t2 ] ->
t1 ~>* ttrue ->
t2 ~>* ttrue.
Proof.
intros.
equivalence_instantiate (ite (lvar 0 term_var) ttrue tfalse);
unfold scbv_normalizing in *; steps.
unshelve epose proof (H3 _); repeat step || t_invert_star;
eauto using star_trans with smallstep cbvlemmas.
Qed.
Lemma equivalent_true:
forall t,
[ t ≡ ttrue ] ->
t ~>* ttrue.
Proof.
intros; eauto using equivalent_star_true, equivalent_sym with star.
Qed.
Lemma equivalent_value_true:
forall v,
[ v ≡ ttrue ] ->
cbv_value v ->
v = ttrue.
Proof.
intros.
apply_anywhere equivalent_true;
repeat step || t_invert_star.
Qed.
Lemma false_true_not_equivalent:
[ tfalse ≡ ttrue ] ->
False.
Proof.
repeat step || apply_anywhere equivalent_true || t_invert_star.
Qed.
Lemma equivalent_star_false:
forall t1 t2,
[ t1 ≡ t2 ] ->
t1 ~>* tfalse ->
t2 ~>* tfalse.
Proof.
intros.
equivalence_instantiate (ite (lvar 0 term_var) tfalse ttrue);
unfold scbv_normalizing in *; steps.
unshelve epose proof (H3 _); repeat step || t_invert_star;
eauto using star_trans with smallstep cbvlemmas.
Qed.
Lemma equivalent_false:
forall t,
[ t ≡ tfalse ] ->
t ~>* tfalse.
Proof.
intros; eauto using equivalent_star_false, equivalent_sym with star.
Qed.
Lemma equivalent_value_false:
forall v,
[ v ≡ tfalse ] ->
cbv_value v ->
v = tfalse.
Proof.
intros.
apply_anywhere equivalent_false;
repeat step || t_invert_star.
Qed.
Ltac one_step_normalizing :=
eapply scbv_normalizing_back; eauto with smallstep; steps;
unfold scbv_normalizing; steps; eauto with star values.
Ltac not_normalizing :=
top_level_unfold scbv_normalizing; repeat step || t_invert_star.
Lemma equivalent_value_unit:
forall v,
cbv_value v ->
[ uu ≡ v ] ->
v = uu.
Proof.
inversion 1;
repeat step.
- (* zero *)
equivalence_instantiate (tmatch (lvar 0 term_var) ttrue ttrue); steps.
unshelve epose proof (H4 _);
repeat step || t_invert_star;
eauto using star_one, scbv_step_same with smallstep values.
- (* succ *)
equivalence_instantiate (tmatch (lvar 0 term_var) ttrue ttrue); steps.
unshelve epose proof (H5 _);
repeat step || t_invert_star;
eauto using star_one, scbv_step_same with smallstep values.
- (* false *)
equivalence_instantiate (ite (lvar 0 term_var) ttrue ttrue); steps.
unshelve epose proof (H4 _);
repeat step || t_invert_star;
eauto using star_one, scbv_step_same with smallstep values.
- (* true *)
equivalence_instantiate (ite (lvar 0 term_var) ttrue ttrue); steps.
unshelve epose proof (H4 _);
repeat step || t_invert_star;
eauto using star_one, scbv_step_same with smallstep values.
- (* pair *)
equivalence_instantiate (app (notype_lambda ttrue) (pi1 (lvar 0 term_var))); steps.
unshelve epose proof (H6 _);
repeat step || t_invert_star.
eapply star_trans;
eauto using scbv_step_same, star_one with smallstep cbvlemmas values.
- (* lambda *)
equivalence_instantiate (ite (boolean_recognizer 2 (lvar 0 term_var)) ttrue tfalse);
repeat step.
unshelve epose proof (H4 _).
+ eapply star_trans;
eauto using scbv_step_same, star_one with smallstep cbvlemmas values.
+ repeat step || t_invert_star.
inversion H8; repeat step || t_invert_star.
- (* left *)
equivalence_instantiate (sum_match (lvar 0 term_var) ttrue ttrue); steps.
unshelve epose proof (H5 _);
repeat step || t_invert_star;
eauto using star_one, scbv_step_same with smallstep values.
- (* right *)
equivalence_instantiate (sum_match (lvar 0 term_var) ttrue ttrue); steps.
unshelve epose proof (H5 _);
repeat step || t_invert_star;
eauto using star_one, scbv_step_same with smallstep values.
Qed.