aboutsummaryrefslogtreecommitdiffstats
path: root/complete.v
diff options
context:
space:
mode:
Diffstat (limited to 'complete.v')
-rw-r--r--complete.v413
1 files changed, 413 insertions, 0 deletions
diff --git a/complete.v b/complete.v
new file mode 100644
index 0000000..9939b50
--- /dev/null
+++ b/complete.v
@@ -0,0 +1,413 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import gmap relations.
3From mininix Require Import binop expr interpreter maptools matching sem.
4
5Lemma eval_le n uf e v' :
6 eval n uf e = Some v' →
7 ∀ m, n ≤ m → eval m uf e = Some v'.
8Proof.
9 revert uf e v'.
10 induction n; [discriminate|].
11 intros uf e v' Heval [] Hle; [lia|].
12 apply le_S_n in Hle.
13 rewrite eval_S in *.
14 destruct e; repeat (case_match || simplify_option_eq || by eauto).
15 apply bind_Some. exists H.
16 split; try by reflexivity.
17 apply map_mapM_Some_L in Heqo.
18 apply map_mapM_Some_L.
19 eapply map_Forall2_impl_L, Heqo.
20 eauto.
21Qed.
22
23Lemma eval_value n (v : value) : 0 < n → eval n false v = Some v.
24Proof. destruct n, v; by try lia. Qed.
25
26Lemma eval_strong_value n (sv : strong_value) :
27 0 < n →
28 eval n false sv = Some (value_from_strong_value sv).
29Proof. destruct n, sv; by try lia. Qed.
30
31Lemma eval_force_strong_value v : ∃ n,
32 eval n true (expr_from_strong_value v) = Some (value_from_strong_value v).
33Proof.
34 induction v using strong_value_ind'; try by exists 2.
35 unfold expr_from_strong_value. simpl.
36 fold expr_from_strong_value.
37 induction bs using map_ind.
38 + by exists 2.
39 + apply map_Forall_insert in H as [[n Hn] H2]; try done.
40 apply IHbs in H2 as [o Ho]. clear IHbs.
41 exists (S (n `max` o)).
42 rewrite eval_S. csimpl.
43 setoid_rewrite map_mapM_Some_2_L
44 with (m2 := value_from_strong_value <$> <[i := x]>m); csimpl.
45 * by rewrite <-map_fmap_compose.
46 * destruct o as [|o]; csimpl in *; try discriminate.
47 apply map_Forall2_alt_L.
48 split.
49 -- set_solver.
50 -- intros j u v ??. rewrite eval_S in Ho.
51 apply bind_Some in Ho as [vs [Ho1 Ho2]].
52 setoid_rewrite map_mapM_Some_L in Ho1. simplify_eq.
53 unfold expr_from_strong_value in Ho2.
54 rewrite map_fmap_compose in Ho2.
55 simplify_eq.
56 destruct (decide (i = j)).
57 ++ simplify_eq.
58 repeat rewrite lookup_fmap, lookup_insert in *.
59 simplify_eq/=.
60 apply eval_le with (n := n); lia || done.
61 ++ repeat rewrite lookup_fmap, lookup_insert_ne in * by done.
62 repeat rewrite <-lookup_fmap in *.
63 apply map_Forall2_alt_L in Ho1.
64 destruct Ho1 as [Ho1 Ho2].
65 apply eval_le with (n := o); try lia.
66 by apply Ho2 with (i := j).
67Qed.
68
69Lemma eval_force_strong_value' v :
70 ∃ n, eval n false (X_Force (expr_from_strong_value v)) =
71 Some (value_from_strong_value v).
72Proof.
73 destruct (eval_force_strong_value v) as [n Heval].
74 exists (S n). by rewrite eval_S.
75Qed.
76
77Lemma rec_subst_lookup bs x e :
78 bs !! x = Some (B_Nonrec e) → rec_subst bs !! x = Some e.
79Proof. unfold rec_subst. rewrite lookup_fmap. by intros ->. Qed.
80
81Lemma rec_subst_lookup_fmap bs x e :
82 bs !! x = Some e → rec_subst (B_Nonrec <$> bs) !! x = Some e.
83Proof. unfold rec_subst. do 2 rewrite lookup_fmap. by intros ->. Qed.
84
85Lemma rec_subst_lookup_fmap' bs x :
86 is_Some (bs !! x) ↔ is_Some (rec_subst (B_Nonrec <$> bs) !! x).
87Proof.
88 unfold rec_subst. split;
89 do 2 rewrite lookup_fmap in *;
90 intros [b H]; by simplify_option_eq.
91Qed.
92
93Lemma eval_base_step uf e e' v'' n :
94 e -->base e' →
95 eval n uf e' = Some v'' →
96 ∃ m, eval m uf e = Some v''.
97Proof.
98 intros [] Heval.
99 - (* E_Force *)
100 destruct uf.
101 + (* true *)
102 exists (S n). rewrite eval_S. by csimpl.
103 + (* false *)
104 destruct n; try discriminate.
105 rewrite eval_strong_value in Heval by lia.
106 simplify_option_eq.
107 apply eval_force_strong_value'.
108 - (* E_Closed *)
109 exists (S n). rewrite eval_S. by csimpl.
110 - (* E_Placeholder *)
111 exists (S n). rewrite eval_S. by csimpl.
112 - (* E_MSelect *)
113 destruct n; try discriminate.
114 rewrite eval_S in Heval. simplify_option_eq.
115 destruct ys. simplify_option_eq.
116 destruct n as [|[|n]]; try discriminate.
117 rewrite eval_S in Heqo. simplify_option_eq.
118 rewrite eval_S in Heqo1. simplify_option_eq.
119 exists (S (S (S (S n)))). rewrite eval_S. simplify_option_eq.
120 rewrite eval_value by lia. simplify_option_eq.
121 rewrite eval_S. simplify_option_eq.
122 rewrite eval_le with (n := S n) (v' := V_Attrset H0) by done || lia.
123 by simplify_option_eq.
124 - (* E_Select *)
125 exists (S n). rewrite eval_S. csimpl.
126 apply bind_Some. exists (V_Attrset (<[x := e0]>bs)).
127 destruct n; try discriminate. split; [done|].
128 apply bind_Some. exists (<[x := e0]>bs). split; [done|].
129 rewrite lookup_insert. by simplify_option_eq.
130 - (* E_SelectOr *)
131 destruct n; try discriminate.
132 rewrite eval_S in Heval. simplify_option_eq.
133 destruct n as [|[|n]]; try discriminate.
134 rewrite eval_S in Heqo. simplify_option_eq.
135 rewrite eval_S in Heqo0. simplify_option_eq.
136 exists (S (S (S n))). rewrite eval_S. simplify_option_eq.
137 rewrite eval_value by lia. simplify_option_eq.
138 case_match.
139 + rewrite bool_decide_eq_true in H. destruct H as [d Hd].
140 simplify_option_eq. rewrite eval_S in Heval. simplify_option_eq.
141 rewrite eval_S in Heqo. simplify_option_eq.
142 apply eval_le with (n := S n); done || lia.
143 + rewrite bool_decide_eq_false in H. apply eq_None_not_Some in H.
144 by simplify_option_eq.
145 - (* E_MSelectOr *)
146 destruct n; try discriminate.
147 rewrite eval_S in Heval. simplify_option_eq.
148 destruct ys. simplify_option_eq.
149 destruct n as [|[|n]]; try discriminate.
150 rewrite eval_S in Heqo. simplify_option_eq.
151 rewrite eval_S in Heqo0. simplify_option_eq.
152 exists (S (S (S n))). rewrite eval_S. simplify_option_eq.
153 rewrite eval_value by lia. simplify_option_eq.
154 case_match.
155 + rewrite bool_decide_eq_true in H. destruct H as [d Hd].
156 simplify_option_eq. rewrite eval_S in Heval. simplify_option_eq.
157 rewrite eval_S in Heqo. simplify_option_eq.
158 destruct n; try discriminate. rewrite eval_S in Heqo0.
159 simplify_option_eq. rewrite eval_S.
160 simplify_option_eq.
161 setoid_rewrite eval_le with (n := S n) (v' := V_Attrset H0); done || lia.
162 + rewrite bool_decide_eq_false in H. apply eq_None_not_Some in H.
163 by simplify_option_eq.
164 - (* E_Rec *)
165 exists (S n). rewrite eval_S. by csimpl.
166 - (* E_Let *)
167 exists (S n). rewrite eval_S. by csimpl.
168 - (* E_With *)
169 exists (S n). rewrite eval_S. csimpl.
170 apply bind_Some. exists (V_Attrset bs).
171 by destruct n; try discriminate.
172 - (* E_WithNoAttrset *)
173 exists (S n). rewrite eval_S. csimpl.
174 apply bind_Some. exists v1.
175 destruct v1; try by destruct n; try discriminate.
176 exfalso. apply H. by exists bs.
177 - (* E_ApplySimple *)
178 exists (S n). rewrite eval_S. simpl.
179 apply bind_Some. exists (V_Fn x e1).
180 split; [|assumption].
181 destruct n; try discriminate; reflexivity.
182 - (* E_ApplyAttrset *)
183 exists (S n). rewrite eval_S. csimpl.
184 apply bind_Some. exists (V_AttrsetFn m e0).
185 destruct n; try discriminate. split; [done|].
186 apply bind_Some. exists (V_Attrset bs). split; [done|].
187 apply bind_Some. exists bs. split; [done|].
188 apply bind_Some. apply matches_complete in H.
189 by exists bs'.
190 - (* E_ApplyFunctor *)
191 exists (S n). rewrite eval_S. csimpl.
192 apply bind_Some. exists (V_Attrset (<["__functor" := e2]>bs)).
193 destruct n; try discriminate. split; [done|].
194 rewrite lookup_insert. by simplify_option_eq.
195 - (* E_IfTrue *)
196 exists (S n). rewrite eval_S. csimpl.
197 apply bind_Some. exists true.
198 by destruct n; try discriminate.
199 - (* E_IfFalse *)
200 exists (S n). rewrite eval_S. csimpl.
201 apply bind_Some. exists false.
202 by destruct n; try discriminate.
203 - (* E_Op *)
204 exists (S n). rewrite eval_S. simpl.
205 apply bind_Some. exists v1.
206 destruct n; try discriminate.
207 split.
208 + apply eval_value. lia.
209 + apply bind_Some. exists v2. split.
210 * apply eval_value. lia.
211 * apply binop_eval_complete in H.
212 apply bind_Some. by exists u.
213 - (* E_OpHasAttrTrue *)
214 exists (S n). rewrite eval_S. csimpl.
215 apply bind_Some. exists (V_Attrset bs).
216 destruct n; try discriminate. rewrite eval_S in Heval.
217 simplify_option_eq. by rewrite bool_decide_eq_true_2.
218 - (* E_OpHasAttrFalse *)
219 exists (S n). rewrite eval_S. csimpl.
220 apply bind_Some. exists (V_Attrset bs).
221 destruct n; try discriminate. rewrite eval_S in Heval.
222 simplify_option_eq. rewrite eq_None_not_Some in H.
223 by rewrite bool_decide_eq_false_2.
224 - (* E_OpHasAttrNoAttrset *)
225 exists (S n). rewrite eval_S. csimpl.
226 destruct n; try discriminate. rewrite eval_S in Heval.
227 simplify_option_eq.
228 apply bind_Some. exists v.
229 split; [apply eval_value; lia|].
230 case_match; try done.
231 exfalso. apply H. by exists bs.
232 - (* E_Assert *)
233 exists (S n). rewrite eval_S. csimpl.
234 apply bind_Some. exists true.
235 split; [by destruct n | done].
236Qed.
237
238Lemma eval_step_ctx : ∀ e e' E uf_ext uf_int n v'',
239 is_ctx uf_ext uf_int E →
240 e -->base e' →
241 eval n uf_ext (E e') = Some v'' →
242 ∃ m, eval m uf_ext (E e) = Some v''.
243Proof.
244 intros e e' E uf_in uf_out n v'' Hctx Hbstep.
245 revert v''.
246 induction Hctx.
247 - intros. by apply eval_base_step with (e' := e') (n := n).
248 - inv H; intros.
249 + destruct n as [|n]; try discriminate.
250 rewrite eval_S in H. simplify_option_eq.
251 destruct xs. simplify_option_eq.
252 apply eval_le with (m := S n) in Heqo; try lia.
253 apply IHHctx in Heqo as [m He].
254 exists (S (n `max` m)).
255 rewrite eval_S. simplify_option_eq.
256 rewrite eval_le with (n := m) (v' := V_Attrset H1) by lia || done.
257 simplify_option_eq.
258 case_match; by rewrite eval_le with (n := n) (v' := v'') by lia || done.
259 + intros.
260 destruct n as [|n]; try discriminate.
261 rewrite eval_S in H. simplify_option_eq.
262 destruct xs. simplify_option_eq.
263 apply eval_le with (m := S n) in Heqo; try lia.
264 apply IHHctx in Heqo as [m He].
265 exists (S (n `max` m)).
266 rewrite eval_S. simplify_option_eq.
267 setoid_rewrite eval_le with (n := m); try lia || done.
268 simplify_option_eq. repeat case_match;
269 apply eval_le with (n := n); lia || done.
270 + intros.
271 destruct n as [|n]; try discriminate.
272 rewrite eval_S in H. simplify_option_eq.
273 apply eval_le with (m := S n) in Heqo; try lia.
274 apply IHHctx in Heqo as [m He].
275 exists (S (n `max` m)).
276 rewrite eval_S. simplify_option_eq.
277 setoid_rewrite eval_le with (n := m); try lia || done.
278 simplify_option_eq. repeat case_match;
279 apply eval_le with (n := n); lia || done.
280 + (* X_Apply *)
281 intros.
282 destruct n as [|n]; try discriminate.
283 rewrite eval_S in H. simplify_option_eq.
284 apply eval_le with (m := S n) in Heqo; try done || lia.
285 apply IHHctx in Heqo as [m He].
286 exists (S (n `max` m)).
287 rewrite eval_S. simplify_option_eq.
288 destruct H0; try discriminate.
289 * setoid_rewrite eval_le with (n := m); try done || lia.
290 simplify_option_eq.
291 setoid_rewrite eval_le with (n := n); done || lia.
292 * setoid_rewrite eval_le with (n := m); try done || lia.
293 simplify_option_eq.
294 rewrite eval_le with (n := n) at 1; try done || lia.
295 simplify_option_eq.
296 setoid_rewrite eval_le with (n := n); done || lia.
297 * setoid_rewrite eval_le with (n := m); try done || lia.
298 simplify_option_eq.
299 setoid_rewrite eval_le with (n := n); done || lia.
300 + intros.
301 destruct n as [|n]; try discriminate.
302 rewrite eval_S in H. simplify_option_eq.
303 destruct n; try discriminate. rewrite eval_S in Heqo.
304 simplify_option_eq.
305 apply eval_le with (m := S (S n)) in Heqo; try lia.
306 apply IHHctx in Heqo as [o He].
307 exists (S (S (n `max` o))).
308 rewrite eval_S. simplify_option_eq.
309 destruct o as [|o]; try discriminate.
310 setoid_rewrite eval_le with (n := S o) (v' := V_AttrsetFn m e1);
311 try done || lia.
312 simplify_option_eq.
313 rewrite eval_le with (n := S o) (v' := V_Attrset H1);
314 try by rewrite eval_S || lia.
315 simplify_option_eq.
316 rewrite eval_le with (n := S n) (v' := v''); done || lia.
317 + intros.
318 destruct n as [|n]; try discriminate.
319 rewrite eval_S in H. simplify_option_eq.
320 apply eval_le with (m := S n) in Heqo. 2: lia.
321 apply IHHctx in Heqo as [m He].
322 exists (S (n `max` m)).
323 rewrite eval_S. simplify_option_eq.
324 rewrite eval_le with (n := m) (v' := H1) by lia || done.
325 setoid_rewrite eval_le with (n := n) (v' := v''); try lia || done.
326 + intros.
327 destruct n as [|n]; try discriminate.
328 rewrite eval_S in H. simplify_option_eq.
329 apply eval_le with (m := S n) in Heqo. 2: lia.
330 apply IHHctx in Heqo as [m He].
331 exists (S (n `max` m)).
332 destruct H0; try discriminate.
333 rewrite eval_S. simplify_option_eq.
334 setoid_rewrite eval_le with (n := m) (v' := p); try lia || done.
335 simplify_option_eq. destruct p; try discriminate.
336 apply eval_le with (n := n); lia || done.
337 + intros.
338 destruct n as [|n]; try discriminate.
339 rewrite eval_S in H. simplify_option_eq.
340 apply eval_le with (m := S n) in Heqo. 2: lia.
341 apply IHHctx in Heqo as [m He].
342 exists (S (n `max` m)).
343 rewrite eval_S. simplify_option_eq.
344 rewrite eval_le with (n := n) (v' := H1) by lia || done.
345 rewrite eval_le with (n := m) (v' := H0) by lia || done.
346 simplify_option_eq.
347 apply eval_le with (n := n); lia || done.
348 + intros.
349 destruct n as [|n]; try discriminate.
350 rewrite eval_S in H. simplify_option_eq.
351 apply eval_le with (m := S n) in Heqo0. 2: lia.
352 apply IHHctx in Heqo0 as [m He].
353 exists (S (n `max` m)).
354 rewrite eval_S. simplify_option_eq.
355 rewrite eval_le with (n := m) (v' := H1) by lia || done.
356 rewrite eval_le with (n := n) (v' := H0) by lia || done.
357 simplify_option_eq.
358 apply eval_le with (n := n) (v' := v''); lia || done.
359 + (* IsCtxItem_OpHasAttrL *)
360 intros.
361 destruct n as [|n]; try discriminate.
362 rewrite eval_S in H. simplify_option_eq.
363 apply eval_le with (m := S n) in Heqo. 2: lia.
364 apply IHHctx in Heqo as [m He].
365 exists (S (n `max` m)).
366 rewrite eval_S. simplify_option_eq.
367 by rewrite eval_le with (n := m) (v' := H0) by lia || done.
368 + intros.
369 destruct n as [|n]; try discriminate.
370 rewrite eval_S in H. simplify_option_eq.
371 apply eval_le with (m := S n) in H. 2: lia.
372 apply IHHctx in H as [m He].
373 exists (S (n `max` m)).
374 rewrite eval_S; simplify_option_eq.
375 apply eval_le with (n := m) (v' := v''); lia || done.
376 + intros. simplify_option_eq.
377 destruct n as [|n]; try discriminate.
378 rewrite eval_S in H. simplify_option_eq.
379 apply map_mapM_Some_L in Heqo.
380 destruct (map_Forall2_destruct _ _ _ _ _ Heqo)
381 as [v' [m2' [Hkm2' HeqH0]]]. simplify_option_eq.
382 apply map_Forall2_insert_inv in Heqo as [Hinterp HForall2]; try done.
383 apply eval_le with (m := S n) in Hinterp; try lia.
384 apply IHHctx in Hinterp as [m Hinterp].
385 exists (S (n `max` m)).
386 rewrite eval_S. simplify_option_eq.
387 apply bind_Some. exists (<[x := v']> m2'). split; try done.
388 apply map_mapM_Some_L.
389 apply map_Forall2_insert_weak.
390 * apply eval_le with (n := m); lia || done.
391 * apply map_Forall2_impl_L
392 with (R1 := λ x y, eval n true x = Some y); try done.
393 intros u v Hjuv. by apply eval_le with (n := n); try lia.
394Qed.
395
396Lemma eval_step e e' v'' n :
397 e --> e' →
398 eval n false e' = Some v'' →
399 ∃ m, eval m false e = Some v''.
400Proof.
401 intros. inv H.
402 apply (eval_step_ctx e1 e2 E false uf_int n v'' H1 H2 H0).
403Qed.
404
405Theorem eval_complete e (v' : value) :
406 e -->* v' → ∃ n, eval n false e = Some v'.
407Proof.
408 intros [steps Hsteps] % rtc_nsteps. revert e v' Hsteps.
409 induction steps; intros e e' Hsteps; inv Hsteps.
410 - exists 1. apply eval_value. lia.
411 - destruct (IHsteps y e') as [n Hn]; try done.
412 clear IHsteps. by apply eval_step with (e := e) in Hn.
413Qed.
generated by cgit v1.2.3 (git 2.49.0) at 2025-11-01 23:03:20 +0000