aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.envrc1
-rw-r--r--.gitignore12
-rw-r--r--Makefile20
-rw-r--r--_CoqProject1
-rw-r--r--binop.v87
-rw-r--r--complete.v413
-rw-r--r--correct.v299
-rw-r--r--expr.v250
-rw-r--r--flake.lock61
-rw-r--r--flake.nix23
-rw-r--r--interpreter.v103
-rw-r--r--maptools.v476
-rw-r--r--matching.v609
-rw-r--r--relations.v73
-rw-r--r--sem.v167
-rw-r--r--semprop.v426
-rw-r--r--shared.v66
-rw-r--r--sound.v630
18 files changed, 3717 insertions, 0 deletions
diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
use flake
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..9e35ae7
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,12 @@
1*.aux
2*.glob
3*.vio
4*.vo
5*.vok
6*.vos
7.CoqMakefile.d
8.Makefile.coq.d
9.direnv
10.lia.cache
11Makefile.coq
12Makefile.coq.conf
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..1e32cef
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,20 @@
1# Modified from the Logical Foundations Makefile
2
3COQMFFLAGS := -Q . mininix
4
5ALLVFILES := maptools.v relations.v expr.v shared.v binop.v matching.v sem.v \
6 interpreter.v complete.v sound.v correct.v semprop.v
7
8build: Makefile.coq
9 $(MAKE) -f Makefile.coq
10
11clean::
12 if [ -e Makefile.coq ]; then $(MAKE) -f Makefile.coq cleanall; fi
13 $(RM) $(wildcard Makefile.coq Makefile.coq.conf)
14
15Makefile.coq:
16 coq_makefile $(COQMFFLAGS) -o Makefile.coq $(ALLVFILES)
17
18-include Makefile.coq
19
20.PHONY: build clean
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000..145dd21
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1 @@
-Q . mininix
diff --git a/binop.v b/binop.v
new file mode 100644
index 0000000..c8f87fd
--- /dev/null
+++ b/binop.v
@@ -0,0 +1,87 @@
1Require Import Coq.NArith.BinNat.
2Require Import Coq.Strings.Ascii.
3Require Import Coq.Strings.String.
4From stdpp Require Import fin_sets gmap option.
5From mininix Require Import expr maptools shared.
6
7Open Scope string_scope.
8Open Scope N_scope.
9Open Scope Z_scope.
10Open Scope nat_scope.
11
12Definition right_union {A} (bs1 bs2 : gmap string A) : gmap string A :=
13 bs2 ∪ bs1.
14
15Variant binop_r : op → value → value → value → Prop :=
16 | Bo_PlusInt n1 n2 : binop_r O_Plus (V_Int n1) (V_Int n2) (V_Int (n1 + n2))
17 | Bo_PlusStr s1 s2 : binop_r O_Plus (V_Str s1) (V_Str s2) (V_Str (s1 ++ s2))
18 | Bo_MinInt n1 n2 : binop_r O_Min (V_Int n1) (V_Int n2) (V_Int (n1 - n2))
19 | Bo_UpdAttrset bs1 bs2 :
20 binop_r O_Upd (V_Attrset bs1) (V_Attrset bs2)
21 (V_Attrset (right_union bs1 bs2))
22 | Bo_Eq v1 v2 : binop_r O_Eq v1 v2 (expr_eq v1 v2)
23 | Bo_DivInt (n1 n2 : Z) : n2 ≠ 0%Z → binop_r O_Div n1 n2 (n1 / n2)%Z
24 | Bo_LtInt (n1 n2 : Z) : binop_r O_Lt n1 n2 (bool_decide (n1 < n2)%Z)
25 | Bo_LtStr s1 s2 : binop_r O_Lt (V_Str s1) (V_Str s2) (string_lt s1 s2).
26
27Notation "u1 '⟦' op '⟧' u2 '-⊚->' v" := (binop_r op u1 u2 v) (at level 55).
28
29Definition binop_eval (op : op) (v1 v2 : value) : option value :=
30 match op with
31 | O_Plus =>
32 match v1, v2 with
33 | V_Int n1, V_Int n2 => Some (V_Int (n1 + n2))
34 | V_Str s1, V_Str s2 => Some (V_Str (s1 ++ s2))
35 | _, _ => None
36 end
37 | O_Min =>
38 match v1, v2 with
39 | V_Int n1, V_Int n2 => Some (V_Int (n1 - n2))
40 | _, _ => None
41 end
42 | O_Upd =>
43 match v1, v2 with
44 | V_Attrset bs1, V_Attrset bs2 =>
45 Some (V_Attrset (right_union bs1 bs2))
46 | _, _ => None
47 end
48 | O_Eq => Some (V_Bool (expr_eq (X_V v1) (X_V v2)))
49 | O_Div =>
50 match v1, v2 with
51 | V_Int n1, V_Int n2 =>
52 if decide (n2 = 0)%Z
53 then None
54 else Some (V_Int (n1 / n2)%Z)
55 | _, _ => None
56 end
57 | O_Lt =>
58 match v1, v2 with
59 | V_Int n1, V_Int n2 => Some (V_Bool (bool_decide (n1 < n2)%Z))
60 | V_Str s1, V_Str s2 => Some (V_Bool (string_lt s1 s2))
61 | _, _ => None
62 end
63 end.
64
65Theorem binop_eval_sound op u1 u2 v :
66 binop_eval op u1 u2 = Some v → binop_r op u1 u2 v.
67Proof.
68 intros Heval.
69 destruct op, u1, u2; try discriminate; simplify_eq/=; try constructor.
70 destruct (decide (n0 = 0)%Z); try discriminate.
71 simplify_eq/=. by constructor.
72Qed.
73
74Theorem binop_eval_complete op u1 u2 v :
75 binop_r op u1 u2 v → binop_eval op u1 u2 = Some v.
76Proof.
77 intros Heval. inv Heval; try done.
78 unfold binop_eval. by apply decide_False.
79Qed.
80
81Theorem binop_deterministic op u1 u2 v1 v2 :
82 u1 ⟦op⟧ u2 -⊚-> v1 → u1 ⟦op⟧ u2 -⊚-> v2 → v1 = v2.
83Proof.
84 intros Heval1 Heval2.
85 apply binop_eval_complete in Heval1, Heval2.
86 congruence.
87Qed.
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.
diff --git a/correct.v b/correct.v
new file mode 100644
index 0000000..89f5894
--- /dev/null
+++ b/correct.v
@@ -0,0 +1,299 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import gmap.
3From mininix Require Import
4 expr relations sem interpreter complete sound shared.
5
6Theorem correct e v' : (∃ n, eval n false e = Some v') ↔ e -->* v'.
7Proof.
8 split.
9 - intros [n Heval]. by apply (eval_sound_strong n false).
10 - intros Heval. by apply eval_complete.
11Qed.
12
13(* Top-level program reduction/evaluation:
14 we make the prelude available here. *)
15
16Definition with_prelude (e : expr) : expr :=
17 subst (closed prelude) e.
18
19Definition tl_reds (e e' : expr) :=
20 with_prelude e -->* e'.
21
22Definition tl_eval (n : nat) (e : expr) : option value :=
23 eval n false (subst (closed prelude) e).
24
25Definition tl_evals e e' := ∃ n, tl_eval n e = Some e'.
26
27(* Macros *)
28
29Definition μ_neq e1 e2 := X_Cond (X_Op O_Eq e1 e2) false true.
30Definition μ_or e1 e2 := X_Cond e1 true e2.
31Definition μ_and e1 e2 := X_Cond e1 e2 false.
32Definition μ_impl e1 e2 := X_Cond e1 e2 true.
33Definition μ_neg e := X_Cond e false true.
34
35Definition μ_le n m := μ_or (X_Op O_Eq n m) (X_Op O_Lt n m).
36Definition μ_gt n m := X_Op O_Lt m n.
37Definition μ_ge n m := μ_or (X_Op O_Eq n m) (μ_gt n m).
38
39(* Tests/examples *)
40
41Definition ex1 := X_LetBinding {[ "a" := B_Rec 1%Z ]} "a".
42
43(* [let a = 1; in a] gives 1 *)
44Theorem ex1_step : tl_reds ex1 1%Z.
45Proof.
46 unfold ex1.
47 eapply rtc_l.
48 - by eapply E_Ctx with (E := id).
49 - simplify_option_eq.
50 eapply rtc_once.
51 by eapply E_Ctx with (E := id).
52Qed.
53
54Example ex1_eval : tl_evals ex1 (V_Int 1).
55Proof. by exists 3. Qed.
56
57(* Definition ex2 := <{ let a = 1 in with { a = 2 }; a }>. *)
58Definition ex2 := X_LetBinding {[ "a" := B_Rec 1%Z ]}
59 (X_Incl (V_Attrset {[ "a" := X_V 2%Z ]}) "a").
60
61(* [let a = 1; in with { a = 2; }; a] gives 1 *)
62Theorem ex2_step : tl_reds ex2 1%Z.
63Proof.
64 unfold ex2.
65 eapply rtc_l.
66 - by eapply E_Ctx with (E := id).
67 - simplify_option_eq.
68 eapply rtc_l.
69 + by eapply E_Ctx with (E := id).
70 + simpl. eapply rtc_once.
71 by eapply E_Ctx with (E := id).
72Qed.
73
74Example ex2_eval : tl_evals ex2 (V_Int 1).
75Proof. by exists 4. Qed.
76
77(* [with { a = 1; }; with { a = 2; }; a] gives 2 *)
78Definition ex3 :=
79 X_Incl (V_Attrset {[ "a" := X_V 1%Z ]})
80 (X_Incl (V_Attrset {[ "a" := X_V 2%Z ]}) "a").
81
82Theorem ex3_step : tl_reds ex3 2%Z.
83Proof.
84 unfold ex3.
85 eapply rtc_l.
86 - eapply E_Ctx with (E := id); [done | apply E_With].
87 - simpl. eapply rtc_l.
88 + by eapply E_Ctx with (E := id).
89 + simplify_option_eq.
90 eapply rtc_once.
91 by eapply E_Ctx with (E := id).
92Qed.
93
94Example ex3_eval : tl_evals ex3 (V_Int 2).
95Proof. by exists 4. Qed.
96
97(* [({ x, y ? x } : y) { x = 1; }] gives 1 *)
98Definition ex4 :=
99 X_Apply
100 (V_AttrsetFn
101 (M_Matcher
102 {[ "x" := M_Mandatory;
103 "y" := M_Optional "x"
104 ]}
105 true)
106 "y")
107 (V_Attrset {[ "x" := X_V 1%Z ]}).
108
109Example ex4_eval : tl_evals ex4 (V_Int 1).
110Proof. by exists 7. Qed.
111
112(* [({ x ? y, y ? x } : y) { x = 1; }] gives 1 *)
113Definition ex5 :=
114 X_Apply
115 (V_AttrsetFn
116 (M_Matcher
117 {[ "x" := M_Optional "y";
118 "y" := M_Optional "x"
119 ]}
120 true)
121 "y")
122 (V_Attrset {[ "x" := X_V 1%Z ]}).
123
124Example ex5_eval : tl_evals ex5 (V_Int 1).
125Proof. by exists 7. Qed.
126
127(* [let binToString = n:
128 if n == 0
129 then "0"
130 else if n == 1
131 then "1"
132 else binToString (n / 2) + (if isEven n then "0" else "1");
133 isEven = n: n != 1 && (n = 0 || isEven (n - 2));
134 test = { x, y ? attrs.x, ... } @ attrs:
135 "x: " + x + ", y: " + y + ", z: " + attrs.z or "(no z)"
136 in test { x = binToString 6; }] gives "x: 110, y: 110, z: (no z)" *)
137Definition ex6 :=
138 X_LetBinding
139 {[ "binToString" := B_Rec $ V_Fn "n" $
140 X_Cond
141 (X_Op O_Eq "n" 0%Z)
142 (V_Str "0")
143 (X_Cond
144 (X_Op O_Eq "n" 1%Z)
145 (V_Str "1")
146 (X_Op O_Plus
147 (X_Apply
148 "binToString"
149 (X_Op O_Div "n" 2%Z))
150 (X_Cond
151 (X_Apply "isEven" "n")
152 (V_Str "0")
153 (V_Str "1"))));
154 "isEven" := B_Rec $ V_Fn "n" $
155 μ_and
156 (μ_neq "n" 1%Z)
157 (μ_or
158 (X_Op O_Eq "n" 0%Z)
159 (X_Apply "isEven" (X_Op O_Min "n" 2%Z)));
160 "test" := B_Rec $ V_Fn "attrs" $
161 X_Apply
162 (V_AttrsetFn
163 (M_Matcher
164 {[ "x" := M_Mandatory;
165 "y" := M_Optional
166 (X_Select "attrs"
167 (nonempty_singleton "x"))
168 ]} false)
169 (X_Op O_Plus
170 (X_Op O_Plus
171 (X_Op O_Plus
172 (X_Op O_Plus
173 (X_Op O_Plus
174 (V_Str "x: ")
175 "x")
176 (V_Str ", y: "))
177 "y")
178 (V_Str ", z: "))
179 (X_SelectOr
180 "attrs"
181 (nonempty_singleton "z")
182 (V_Str "(no z)"))))
183 "attrs"
184 ]}
185 (X_Apply "test" $ V_Attrset
186 {[ "x" := X_Apply "binToString" 6%Z ]}).
187
188Example ex6_eval : tl_evals ex6 (V_Str "x: 110, y: 110, z: (no z)").
189Proof. by exists 37. Qed.
190
191(* Important check of if placeholders work correctly:
192 [with { x = 1; }; let foo = y: let x = 2; in y; foo x]
193 gives 1 *)
194Definition ex7 := X_Incl
195 (V_Attrset {[ "x" := X_V 1%Z ]})
196 (X_LetBinding
197 {[ "foo" := B_Rec $ V_Fn "y" $
198 X_LetBinding {[ "x" := B_Rec 2%Z ]} "y"
199 ]}
200 (X_Apply "foo" "x")).
201
202Example ex7_eval : tl_evals ex7 (V_Int 1).
203Proof. by exists 7. Qed.
204
205Definition ex8 :=
206 X_LetBinding
207 {[ "divide" := B_Rec $ V_Fn "a" $ V_Fn "b" $
208 X_Assert
209 (μ_and (μ_ge "a" 0%Z) (μ_gt "b" 0%Z))
210 (X_Cond
211 (X_Op O_Lt "a" "b")
212 0
213 (X_Op
214 O_Plus
215 (X_Apply
216 (X_Apply
217 "divide"
218 (X_Op O_Min "a" "b"))
219 "b")
220 1));
221 "divider" := B_Rec $ X_Attrset
222 {[ "__functor" := B_Nonrec $ V_Fn "self" $ V_Fn "x" $
223 X_Op
224 O_Upd
225 "self"
226 (X_Attrset
227 {[ "value" := B_Nonrec $
228 X_Apply
229 (X_Apply
230 "divide"
231 (X_Select "self" $ nonempty_singleton "value"))
232 "x"
233 ]})
234 ]};
235 "mkDivider" := B_Rec $ V_Fn "value" $
236 X_Op
237 O_Upd
238 "divider"
239 (X_Attrset {[ "value" := B_Nonrec "value" ]})
240 ]}%Z
241 (X_Select
242 (X_Apply (X_Apply (X_Apply "mkDivider" 100) 5) 4)
243 (nonempty_singleton "value"))%Z.
244
245Example ex8_eval : tl_evals ex8 (V_Int 5).
246Proof. by exists 170. Qed.
247
248Example ex9 :=
249 X_Apply
250 (X_Apply
251 (V_Attrset
252 {[ "__functor" := X_V $ V_Fn "self" $ V_Fn "f" $
253 X_Apply "f" (X_Apply "self" "f")
254 ]})
255 (V_Fn "go" $ V_Fn "n" $
256 X_Cond
257 (μ_le "n" 1)
258 "n"
259 (X_Op
260 O_Plus
261 (X_Apply "go" (X_Op O_Min "n" 1))
262 (X_Apply "go" (X_Op O_Min "n" 2)))))%Z
263 15%Z.
264
265Example ex9_eval : tl_evals ex9 (V_Int 610).
266Proof. by exists 78. Qed.
267
268Example ex10 :=
269 X_LetBinding
270 {[ "true" := B_Rec 42 ]}%Z
271 (X_Op O_Eq "true" 42)%Z.
272
273Example ex10_eval : tl_evals ex10 (V_Bool true).
274Proof. by exists 4. Qed.
275
276Definition ex11 :=
277 X_LetBinding
278 {[ "x" := B_Rec "y" ]}%Z
279 (X_LetBinding {[ "y" := B_Rec 10 ]} "x")%Z.
280
281Example ex11_eval : tl_eval 1000 ex11 = None.
282Proof. done. Qed.
283
284Definition ex12 :=
285 X_LetBinding
286 {[ "pkgs" := B_Rec $ V_Attrset
287 {[ "x" := X_Incl (V_Attrset {[ "y" := X_V 1%Z ]}) "y" ]}
288 ]}
289 (X_Select
290 (X_Attrset
291 {[ "x" := B_Rec $ X_Select "pkgs" (nonempty_singleton "x");
292 "y" := B_Rec 3%Z
293 ]})
294 (nonempty_singleton "x")).
295
296Example ex12_eval : tl_eval 1000 ex12 = Some (V_Int 1).
297Proof. done. Qed.
298
299(* Aio, quantitas magna frumentorum est. *)
diff --git a/expr.v b/expr.v
new file mode 100644
index 0000000..11c0737
--- /dev/null
+++ b/expr.v
@@ -0,0 +1,250 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import gmap.
3
4(* The Nix Expression Language *)
5
6(** Selected operators from Dolsta and Löh, 2008. Newer definitions at
7 https://nixos.org/manual/nix/stable/language/operators *)
8Variant op : Type :=
9 | O_Eq (* = *)
10 | O_Lt (* < *)
11 | O_Plus (* + *)
12 | O_Min (* - *)
13 | O_Div (* / *)
14 | O_Upd. (* // *)
15
16Hint Constructors op : core.
17
18Variant nonempty A := Ne_Cons (head : A) (tail : list A).
19Arguments Ne_Cons {A} _ _.
20Hint Constructors nonempty : core.
21
22Inductive expr : Type :=
23 | X_V (v : value) (* v *)
24 | X_Id (x : string) (* x *)
25 | X_Attrset (bs : gmap string b_rhs) (* { bᵣ* } *)
26 | X_LetBinding (bs : gmap string b_rhs) (e : expr) (* let bᵣ* in e *)
27 | X_Select (e : expr) (xs : nonempty string) (* e.xs *)
28 | X_SelectOr (e : expr) (xs : nonempty string) (or : expr) (* e.xs or e *)
29 | X_Apply (e1 e2 : expr) (* e1 e2 *)
30 | X_Cond (e1 e2 e3 : expr) (* if e1 then e2 else e3 *)
31 | X_Incl (e1 e2 : expr) (* with e1; e2 *)
32 | X_Assert (e1 e2 : expr) (* assert e1; e2 *)
33 | X_Op (op : op) (e1 e2 : expr) (* e1 <op> e2 *)
34 | X_HasAttr (e1 : expr) (x : string) (* e ? x *)
35 | X_Force (e : expr) (* force e *)
36 | X_Closed (e : expr) (* closed(e) *)
37 | X_Placeholder (x : string) (e : expr) (* placeholderₓ(e) *)
38with b_rhs :=
39 | B_Rec (e : expr) (* := e *)
40 | B_Nonrec (e : expr) (* :=ᵣ e *)
41with matcher :=
42 | M_Matcher (ms : gmap string m_rhs) (strict : bool)
43with m_rhs :=
44 | M_Mandatory
45 | M_Optional (e : expr) (* ? e *)
46with value :=
47 | V_Bool (p : bool) : value (* true | false *)
48 | V_Null : value (* null *)
49 | V_Int (n : Z) : value (* n *)
50 | V_Str (s : string) : value (* s *)
51 | V_Fn (x : string) (e : expr) : value (* x: e *)
52 | V_AttrsetFn (m : matcher) (e : expr) : value (* { m }: e *)
53 | V_Attrset (bs : gmap string expr) : value. (* { b* } *)
54
55Hint Constructors expr : core.
56
57Instance Maybe_X_Attrset : Maybe X_Attrset := λ e,
58 match e with
59 | X_Attrset bs => Some bs
60 | _ => None
61 end.
62
63Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs,
64 match rhs with
65 | B_Nonrec e => Some e
66 | _ => None
67 end.
68
69Instance Maybe_B_Rec : Maybe B_Rec := λ rhs,
70 match rhs with
71 | B_Rec e => Some e
72 | _ => None
73 end.
74
75Lemma maybe_b_rhs_excl b :
76 is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b) → False.
77Proof. intros [e2 Hnonrec] [e1 Hrec]. simplify_option_eq. Qed.
78
79Lemma no_b_nonrec__b_rec b :
80 ¬ is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b).
81Proof.
82 destruct b; try by eauto.
83 simplify_eq/=. intros contra. apply is_Some_alt. eauto.
84Qed.
85
86Lemma no_b_rec__b_nonrec b :
87 ¬ is_Some (maybe B_Rec b) → is_Some (maybe B_Nonrec b).
88Proof.
89 destruct b; try by eauto.
90 simplify_eq/=. intros contra. apply is_Some_alt. eauto.
91Qed.
92
93Instance Maybe_V_Attrset : Maybe V_Attrset := λ e,
94 match e with
95 | V_Attrset bs => Some bs
96 | _ => None
97 end.
98
99Instance Maybe_V_Bool : Maybe V_Bool := λ e,
100 match e with
101 | V_Bool p => Some p
102 | _ => None
103 end.
104
105Global Instance B_Nonrec_inj : Inj (=) (=) B_Nonrec.
106Proof. intros [] [] ?; by simplify_eq. Qed.
107
108Definition matcher_keys (m : matcher) : gset string :=
109 match m with M_Matcher ms _ => dom ms end.
110
111Definition matcher_map (f : expr → expr) (m : matcher) : matcher :=
112 let map_m_rhs := λ rhs,
113 match rhs with
114 | M_Optional e => M_Optional (f e)
115 | _ => rhs
116 end in
117 match m with
118 | M_Matcher ms strict => M_Matcher (map_m_rhs <$> ms) strict
119 end.
120
121Local Definition map_delete_all {K V} `{Countable K}
122 (ks : gset K) (m : gmap K V) : gmap K V :=
123 set_fold (λ k m', map_delete k m') m ks.
124
125Local Definition b_rhs_map (f g : expr → expr) (rhs : b_rhs) : b_rhs :=
126 match rhs with
127 | B_Rec e => B_Rec (f e)
128 | B_Nonrec e => B_Nonrec (g e)
129 end.
130
131(* See Dolstra (2006), §4.3.3 and fig. 4.6 (p. 75, PDF: p. 83) *)
132Fixpoint subst (subs : gmap string expr) (e : expr) : expr :=
133 let msubst subs' := b_rhs_map (subst subs') (subst subs) in
134 match e with
135 | X_V V_Null | X_V (V_Bool _) | X_V (V_Str _) | X_V (V_Int _) => e
136 | X_Id x | X_Placeholder x _ => default e (subs !! x)
137 | X_Attrset bs =>
138 let subs' := map_delete_all (dom bs) subs in
139 X_Attrset (msubst subs' <$> bs)
140 | X_V (V_Attrset bs) =>
141 X_V (V_Attrset (subst subs <$> bs))
142 | X_LetBinding bs e' =>
143 let subs' := map_delete_all (dom bs) subs in
144 X_LetBinding (msubst subs' <$> bs) (subst subs' e')
145 | X_Select e' x => X_Select (subst subs e') x
146 | X_SelectOr e' x or => X_SelectOr (subst subs e') x (subst subs or)
147 | X_V (V_Fn x e') =>
148 let subs' := map_delete x subs in
149 X_V (V_Fn x (subst subs' e'))
150 | X_V (V_AttrsetFn (M_Matcher ms _ as m) e') =>
151 let subs' := map_delete_all (matcher_keys m) subs in
152 X_V (V_AttrsetFn (matcher_map (subst subs') m) (subst subs' e'))
153 | X_Apply e1 e2 => X_Apply (subst subs e1) (subst subs e2)
154 | X_Cond e1 e2 e3 => X_Cond (subst subs e1) (subst subs e2) (subst subs e3)
155 | X_Incl e1 e2 => X_Incl (subst subs e1) (subst subs e2)
156 | X_Op op e1 e2 => X_Op op (subst subs e1) (subst subs e2)
157 | X_HasAttr e x => X_HasAttr (subst subs e) x
158 | X_Assert e1 e2 => X_Assert (subst subs e1) (subst subs e2)
159 | X_Closed e => X_Closed e
160 | X_Force e => X_Force (subst subs e)
161 end.
162
163Definition closed (bs : gmap string expr) : gmap string expr :=
164 X_Closed <$> bs.
165
166Definition placeholders (bs : gmap string expr) : gmap string expr :=
167 map_imap (λ (x : string) (e : expr), Some (X_Placeholder x e)) bs.
168
169Definition nonempty_singleton {A} (a : A): nonempty A := Ne_Cons a nil.
170
171Definition nonempty_cons {A} (a : A) (l : nonempty A) : nonempty A :=
172 match l with Ne_Cons head tail => Ne_Cons a (head :: tail) end.
173
174Definition indirect (bs : gmap string b_rhs) : gmap string expr :=
175 map_imap (λ (x : string) (rhs : b_rhs),
176 Some (X_Select (X_Attrset bs) (nonempty_singleton x))) bs.
177
178Definition rec_subst (bs : gmap string b_rhs) : gmap string expr :=
179 let subs := indirect bs
180 in (λ b, match b with
181 | B_Rec e => subst (closed subs) e
182 | B_Nonrec e => e
183 end) <$> bs.
184
185Inductive strong_value : Type :=
186 | SV_Bool (b : bool)
187 | SV_Null
188 | SV_Int (n : Z)
189 | SV_Str (s : string)
190 | SV_Fn (x : string) (e : expr)
191 | SV_AttrsetFn (m : matcher) (e : expr)
192 | SV_Attrset (bs : gmap string strong_value).
193
194Fixpoint value_from_strong_value (sv : strong_value) : value :=
195 match sv with
196 | SV_Null => V_Null
197 | SV_Bool b => V_Bool b
198 | SV_Int n => V_Int n
199 | SV_Str s => V_Str s
200 | SV_Fn x e => V_Fn x e
201 | SV_AttrsetFn m e => V_AttrsetFn m e
202 | SV_Attrset bs => V_Attrset (X_V ∘ value_from_strong_value <$> bs)
203 end.
204
205Global Instance X_V_inj : Inj (=) (=) X_V.
206Proof. intros [] [] ?; by simplify_eq. Qed.
207
208Definition expr_from_strong_value : strong_value → expr :=
209 X_V ∘ value_from_strong_value.
210
211(* Based on the fin_maps test from stdpp *)
212Fixpoint sv_size (sv : strong_value) : nat :=
213 match sv with
214 | SV_Null | SV_Bool _ | SV_Int _ | SV_Str _
215 | SV_Fn _ _ | SV_AttrsetFn _ _ => 1
216 | SV_Attrset bs => S (map_fold (λ _ sv', plus (sv_size sv')) 0 bs)
217 end.
218
219(* Based on the fin_maps test from stdpp *)
220Lemma strong_value_ind' :
221 ∀ P : strong_value → Prop,
222 P SV_Null →
223 (∀ b : bool, P (SV_Bool b)) →
224 (∀ n : Z, P (SV_Int n)) →
225 (∀ s : string, P (SV_Str s)) →
226 (∀ (x : string) (e : expr), P (SV_Fn x e)) →
227 (∀ (m : matcher) (e : expr), P (SV_AttrsetFn m e)) →
228 (∀ bs : gmap string strong_value,
229 map_Forall (λ i, P) bs → P (SV_Attrset bs)) →
230 ∀ s : strong_value, P s.
231Proof.
232 intros P PNull PBool PInt PStr PFn PAttrsetFn PAttrset sv.
233 remember (sv_size sv) as n eqn:Hn. revert sv Hn.
234 induction (lt_wf n) as [n _ IH]; intros [| | | | | | bs] ->; simpl in *; try done.
235 apply PAttrset. revert bs IH.
236 apply (map_fold_ind (λ r bs, (∀ n', n' < S r → _) → map_Forall (λ _, P) bs)).
237 - intros IH. apply map_Forall_empty.
238 - intros k sv bs r ? IHbs IHsv. apply map_Forall_insert; [done|]. split.
239 + eapply IHsv; [|done]; lia.
240 + eapply IHbs. intros; eapply IHsv; [|done]; lia.
241Qed.
242
243Coercion X_Id : string >-> expr.
244Coercion V_Int : Z >-> value.
245(* Leaving this out for now: would conflict with X_Id and
246 therefore cause ambiguity *)
247(* Coercion X_StrVal : string >-> expr. *)
248Coercion V_Bool : bool >-> value.
249Coercion X_V : value >-> expr.
250Coercion value_from_strong_value : strong_value >-> value.
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..82ae26f
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,61 @@
1{
2 "nodes": {
3 "flake-utils": {
4 "inputs": {
5 "systems": "systems"
6 },
7 "locked": {
8 "lastModified": 1710146030,
9 "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
10 "owner": "numtide",
11 "repo": "flake-utils",
12 "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
13 "type": "github"
14 },
15 "original": {
16 "owner": "numtide",
17 "repo": "flake-utils",
18 "type": "github"
19 }
20 },
21 "nixpkgs": {
22 "locked": {
23 "lastModified": 1719253556,
24 "narHash": "sha256-A/76RFUVxZ/7Y8+OMVL1Lc8LRhBxZ8ZE2bpMnvZ1VpY=",
25 "owner": "NixOS",
26 "repo": "nixpkgs",
27 "rev": "fc07dc3bdf2956ddd64f24612ea7fc894933eb2e",
28 "type": "github"
29 },
30 "original": {
31 "owner": "NixOS",
32 "ref": "nixos-24.05",
33 "repo": "nixpkgs",
34 "type": "github"
35 }
36 },
37 "root": {
38 "inputs": {
39 "flake-utils": "flake-utils",
40 "nixpkgs": "nixpkgs"
41 }
42 },
43 "systems": {
44 "locked": {
45 "lastModified": 1681028828,
46 "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
47 "owner": "nix-systems",
48 "repo": "default",
49 "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
50 "type": "github"
51 },
52 "original": {
53 "owner": "nix-systems",
54 "repo": "default",
55 "type": "github"
56 }
57 }
58 },
59 "root": "root",
60 "version": 7
61}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..e9c35a4
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,23 @@
1{
2 inputs = {
3 nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.05";
4 flake-utils.url = "github:numtide/flake-utils";
5 };
6
7 outputs = { self, nixpkgs, flake-utils, ... }:
8 flake-utils.lib.eachDefaultSystem (system:
9 let
10 pkgs = import nixpkgs { inherit system; };
11 in
12 {
13 devShells.default = with pkgs; mkShell {
14 buildInputs = [
15 coqPackages.coqide
16 coqPackages.stdpp
17 coq
18 ];
19 };
20
21 formatter = pkgs.nixpkgs-fmt;
22 });
23}
diff --git a/interpreter.v b/interpreter.v
new file mode 100644
index 0000000..c701b42
--- /dev/null
+++ b/interpreter.v
@@ -0,0 +1,103 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import fin_maps.
3From mininix Require Import binop expr maptools matching.
4
5Open Scope string_scope.
6
7Definition eval1 (go : bool → expr → option value)
8 (uf : bool) (d : expr) : option value :=
9 match d with
10 | X_Id _ => None
11 | X_Force e => go true e
12 | X_Closed e => go uf e
13 | X_Placeholder x e => go uf e
14 | X_V (V_Attrset bs) =>
15 if uf
16 then vs' ← map_mapM (go true) bs;
17 Some (V_Attrset (X_V <$> vs'))
18 else Some (V_Attrset bs)
19 | X_V v => Some v
20 | X_Attrset bs => go uf (V_Attrset (rec_subst bs))
21 | X_LetBinding bs e =>
22 let e' := subst (closed (rec_subst bs)) e
23 in go uf e'
24 | X_Select e (Ne_Cons x ys) =>
25 v' ← go false e;
26 bs ← maybe V_Attrset v';
27 e'' ← bs !! x;
28 match ys with
29 | [] => go uf e''
30 | y :: ys => go uf (X_Select e'' (Ne_Cons y ys))
31 end
32 | X_SelectOr e (Ne_Cons x ys) or =>
33 v' ← go false e;
34 bs ← maybe V_Attrset v';
35 match bs !! x with
36 | Some e'' =>
37 match ys with
38 | [] => go uf e''
39 | y :: ys => go uf (X_SelectOr e'' (Ne_Cons y ys) or)
40 end
41 | None => go uf or
42 end
43 | X_Apply e1 e2 =>
44 v1' ← go false e1;
45 match v1' with
46 | V_Fn x e =>
47 let e' := subst {[x := X_Closed e2]} e
48 in go uf e'
49 | V_AttrsetFn m e =>
50 v2' ← go false e2;
51 bs ← maybe V_Attrset v2';
52 bs' ← matches m bs;
53 go uf (X_LetBinding bs' e)
54 | V_Attrset bs =>
55 f ← bs !! "__functor";
56 go uf (X_Apply (X_Apply f (V_Attrset bs)) e2)
57 | _ => None
58 end
59 | X_Cond e1 e2 e3 =>
60 v1' ← go false e1;
61 b ← maybe V_Bool v1';
62 go uf (if b : bool then e2 else e3)
63 | X_Incl e1 e2 =>
64 v1' ← go false e1;
65 match v1' with
66 | V_Attrset bs => go uf (subst (placeholders bs) e2)
67 | _ => go uf e2
68 end
69 | X_Op op e1 e2 =>
70 e1' ← go false e1;
71 e2' ← go false e2;
72 v' ← binop_eval op e1' e2';
73 go uf (X_V v')
74 | X_HasAttr e x =>
75 v' ← go false e;
76 Some $ V_Bool $
77 match v' with
78 | V_Attrset bs =>
79 bool_decide (is_Some (bs !! x))
80 | _ => false
81 end
82 | X_Assert e1 e2 =>
83 v1' ← go false e1;
84 match v1' with
85 | V_Bool true => go uf e2
86 | _ => None
87 end
88 end.
89
90Fixpoint eval (n : nat) (uf : bool) (e : expr) : option value :=
91 match n with
92 | O => None
93 | S n => eval1 (eval n) uf e
94 end.
95
96(* Don't automatically 'simplify' eval: this can lead to very complicated
97 assumptions and goals. Instead, we define our own lemma which can be used
98 to unfold eval once. This allows us to write proofs in a much more
99 controlled manner, and we can still leverage tactics like simplify_option_eq
100 without everything blowing up uncontrollably *)
101Global Opaque eval.
102Lemma eval_S n : eval (S n) = eval1 (eval n).
103Proof. done. Qed.
diff --git a/maptools.v b/maptools.v
new file mode 100644
index 0000000..2478430
--- /dev/null
+++ b/maptools.v
@@ -0,0 +1,476 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import countable fin_maps fin_map_dom.
3
4(** Generic lemmas for finite maps and their domains *)
5
6Lemma map_insert_empty_lookup {A} `{FinMap K M}
7 (i j : K) (u v : A) :
8 <[i := u]> (∅ : M A) !! j = Some v → i = j ∧ v = u.
9Proof.
10 intros Hiel.
11 destruct (decide (i = j)).
12 - split; try done. simplify_eq /=.
13 rewrite lookup_insert in Hiel. congruence.
14 - rewrite lookup_insert_ne in Hiel; try done.
15 exfalso. eapply lookup_empty_Some, Hiel.
16Qed.
17
18Lemma map_insert_ne_inv `{FinMap K M} {A}
19 (m1 m2 : M A) i j x y :
20 i ≠ j →
21 <[i := x]>m1 = <[j := y]>m2 →
22 m2 !! i = Some x ∧ m1 !! j = Some y ∧
23 delete i (delete j m1) = delete i (delete j m2).
24Proof.
25 intros Hneq Heq.
26 split; try split.
27 - rewrite <-lookup_delete_ne with (i := j) by congruence.
28 rewrite <-delete_insert_delete with (x := y).
29 rewrite <-Heq.
30 rewrite lookup_delete_ne by congruence.
31 by rewrite lookup_insert.
32 - rewrite <-lookup_delete_ne with (i := i) by congruence.
33 rewrite <-delete_insert_delete with (x := x).
34 rewrite Heq.
35 rewrite lookup_delete_ne by congruence.
36 by rewrite lookup_insert.
37 - setoid_rewrite <-delete_insert_delete with (x := x) at 1.
38 setoid_rewrite <-delete_insert_delete with (x := y) at 4.
39 rewrite <-delete_insert_ne by congruence.
40 by do 2 f_equal.
41Qed.
42
43Lemma map_insert_inv `{FinMap K M} {A}
44 (m1 m2 : M A) i x y :
45 <[i := x]>m1 = <[i := y]>m2 →
46 x = y ∧ delete i m1 = delete i m2.
47Proof.
48 intros Heq.
49 split; try split.
50 - apply Some_inj.
51 replace (Some x) with (<[i := x]>m1 !! i) by apply lookup_insert.
52 replace (Some y) with (<[i := y]>m2 !! i) by apply lookup_insert.
53 by rewrite Heq.
54 - replace (delete i m1) with (delete i (<[i := x]>m1))
55 by apply delete_insert_delete.
56 replace (delete i m2) with (delete i (<[i := y]>m2))
57 by apply delete_insert_delete.
58 by rewrite Heq.
59Qed.
60
61Lemma fmap_insert_lookup `{FinMap K M} {A B}
62 (f : A → B) (m1 : M A) (m2 : M B) i x :
63 f <$> m1 = <[i := x]>m2 →
64 f <$> m1 !! i = Some x.
65Proof.
66 intros Hmap.
67 rewrite <-lookup_fmap.
68 rewrite Hmap.
69 apply lookup_insert.
70Qed.
71
72Lemma map_dom_delete_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
73 (m1 : M A) (m2 : M B) i x y :
74 dom (delete i m1) = dom (delete i m2) →
75 dom (<[i := x]>m1) = dom (<[i := y]> m2).
76Proof.
77 intros Hdel.
78 setoid_rewrite <-insert_delete_insert at 1 2.
79 rewrite 2 dom_insert_L.
80 set_solver.
81Qed.
82
83Lemma map_dom_delete_insert_subseteq_L `{FinMapDom K M D} `{!LeibnizEquiv D}
84 {A B} (m1 : M A) (m2 : M B) i x y :
85 dom (delete i m1) ⊆ dom (delete i m2) →
86 dom (<[i := x]>m1) ⊆ dom (<[i := y]> m2).
87Proof.
88 intros Hdel.
89 setoid_rewrite <-insert_delete_insert at 1 2.
90 rewrite 2 dom_insert_L.
91 set_solver.
92Qed.
93
94Lemma map_dom_empty_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A}
95 (m : M A) : dom (∅ : M A) = dom m → m = ∅.
96Proof.
97 intros Hdom.
98 rewrite dom_empty_L in Hdom.
99 symmetry in Hdom.
100 by apply dom_empty_inv_L.
101Qed.
102
103Lemma map_dom_insert_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A}
104 (i : K) (x : A) (m1 m2 : M A) :
105 dom (<[i := x]>m1) = dom m2 →
106 dom (delete i m1) = dom (delete i m2) ∧ i ∈ dom m2.
107Proof. set_solver. Qed.
108
109(** map_mapM *)
110
111Definition map_mapM {M : Type → Type} `{MBind F} `{MRet F} `{FinMap K M} {A B}
112 (f : A → F B) (m : M A) : F (M B) :=
113 map_fold (λ i x om', m' ← om'; x' ← f x; mret $ <[i := x']>m') (mret ∅) m.
114
115Lemma map_mapM_dom_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
116 (f : A → option B) (m1 : M A) (m2 : M B) :
117 map_mapM f m1 = Some m2 → dom m1 = dom m2.
118Proof.
119 revert m2.
120 induction m1 using map_ind; intros m2 HmapM.
121 - unfold map_mapM in HmapM. rewrite map_fold_empty in HmapM.
122 simplify_option_eq.
123 by rewrite 2 dom_empty_L.
124 - unfold map_mapM in HmapM.
125 rewrite map_fold_insert_L in HmapM.
126 + simplify_option_eq.
127 apply IHm1 in Heqo.
128 rewrite 2 dom_insert_L.
129 by f_equal.
130 + intros.
131 destruct y; simplify_option_eq; try done.
132 destruct (f z2); simplify_option_eq.
133 * destruct (f z1); simplify_option_eq; try done.
134 f_equal. by apply insert_commute.
135 * destruct (f z1); by simplify_option_eq.
136 + done.
137Qed.
138
139Lemma map_mapM_option_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
140 (f : A → option B) (m1 : M A) (m2 m2' : M B)
141 (i : K) (x : A) (x' : B) :
142 m1 !! i = None →
143 map_mapM f (<[i := x]>m1) = Some m2 →
144 ∃ x', f x = Some x' ∧ map_mapM f m1 = Some (delete i m2).
145Proof.
146 intros Helem HmapM.
147 unfold map_mapM in HmapM.
148 rewrite map_fold_insert_L in HmapM.
149 - simplify_option_eq.
150 exists H15.
151 split; try done.
152 rewrite delete_insert.
153 apply Heqo.
154 apply map_mapM_dom_L in Heqo.
155 apply not_elem_of_dom in Helem.
156 apply not_elem_of_dom.
157 set_solver.
158 - intros.
159 destruct y; simplify_option_eq; try done.
160 destruct (f z2); simplify_option_eq.
161 + destruct (f z1); simplify_option_eq; try done.
162 f_equal. by apply insert_commute.
163 + destruct (f z1); by simplify_option_eq.
164 - done.
165Qed.
166
167(** map_Forall2 *)
168
169Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
170 (R : A → B → Prop) :=
171 map_relation (M := M) R (λ _, False) (λ _, False).
172
173Global Instance map_Forall2_dec `{FinMap K M} {A B} (R : A → B → Prop)
174 `{∀ a b, Decision (R a b)} : RelDecision (map_Forall2 (M := M) R).
175Proof. apply map_relation_dec; intros; try done; apply False_dec. Qed.
176
177Lemma map_Forall2_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
178 (m1 : M A) (m2 : M B) R i x y :
179 m1 !! i = None →
180 m2 !! i = None →
181 R x y →
182 map_Forall2 R m1 m2 →
183 map_Forall2 R (<[i := x]>m1) (<[i := y]>m2).
184Proof.
185 unfold map_Forall2, map_relation, option_relation.
186 intros Him1 Him2 HR HForall2 j.
187 destruct (decide (i = j)).
188 + simplify_option_eq. by rewrite 2 lookup_insert.
189 + rewrite 2 lookup_insert_ne by done. apply HForall2.
190Qed.
191
192Lemma map_Forall2_insert_weak `{FinMap K M} {A B}
193 (m1 : M A) (m2 : M B) R i x y :
194 R x y →
195 map_Forall2 R (delete i m1) (delete i m2) →
196 map_Forall2 R (<[i := x]>m1) (<[i := y]>m2).
197Proof.
198 unfold map_Forall2, map_relation, option_relation.
199 intros HR HForall2 j.
200 destruct (decide (i = j)).
201 - simplify_option_eq. by rewrite 2 lookup_insert.
202 - rewrite 2 lookup_insert_ne by done.
203 rewrite <-lookup_delete_ne with (i := i) by done.
204 replace (m2 !! j) with (delete i m2 !! j); try by apply lookup_delete_ne.
205 apply HForall2.
206Qed.
207
208Lemma map_Forall2_destruct `{FinMap K M} {A B}
209 (m1 : M A) (m2 : M B) R i x :
210 map_Forall2 R (<[i := x]>m1) m2 →
211 ∃ y m2', m2' !! i = None ∧ m2 = <[i := y]>m2'.
212Proof.
213 intros HForall2.
214 unfold map_Forall2, map_relation, option_relation in HForall2.
215 pose proof (HForall2 i). clear HForall2.
216 case_match.
217 - case_match; try done.
218 exists b, (delete i m2).
219 split.
220 * apply lookup_delete.
221 * by rewrite insert_delete_insert, insert_id.
222 - case_match; try done.
223 by rewrite lookup_insert in H8.
224Qed.
225
226Lemma map_Forall2_insert_inv `{FinMap K M} {A B}
227 (m1 : M A) (m2 : M B) R i x y :
228 map_Forall2 R (<[i := x]>m1) (<[i := y]>m2) →
229 R x y ∧ map_Forall2 R (delete i m1) (delete i m2).
230Proof.
231 intros HForall2.
232 unfold map_Forall2, map_relation, option_relation in HForall2.
233 pose proof (HForall2 i).
234 case_match.
235 - case_match; try done.
236 rewrite lookup_insert in H8. rewrite lookup_insert in H9.
237 simplify_eq /=. split; try done.
238 unfold map_Forall2, map_relation, option_relation.
239 intros j.
240 destruct (decide (i = j)).
241 + simplify_option_eq.
242 case_match.
243 * by rewrite lookup_delete in H8.
244 * case_match; [|done].
245 by rewrite lookup_delete in H9.
246 + case_match; case_match;
247 rewrite lookup_delete_ne in H8 by done;
248 rewrite lookup_delete_ne in H9 by done;
249 pose proof (HForall2 j);
250 case_match; case_match; try done;
251 rewrite lookup_insert_ne in H11 by done;
252 rewrite lookup_insert_ne in H12 by done;
253 by simplify_eq /=.
254 - by rewrite lookup_insert in H8.
255Qed.
256
257Lemma map_Forall2_insert_inv_strict `{FinMap K M} {A B}
258 (m1 : M A) (m2 : M B) R i x y :
259 m1 !! i = None →
260 m2 !! i = None →
261 map_Forall2 R (<[i := x]>m1) (<[i := y]>m2) →
262 R x y ∧ map_Forall2 R m1 m2.
263Proof.
264 intros Him1 Him2 HForall2.
265 apply map_Forall2_insert_inv in HForall2 as [HPixy HForall2].
266 split; try done.
267 apply delete_notin in Him1, Him2.
268 by rewrite Him1, Him2 in HForall2.
269Qed.
270
271Lemma map_Forall2_dom_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
272 (R : A → B → Prop) (m1 : M A) (m2 : M B) :
273 map_Forall2 R m1 m2 → dom m1 = dom m2.
274Proof.
275 revert m2.
276 induction m1 using map_ind; intros m2.
277 - intros HForall2.
278 destruct m2 using map_ind; [set_solver|].
279 unfold map_Forall2, map_relation, option_relation in HForall2.
280 pose proof (HForall2 i). by rewrite lookup_empty, lookup_insert in H15.
281 - intros HForall2.
282 apply map_Forall2_destruct in HForall2 as Hm2.
283 destruct Hm2 as [y [m2' [Hm21 Hm22]]]. simplify_eq /=.
284 apply map_Forall2_insert_inv_strict in HForall2 as [_ HForall2]; try done.
285 set_solver.
286Qed.
287
288Lemma map_Forall2_empty_l_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
289 (R : A → B → Prop) (m2 : M B) :
290 map_Forall2 R ∅ m2 → m2 = ∅.
291Proof.
292 intros HForall2.
293 apply map_Forall2_dom_L in HForall2 as Hdom.
294 rewrite dom_empty_L in Hdom.
295 symmetry in Hdom.
296 by apply dom_empty_inv_L in Hdom.
297Qed.
298
299Lemma map_Forall2_empty_r_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
300 (R : A → B → Prop) (m1 : M A) :
301 map_Forall2 R m1 ∅ → m1 = ∅.
302Proof.
303 intros HForall2.
304 apply map_Forall2_dom_L in HForall2 as Hdom.
305 rewrite dom_empty_L in Hdom.
306 by apply dom_empty_inv_L in Hdom.
307Qed.
308
309Lemma map_Forall2_empty `{FinMap K M} {A B} (R : A → B → Prop):
310 map_Forall2 R (∅ : M A) (∅ : M B).
311Proof.
312 unfold map_Forall2, map_relation.
313 intros i. by rewrite 2 lookup_empty.
314Qed.
315
316Lemma map_Forall2_impl_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
317 (R1 R2 : A → B → Prop) :
318 (∀ a b, R1 a b → R2 a b) →
319 ∀ (m1 : M A) (m2 : M B),
320 map_Forall2 R1 m1 m2 → map_Forall2 R2 m1 m2.
321Proof.
322 intros HR1R2 ?? HForall2.
323 unfold map_Forall2, map_relation, option_relation in *.
324 intros j. pose proof (HForall2 j). clear HForall2.
325 case_match; case_match; try done.
326 by apply HR1R2.
327Qed.
328
329Lemma map_Forall2_fmap_r_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B C}
330 (P : A → C → Prop) (m1 : M A) (m2 : M B) (f : B → C) :
331 map_Forall2 P m1 (f <$> m2) → map_Forall2 (λ l r, P l (f r)) m1 m2.
332Proof.
333 intros HForall2.
334 unfold map_Forall2, map_relation, option_relation in *.
335 intros j. pose proof (HForall2 j). clear HForall2.
336 case_match; case_match; try done; case_match;
337 rewrite lookup_fmap in H16; rewrite H17 in H16; by simplify_eq/=.
338Qed.
339
340Lemma map_Forall2_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A}
341 (m1 m2 : M A) :
342 m1 = m2 ↔ map_Forall2 (=) m1 m2.
343Proof.
344 split; revert m2.
345 - induction m1 using map_ind; intros m2 Heq; inv Heq.
346 + apply map_Forall2_empty.
347 + apply map_Forall2_insert_L; try done. by apply IHm1.
348 - induction m1 using map_ind; intros m2 HForall2.
349 + by apply map_Forall2_empty_l_L in HForall2.
350 + apply map_Forall2_destruct in HForall2 as Hm.
351 destruct Hm as [y [m2' [Him2' Heqm2]]]. subst.
352 apply map_Forall2_insert_inv in HForall2 as [Heqxy HForall2].
353 rewrite 2 delete_notin in HForall2 by done.
354 apply IHm1 in HForall2. by subst.
355Qed.
356
357Lemma map_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A}
358 (i : K) (x1 x2 : A) (m1 m2 : M A) :
359 x1 = x2 →
360 delete i m1 = delete i m2 →
361 <[i := x1]>m1 = <[i := x2]>m2.
362Proof.
363 intros Heq Hdel.
364 apply map_Forall2_eq_L.
365 eapply map_Forall2_insert_weak; [done|].
366 by apply map_Forall2_eq_L.
367Qed.
368
369Lemma map_insert_rev_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A}
370 (i : K) (x1 x2 : A) (m1 m2 : M A) :
371 <[i := x1]>m1 = <[i := x2]>m2 → x1 = x2 ∧ delete i m1 = delete i m2.
372Proof.
373 intros Heq. apply map_Forall2_eq_L in Heq.
374 apply map_Forall2_insert_inv in Heq as [Heq1 Heq2].
375 by apply map_Forall2_eq_L in Heq2.
376Qed.
377
378Lemma map_insert_rev_1_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A}
379 (i : K) (x1 x2 : A) (m1 m2 : M A) :
380 <[i := x1]>m1 = <[i := x2]>m2 → x1 = x2.
381Proof. apply map_insert_rev_L. Qed.
382
383Lemma map_insert_rev_2_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A}
384 (i : K) (x1 x2 : A) (m1 m2 : M A) :
385 <[i := x1]>m1 = <[i := x2]>m2 → delete i m1 = delete i m2.
386Proof. apply map_insert_rev_L. Qed.
387
388Lemma map_Forall2_alt_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
389 (R : A → B → Prop) (m1 : M A) (m2 : M B) :
390 map_Forall2 R m1 m2 ↔
391 dom m1 = dom m2 ∧ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → R x y.
392Proof.
393 split.
394 - intros HForall2.
395 split.
396 + by apply map_Forall2_dom_L in HForall2.
397 + intros i x y Him1 Him2.
398 unfold map_Forall2, map_relation, option_relation in HForall2.
399 pose proof (HForall2 i). clear HForall2.
400 by simplify_option_eq.
401 - intros [Hdom HForall2].
402 unfold map_Forall2, map_relation, option_relation.
403 intros j.
404 case_match; case_match; try done.
405 + by eapply HForall2.
406 + apply mk_is_Some in H14.
407 apply not_elem_of_dom in H15.
408 apply elem_of_dom in H14.
409 set_solver.
410 + apply not_elem_of_dom in H14.
411 apply mk_is_Some in H15.
412 apply elem_of_dom in H15.
413 set_solver.
414Qed.
415
416(** Relation between map_mapM and map_Forall2 *)
417
418Lemma map_mapM_Some_1_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
419 (f : A → option B) (m1 : M A) (m2 : M B) :
420 map_mapM f m1 = Some m2 → map_Forall2 (λ x y, f x = Some y) m1 m2.
421Proof.
422 revert m1 m2 f.
423 induction m1 using map_ind.
424 - intros m2 f Hmap_mapM.
425 unfold map_mapM in Hmap_mapM.
426 rewrite map_fold_empty in Hmap_mapM.
427 simplify_option_eq. apply map_Forall2_empty.
428 - intros m2 f Hmap_mapM.
429 csimpl in Hmap_mapM.
430 unfold map_mapM in Hmap_mapM.
431 csimpl in Hmap_mapM.
432 rewrite map_fold_insert_L in Hmap_mapM.
433 + simplify_option_eq.
434 apply IHm1 in Heqo.
435 apply map_Forall2_insert_L; try done.
436 apply not_elem_of_dom in H14.
437 apply not_elem_of_dom.
438 apply map_Forall2_dom_L in Heqo.
439 set_solver.
440 + intros.
441 destruct y; simplify_option_eq; try done.
442 destruct (f z2); simplify_option_eq.
443 * destruct (f z1); simplify_option_eq; try done.
444 f_equal. by apply insert_commute.
445 * destruct (f z1); by simplify_option_eq.
446 + done.
447Qed.
448
449Lemma map_mapM_Some_2_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
450 (f : A → option B) (m1 : M A) (m2 : M B) :
451 map_Forall2 (λ x y, f x = Some y) m1 m2 → map_mapM f m1 = Some m2.
452Proof.
453 revert m2.
454 induction m1 using map_ind; intros m2 HForall2.
455 - unfold map_mapM. rewrite map_fold_empty.
456 apply map_Forall2_empty_l_L in HForall2.
457 by simplify_eq.
458 - destruct (map_Forall2_destruct _ _ _ _ _ HForall2) as
459 [y [m2' [HForall21 HForall22]]]. subst.
460 destruct (map_Forall2_insert_inv_strict _ _ _ _ _ _ H14 HForall21 HForall2) as
461 [Hfy HForall22].
462 apply IHm1 in HForall22.
463 unfold map_mapM.
464 rewrite map_fold_insert_L; try by simplify_option_eq.
465 intros.
466 destruct y0; simplify_option_eq; try done.
467 destruct (f z2); simplify_option_eq.
468 * destruct (f z1); simplify_option_eq; try done.
469 f_equal. by apply insert_commute.
470 * destruct (f z1); by simplify_option_eq.
471Qed.
472
473Lemma map_mapM_Some_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B}
474 (f : A → option B) (m1 : M A) (m2 : M B) :
475 map_mapM f m1 = Some m2 ↔ map_Forall2 (λ x y, f x = Some y) m1 m2.
476Proof. split; [apply map_mapM_Some_1_L | apply map_mapM_Some_2_L]. Qed.
diff --git a/matching.v b/matching.v
new file mode 100644
index 0000000..494bb92
--- /dev/null
+++ b/matching.v
@@ -0,0 +1,609 @@
1Require Import Coq.Strings.Ascii.
2Require Import Coq.Strings.String.
3Require Import Coq.NArith.BinNat.
4From stdpp Require Import fin_sets gmap option.
5From mininix Require Import expr maptools.
6
7Open Scope string_scope.
8Open Scope N_scope.
9Open Scope Z_scope.
10Open Scope nat_scope.
11
12Reserved Notation "bs '~' m '~>' brs" (at level 55).
13
14Inductive matches_r : gmap string expr → matcher → gmap string b_rhs -> Prop :=
15 | E_MatchEmpty strict : ∅ ~ M_Matcher ∅ strict ~> ∅
16 | E_MatchAny bs : bs ~ M_Matcher ∅ false ~> ∅
17 | E_MatchMandatory bs x e m bs' strict :
18 bs !! x = None →
19 m !! x = None →
20 delete x bs ~ M_Matcher m strict ~> bs' →
21 <[x := e]>bs ~ M_Matcher (<[x := M_Mandatory]>m) strict
22 ~> <[x := B_Nonrec e]>bs'
23 | E_MatchOptAvail bs x d e m bs' strict :
24 bs !! x = None →
25 m !! x = None →
26 delete x bs ~ M_Matcher m strict ~> bs' →
27 <[x := d]>bs ~ M_Matcher (<[x := M_Optional e]>m) strict
28 ~> <[x := B_Nonrec d]>bs'
29 | E_MatchOptDefault bs x e m bs' strict :
30 bs !! x = None →
31 m !! x = None →
32 bs ~ M_Matcher m strict ~> bs' →
33 bs ~ M_Matcher (<[x := M_Optional e]>m) strict ~> <[x := B_Rec e]>bs'
34where "bs ~ m ~> brs" := (matches_r bs m brs).
35
36Definition map_foldM `{Countable K} `{FinMap K M} `{MBind F} `{MRet F} {A B}
37 (f : K → A → B → F B) (init : B) (m : M A) : F B :=
38 map_fold (λ i x acc, acc ≫= f i x) (mret init) m.
39
40Definition matches_aux_f (x : string) (rhs : m_rhs)
41 (acc : option (gmap string expr * gmap string b_rhs)) :=
42 acc ← acc;
43 let (bs, brs) := (acc : gmap string expr * gmap string b_rhs) in
44 match rhs with
45 | M_Mandatory =>
46 e ← bs !! x;
47 Some (bs, <[x := B_Nonrec e]>brs)
48 | M_Optional e =>
49 match bs !! x with
50 | Some e' => Some (bs, <[x := B_Nonrec e']>brs)
51 | None => Some (bs, <[x := B_Rec e]>brs)
52 end
53 end.
54
55Definition matches_aux (ms : gmap string m_rhs) (bs : gmap string expr) :
56 option (gmap string expr * gmap string b_rhs) :=
57 map_fold matches_aux_f (Some (bs, ∅)) ms.
58
59Definition matches (m : matcher) (bs : gmap string expr) :
60 option (gmap string b_rhs) :=
61 match m with
62 | M_Matcher ms strict =>
63 guard (strict → dom bs ⊆ matcher_keys m);;
64 snd <$> matches_aux ms bs
65 end.
66
67(* Copied from stdpp and changed so that the value types
68 of m1 and m2 are decoupled *)
69Lemma dom_subseteq_size' `{FinMapDom K M D} {A B} (m1 : M A) (m2 : M B) :
70 dom m2 ⊆ dom m1 → size m2 ≤ size m1.
71Proof.
72 revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom.
73 { rewrite map_size_empty. lia. }
74 rewrite dom_insert in Hdom.
75 assert (i ∉ dom m2) by (by apply not_elem_of_dom).
76 assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver.
77 rewrite <-(insert_delete m1 i x') by done.
78 rewrite !map_size_insert_None, <-Nat.succ_le_mono
79 by (by rewrite ?lookup_delete).
80 apply IH. rewrite dom_delete. set_solver.
81Qed.
82
83Lemma dom_empty_subset `{Countable K} `{FinMapDom K M D} {A B} (m : M A) :
84 dom m ⊆ dom (∅ : M B) → m = ∅.
85Proof.
86 intros Hdom.
87 apply dom_subseteq_size' in Hdom.
88 rewrite map_size_empty in Hdom.
89 inv Hdom.
90 by apply map_size_empty_inv.
91Qed.
92
93Lemma matches_aux_empty bs : matches_aux ∅ bs = Some (bs, ∅).
94Proof. done. Qed.
95
96Lemma matches_aux_f_comm (x : string) (rhs : m_rhs) (m : gmap string m_rhs)
97 (y z : string) (rhs1 rhs2 : m_rhs)
98 (acc : option (gmap string expr * gmap string b_rhs)) :
99 m !! x = None → y ≠ z →
100 <[x:=rhs]> m !! y = Some rhs1 →
101 <[x:=rhs]> m !! z = Some rhs2 →
102 matches_aux_f y rhs1 (matches_aux_f z rhs2 acc) =
103 matches_aux_f z rhs2 (matches_aux_f y rhs1 acc).
104Proof.
105 intros Hxm Hyz Hym Hzm.
106 unfold matches_aux_f.
107 destruct acc.
108 repeat (simplify_option_eq || done ||
109 destruct (g !! y) eqn:Egy || destruct (g !! z) eqn:Egz ||
110 case_match || rewrite insert_commute). done.
111Qed.
112
113Lemma matches_aux_insert m bs x rhs :
114 m !! x = None →
115 matches_aux (<[x := rhs]>m) bs = matches_aux_f x rhs (matches_aux m bs).
116Proof.
117 intros Hnotin. unfold matches_aux.
118 rewrite map_fold_insert_L; try done.
119 clear bs.
120 intros y z rhs1 rhs2 acc Hyz Hym Hzm.
121 by eapply matches_aux_f_comm.
122Qed.
123
124Lemma matches_aux_bs m bs bs' brs :
125 matches_aux m bs = Some (bs', brs) → bs = bs'.
126Proof.
127 revert bs bs' brs.
128 induction m using map_ind; intros bs bs' brs Hmatches.
129 - rewrite matches_aux_empty in Hmatches. congruence.
130 - rewrite matches_aux_insert in Hmatches; try done.
131 unfold matches_aux_f in Hmatches.
132 simplify_option_eq.
133 destruct H0.
134 case_match; try case_match;
135 simplify_option_eq; by apply IHm with (brs := g0).
136Qed.
137
138Lemma matches_aux_impl m bs brs x e :
139 m !! x = None →
140 bs !! x = None →
141 matches_aux m (<[x := e]>bs) = Some (<[x := e]>bs, brs) →
142 matches_aux m bs = Some (bs, brs).
143Proof.
144 intros Hxm Hxbs Hmatches.
145 revert bs brs Hxm Hxbs Hmatches.
146 induction m using map_ind; intros bs brs Hxm Hxbs Hmatches.
147 - rewrite matches_aux_empty.
148 rewrite matches_aux_empty in Hmatches.
149 by simplify_option_eq.
150 - rewrite matches_aux_insert in Hmatches by done.
151 rewrite matches_aux_insert by done.
152 apply lookup_insert_None in Hxm as [Hxm1 Hxm2].
153 unfold matches_aux_f in Hmatches. simplify_option_eq.
154 destruct H0. case_match.
155 + simplify_option_eq.
156 rewrite lookup_insert_ne in Heqo0 by done.
157 pose proof (IHm bs g0 Hxm1 Hxbs Heqo).
158 rewrite H1. by simplify_option_eq.
159 + case_match; simplify_option_eq;
160 rewrite lookup_insert_ne in H1 by done;
161 pose proof (IHm bs g0 Hxm1 Hxbs Heqo);
162 rewrite H0; by simplify_option_eq.
163Qed.
164
165Lemma matches_aux_impl_2 m bs brs x e :
166 m !! x = None →
167 bs !! x = None →
168 matches_aux m bs = Some (bs, brs) →
169 matches_aux m (<[x := e]>bs) = Some (<[x := e]>bs, brs).
170Proof.
171 intros Hxm Hxbs Hmatches.
172 revert bs brs Hxm Hxbs Hmatches.
173 induction m using map_ind; intros bs brs Hxm Hxbs Hmatches.
174 - rewrite matches_aux_empty.
175 rewrite matches_aux_empty in Hmatches.
176 by simplify_option_eq.
177 - rewrite matches_aux_insert in Hmatches by done.
178 rewrite matches_aux_insert by done.
179 apply lookup_insert_None in Hxm as [Hxm1 Hxm2].
180 unfold matches_aux_f in Hmatches. simplify_option_eq.
181 destruct H0. case_match.
182 + simplify_option_eq.
183 rewrite <-lookup_insert_ne with (i := x) (x := e) in Heqo0 by done.
184 pose proof (IHm bs g0 Hxm1 Hxbs Heqo).
185 rewrite H1. by simplify_option_eq.
186 + case_match; simplify_option_eq;
187 rewrite <-lookup_insert_ne with (i := x) (x := e) in H1 by done;
188 pose proof (IHm bs g0 Hxm1 Hxbs Heqo);
189 rewrite H0; by simplify_option_eq.
190Qed.
191
192Lemma matches_aux_dom m bs brs :
193 matches_aux m bs = Some (bs, brs) → dom m = dom brs.
194Proof.
195 revert bs brs.
196 induction m using map_ind; intros bs brs Hmatches.
197 - rewrite matches_aux_empty in Hmatches. by simplify_eq.
198 - rewrite matches_aux_insert in Hmatches by done.
199 unfold matches_aux_f in Hmatches. simplify_option_eq. destruct H0.
200 case_match; try case_match;
201 simplify_option_eq; apply IHm in Heqo; set_solver.
202Qed.
203
204Lemma matches_aux_inv m bs brs x e :
205 m !! x = None → bs !! x = None → brs !! x = None →
206 matches_aux (<[x := M_Mandatory]>m) (<[x := e]>bs) =
207 Some (<[x := e]>bs, <[x := B_Nonrec e]>brs) →
208 matches_aux m bs = Some (bs, brs).
209Proof.
210 intros Hxm Hxbs Hxbrs Hmatches.
211 rewrite matches_aux_insert in Hmatches by done.
212 unfold matches_aux_f in Hmatches. simplify_option_eq.
213 destruct H. simplify_option_eq.
214 rewrite lookup_insert in Heqo0. simplify_option_eq.
215 apply matches_aux_impl in Heqo; try done.
216 simplify_option_eq.
217 apply matches_aux_dom in Heqo as Hdom.
218 rewrite Heqo. do 2 f_equal.
219 assert (g0 !! x = None).
220 { apply not_elem_of_dom in Hxm.
221 rewrite Hdom in Hxm.
222 by apply not_elem_of_dom. }
223 replace g0 with (delete x (<[x:=B_Nonrec H]> g0));
224 try by rewrite delete_insert.
225 replace brs with (delete x (<[x:=B_Nonrec H]> brs));
226 try by rewrite delete_insert.
227 by rewrite H1.
228Qed.
229
230Lemma disjoint_union_subseteq_l `{FinSet A C} `{!LeibnizEquiv C} (X Y Z : C) :
231 X ## Y → X ## Z → X ∪ Y ⊆ X ∪ Z → Y ⊆ Z.
232Proof.
233 revert Y Z.
234 induction X using set_ind_L; intros Y Z Hdisj1 Hdisj2 Hsubs.
235 - by do 2 rewrite union_empty_l_L in Hsubs.
236 - do 2 rewrite <-union_assoc_L in Hsubs.
237 apply IHX; set_solver.
238Qed.
239
240Lemma singleton_notin_union_disjoint `{FinMapDom K M D} {A} (m : M A) (i : K) :
241 m !! i = None →
242 {[i]} ## dom m.
243Proof.
244 intros Hlookup. apply disjoint_singleton_l.
245 by apply not_elem_of_dom in Hlookup.
246Qed.
247
248Lemma matches_step bs brs m strict x :
249 matches (M_Matcher (<[x := M_Mandatory]>m) strict) bs = Some brs →
250 ∃ e, bs !! x = Some e ∧ brs !! x = Some (B_Nonrec e).
251Proof.
252 intros Hmatches.
253 destruct (decide (is_Some (bs !! x))).
254 - destruct i. exists x0. split; [done|].
255 unfold matches in Hmatches.
256 destruct strict; simplify_option_eq.
257 + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m))
258 in Heqo0; try by rewrite insert_delete_insert.
259 rewrite matches_aux_insert in Heqo0 by apply lookup_delete.
260 unfold matches_aux_f in Heqo0. simplify_option_eq.
261 destruct H3. simplify_option_eq.
262 apply matches_aux_bs in Heqo as Hdom. simplify_option_eq.
263 apply lookup_insert.
264 + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m))
265 in Heqo; try by rewrite insert_delete_insert.
266 rewrite matches_aux_insert in Heqo by apply lookup_delete.
267 unfold matches_aux_f in Heqo. simplify_option_eq.
268 destruct H1. simplify_option_eq.
269 apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq.
270 apply lookup_insert.
271 - unfold matches in Hmatches.
272 destruct strict; simplify_option_eq.
273 + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m))
274 in Heqo0; try by rewrite insert_delete_insert.
275 rewrite matches_aux_insert in Heqo0 by apply lookup_delete.
276 unfold matches_aux_f in Heqo0. simplify_option_eq.
277 destruct H2. simplify_option_eq.
278 apply matches_aux_bs in Heqo as Hdom. simplify_option_eq.
279 rewrite Heqo1 in n.
280 exfalso. by apply n.
281 + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m))
282 in Heqo; try by rewrite insert_delete_insert.
283 rewrite matches_aux_insert in Heqo by apply lookup_delete.
284 unfold matches_aux_f in Heqo. simplify_option_eq.
285 destruct H0. simplify_option_eq.
286 apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq.
287 rewrite Heqo1 in n.
288 exfalso. by apply n.
289Qed.
290
291Lemma matches_step' bs brs m strict x :
292 matches (M_Matcher (<[x := M_Mandatory]>m) strict) bs = Some brs →
293 ∃ e bs' brs',
294 bs' !! x = None ∧ bs = <[x := e]>bs' ∧
295 brs' !! x = None ∧ brs = <[x := B_Nonrec e]>brs'.
296Proof.
297 intros Hmatches.
298 apply matches_step in Hmatches as He.
299 destruct He as [e [He1 He2]].
300 exists e, (delete x bs), (delete x brs).
301 split_and!; by apply lookup_delete || rewrite insert_delete.
302Qed.
303
304Lemma matches_opt_step bs brs m strict x d :
305 matches (M_Matcher (<[x := M_Optional d]>m) strict) bs = Some brs →
306 (∃ e, bs !! x = Some e ∧ brs !! x = Some (B_Nonrec e)) ∨
307 bs !! x = None ∧ brs !! x = Some (B_Rec d).
308Proof.
309 intros Hmatches.
310 destruct (decide (is_Some (bs !! x))).
311 - destruct i. left. exists x0. split; [done|].
312 unfold matches in Hmatches.
313 destruct strict; simplify_option_eq.
314 + replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m))
315 in Heqo0; try by rewrite insert_delete_insert.
316 rewrite matches_aux_insert in Heqo0 by apply lookup_delete.
317 unfold matches_aux_f in Heqo0. simplify_option_eq.
318 destruct H3. simplify_option_eq.
319 apply matches_aux_bs in Heqo as Hdom. simplify_option_eq.
320 apply lookup_insert.
321 + replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m))
322 in Heqo; try by rewrite insert_delete_insert.
323 rewrite matches_aux_insert in Heqo by apply lookup_delete.
324 unfold matches_aux_f in Heqo. simplify_option_eq.
325 destruct H1. simplify_option_eq.
326 apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq.
327 apply lookup_insert.
328 - unfold matches in Hmatches.
329 destruct strict; simplify_option_eq.
330 + right. apply eq_None_not_Some in n. split; [done|].
331 destruct H0. simplify_option_eq.
332 apply matches_aux_bs in Heqo0 as Hbs. subst.
333 replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m))
334 in Heqo0; try by rewrite insert_delete_insert.
335 rewrite matches_aux_insert in Heqo0 by apply lookup_delete.
336 unfold matches_aux_f in Heqo0. simplify_option_eq.
337 destruct H0. simplify_option_eq.
338 apply matches_aux_bs in Heqo as Hdom. simplify_option_eq.
339 apply lookup_insert.
340 + right. apply eq_None_not_Some in n. split; [done|].
341 destruct H. simplify_option_eq.
342 apply matches_aux_bs in Heqo as Hbs. subst.
343 replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m))
344 in Heqo; try by rewrite insert_delete_insert.
345 rewrite matches_aux_insert in Heqo by apply lookup_delete.
346 unfold matches_aux_f in Heqo. simplify_option_eq.
347 destruct H. simplify_option_eq.
348 apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq.
349 apply lookup_insert.
350Qed.
351
352Lemma matches_opt_step' bs brs m strict x d :
353 matches (M_Matcher (<[x := M_Optional d]>m) strict) bs = Some brs →
354 (∃ e bs' brs',
355 bs' !! x = None ∧ bs = <[x := e]>bs' ∧
356 brs' !! x = None ∧ brs = <[x := B_Nonrec e]>brs') ∨
357 (∃ brs',
358 bs !! x = None ∧ brs' !! x = None ∧
359 brs = <[x := B_Rec d]>brs').
360Proof.
361 intros Hmatches.
362 apply matches_opt_step in Hmatches as He.
363 destruct He as [He|He].
364 - destruct He as [e [He1 He2]]. left.
365 exists e, (delete x bs), (delete x brs).
366 split; try split; try split.
367 + apply lookup_delete.
368 + by rewrite insert_delete.
369 + apply lookup_delete.
370 + by rewrite insert_delete.
371 - destruct He as [He1 He2]. right.
372 exists (delete x brs). split; try split; try done.
373 + apply lookup_delete.
374 + by rewrite insert_delete.
375Qed.
376
377Lemma matches_inv m bs brs strict x e :
378 m !! x = None → bs !! x = None → brs !! x = None →
379 matches (M_Matcher (<[x := M_Mandatory]>m) strict) (<[x := e]>bs) =
380 Some (<[x := B_Nonrec e]>brs) →
381 matches (M_Matcher m strict) bs = Some brs.
382Proof.
383 intros Hxm Hxbs Hxbrs Hmatch.
384 destruct strict.
385 - simplify_option_eq.
386 + destruct H0. apply matches_aux_bs in Heqo0 as Hbs.
387 simplify_option_eq. by erewrite matches_aux_inv.
388 + exfalso. apply H2.
389 repeat rewrite dom_insert in H1.
390 assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. }
391 assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. }
392 by apply disjoint_union_subseteq_l with (X := {[x]}).
393 - simplify_option_eq.
394 destruct H. apply matches_aux_bs in Heqo as Hbs.
395 simplify_option_eq. by erewrite matches_aux_inv.
396Qed.
397
398Lemma matches_aux_avail_inv m bs brs x d e :
399 m !! x = None → bs !! x = None → brs !! x = None →
400 matches_aux (<[x := M_Optional d]>m) (<[x := e]>bs) =
401 Some (<[x := e]>bs, <[x := B_Nonrec e]>brs) →
402 matches_aux m bs = Some (bs, brs).
403Proof.
404 intros Hxm Hxbs Hxbrs Hmatches.
405 rewrite matches_aux_insert in Hmatches by done.
406 unfold matches_aux_f in Hmatches. simplify_option_eq.
407 destruct H. simplify_option_eq.
408 apply matches_aux_bs in Heqo as Hbs. subst.
409 rewrite lookup_insert in Hmatches. simplify_option_eq.
410 apply matches_aux_impl in Heqo; try done.
411 simplify_option_eq.
412 apply matches_aux_dom in Heqo as Hdom.
413 rewrite Heqo. do 2 f_equal.
414 assert (g0 !! x = None).
415 { apply not_elem_of_dom in Hxm.
416 rewrite Hdom in Hxm.
417 by apply not_elem_of_dom. }
418 replace g0 with (delete x (<[x:=B_Nonrec e]> g0));
419 try by rewrite delete_insert.
420 replace brs with (delete x (<[x:=B_Nonrec e]> brs));
421 try by rewrite delete_insert.
422 by rewrite Hmatches.
423Qed.
424
425Lemma matches_avail_inv m bs brs strict x d e :
426 m !! x = None → bs !! x = None → brs !! x = None →
427 matches (M_Matcher (<[x := M_Optional d]>m) strict) (<[x := e]>bs) =
428 Some (<[x := B_Nonrec e]>brs) →
429 matches (M_Matcher m strict) bs = Some brs.
430Proof.
431 intros Hxm Hxbs Hxbrs Hmatch.
432 destruct strict.
433 - simplify_option_eq.
434 + destruct H0. apply matches_aux_bs in Heqo0 as Hbs.
435 simplify_option_eq. by erewrite matches_aux_avail_inv.
436 + exfalso. apply H2.
437 repeat rewrite dom_insert in H1.
438 assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. }
439 assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. }
440 by apply disjoint_union_subseteq_l with (X := {[x]}).
441 - simplify_option_eq.
442 destruct H. apply matches_aux_bs in Heqo as Hbs.
443 simplify_option_eq. by erewrite matches_aux_avail_inv.
444Qed.
445
446Lemma matches_aux_default_inv m bs brs x e :
447 m !! x = None → bs !! x = None → brs !! x = None →
448 matches_aux (<[x := M_Optional e]>m) bs =
449 Some (bs, <[x := B_Rec e]>brs) →
450 matches_aux m bs = Some (bs, brs).
451Proof.
452 intros Hxm Hxbs Hxbrs Hmatches.
453 rewrite matches_aux_insert in Hmatches by done.
454 unfold matches_aux_f in Hmatches. simplify_option_eq.
455 destruct H. simplify_option_eq.
456 apply matches_aux_bs in Heqo as Hbs. subst.
457 rewrite Hxbs in Hmatches. simplify_option_eq.
458 apply matches_aux_dom in Heqo as Hdom.
459 do 2 f_equal.
460 assert (g0 !! x = None).
461 { apply not_elem_of_dom in Hxm.
462 rewrite Hdom in Hxm.
463 by apply not_elem_of_dom. }
464 replace g0 with (delete x (<[x:=B_Rec e]> g0));
465 try by rewrite delete_insert.
466 replace brs with (delete x (<[x:=B_Rec e]> brs));
467 try by rewrite delete_insert.
468 by rewrite Hmatches.
469Qed.
470
471Lemma matches_default_inv m bs brs strict x e :
472 m !! x = None → bs !! x = None → brs !! x = None →
473 matches (M_Matcher (<[x := M_Optional e]>m) strict) bs =
474 Some (<[x := B_Rec e]>brs) →
475 matches (M_Matcher m strict) bs = Some brs.
476Proof.
477 intros Hxm Hxbs Hxbrs Hmatch.
478 destruct strict.
479 - simplify_option_eq.
480 + destruct H0. apply matches_aux_bs in Heqo0 as Hbs.
481 simplify_option_eq. by erewrite matches_aux_default_inv.
482 + exfalso. apply H2.
483 rewrite dom_insert in H1.
484 assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. }
485 assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. }
486 apply disjoint_union_subseteq_l with (X := {[x]}); set_solver.
487 - simplify_option_eq.
488 destruct H. apply matches_aux_bs in Heqo as Hbs.
489 simplify_option_eq. by erewrite matches_aux_default_inv.
490Qed.
491
492Theorem matches_sound m bs brs : matches m bs = Some brs → bs ~ m ~> brs.
493Proof.
494 intros Hmatches.
495 destruct m.
496 revert strict bs brs Hmatches.
497 induction ms using map_ind; intros strict bs brs Hmatches.
498 - destruct strict; simplify_option_eq.
499 + apply dom_empty_subset in H0. simplify_eq.
500 constructor.
501 + constructor.
502 - destruct x.
503 + apply matches_step' in Hmatches as He.
504 destruct He as [e [bs' [brs' [Hbs'1 [Hbs'2 [Hbrs'1 Hbrs'2]]]]]].
505 subst. constructor; try done.
506 rewrite delete_notin by done.
507 apply IHms.
508 by apply matches_inv in Hmatches.
509 + apply matches_opt_step' in Hmatches as He. destruct He as [He|He].
510 * destruct He as [d [bs' [brs' [Hibs' [Hbs' [Hibrs' Hbrs']]]]]].
511 subst. constructor; try done.
512 rewrite delete_notin by done.
513 apply IHms.
514 by apply matches_avail_inv in Hmatches.
515 * destruct He as [brs' [Hibs [Hibrs' Hbrs']]].
516 subst. constructor; try done.
517 apply IHms.
518 by apply matches_default_inv in Hmatches.
519Qed.
520
521Theorem matches_complete m bs brs : bs ~ m ~> brs → matches m bs = Some brs.
522Proof.
523 intros Hbs.
524 induction Hbs.
525 - unfold matches. by simplify_option_eq.
526 - unfold matches. by simplify_option_eq.
527 - unfold matches in *. destruct strict.
528 + simplify_option_eq.
529 * simplify_option_eq. destruct H2. simplify_option_eq.
530 apply fmap_Some. exists (<[x := e]>bs, <[x := B_Nonrec e]>g0).
531 split; [|done].
532 rewrite matches_aux_insert by done.
533 apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq.
534 apply matches_aux_impl_2 with (x := x) (e := e) in Heqo0;
535 [| done | apply lookup_delete].
536 replace bs with (delete x bs); try by apply delete_notin.
537 unfold matches_aux_f.
538 simplify_option_eq. apply bind_Some. exists e.
539 split; [apply lookup_insert | done].
540 * exfalso. apply H4.
541 replace bs with (delete x bs); try by apply delete_notin.
542 apply map_dom_delete_insert_subseteq_L.
543 set_solver.
544 + simplify_option_eq. destruct H1. simplify_option_eq.
545 apply fmap_Some. exists (<[x := e]>bs, <[x := B_Nonrec e]>g0).
546 split; [|done].
547 rewrite matches_aux_insert by done.
548 apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq.
549 apply matches_aux_impl_2 with (x := x) (e := e) in Heqo;
550 [| done | apply lookup_delete].
551 replace bs with (delete x bs); try by apply delete_notin.
552 unfold matches_aux_f.
553 simplify_option_eq. apply bind_Some. exists e.
554 split; [apply lookup_insert | done].
555 - unfold matches in *. destruct strict.
556 + simplify_option_eq.
557 * simplify_option_eq. destruct H2. simplify_option_eq.
558 apply fmap_Some. exists (<[x := d]>bs, <[x := B_Nonrec d]>g0).
559 split; [|done].
560 rewrite matches_aux_insert by done.
561 apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq.
562 apply matches_aux_impl_2 with (x := x) (e := d) in Heqo0;
563 [| done | apply lookup_delete].
564 replace bs with (delete x bs); try by apply delete_notin.
565 unfold matches_aux_f.
566 simplify_option_eq. case_match.
567 -- rewrite lookup_insert in H2. congruence.
568 -- by rewrite lookup_insert in H2.
569 * exfalso. apply H4.
570 replace bs with (delete x bs); try by apply delete_notin.
571 apply map_dom_delete_insert_subseteq_L.
572 set_solver.
573 + simplify_option_eq. destruct H1. simplify_option_eq.
574 apply fmap_Some. exists (<[x := d]>bs, <[x := B_Nonrec d]>g0).
575 split; [|done].
576 rewrite matches_aux_insert by done.
577 apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq.
578 apply matches_aux_impl_2 with (x := x) (e := d) in Heqo;
579 [| done | apply lookup_delete].
580 replace bs with (delete x bs); try by apply delete_notin.
581 unfold matches_aux_f.
582 simplify_option_eq. case_match.
583 * rewrite lookup_insert in H1. congruence.
584 * by rewrite lookup_insert in H1.
585 - unfold matches in *. destruct strict.
586 + simplify_option_eq.
587 * simplify_option_eq. destruct H2. simplify_option_eq.
588 apply fmap_Some. exists (bs, <[x := B_Rec e]>g0).
589 split; [|done].
590 rewrite matches_aux_insert by done.
591 apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq.
592 unfold matches_aux_f.
593 by simplify_option_eq.
594 * exfalso. apply H4. set_solver.
595 + simplify_option_eq. destruct H1. simplify_option_eq.
596 apply fmap_Some. exists (bs, <[x := B_Rec e]>g0).
597 split; [|done].
598 rewrite matches_aux_insert by done.
599 apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq.
600 unfold matches_aux_f.
601 by simplify_option_eq.
602Qed.
603
604Theorem matches_correct m bs brs : matches m bs = Some brs ↔ bs ~ m ~> brs.
605Proof. split; [apply matches_sound | apply matches_complete]. Qed.
606
607Theorem matches_deterministic m bs brs1 brs2 :
608 bs ~ m ~> brs1 → bs ~ m ~> brs2 → brs1 = brs2.
609Proof. intros H1 H2. apply matches_correct in H1, H2. congruence. Qed.
diff --git a/relations.v b/relations.v
new file mode 100644
index 0000000..9bfb7e6
--- /dev/null
+++ b/relations.v
@@ -0,0 +1,73 @@
1From stdpp Require Import relations.
2
3Definition deterministic {A} (R : relation A) :=
4 ∀ x y1 y2, R x y1 → R x y2 → y1 = y2.
5
6(* As in Baader and Nipkow (1998): *)
7(* y is a normal form of x if x -->* y and y is in normal form. *)
8Definition is_nf_of `(R : relation A) x y := (rtc R x y) ∧ nf R y.
9
10(** The reflexive closure. *)
11Inductive rc {A} (R : relation A) : relation A :=
12 | rc_refl x : rc R x x
13 | rc_once x y : R x y → rc R x y.
14
15Hint Constructors rc : core.
16
17(* Baader and Nipkow, Definition 2.7.3. *)
18Definition strongly_confluent {A} (R : relation A) :=
19 ∀ x y1 y2, R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rc R y2 z.
20
21(* Baader and Nipkow, Definition 2.1.4. *)
22Definition semi_confluent {A} (R : relation A) :=
23 ∀ x y1 y2, R x y1 → rtc R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z.
24
25(* Lemma 2.7.4 from Baader and Nipkow *)
26Lemma strong__semi_confluence {A} (R : relation A) :
27 strongly_confluent R → semi_confluent R.
28Proof.
29 intros Hstrc.
30 unfold strongly_confluent in Hstrc.
31 unfold semi_confluent.
32 intros x1 y1 xn Hxy1 [steps Hsteps] % rtc_nsteps.
33 revert x1 y1 xn Hxy1 Hsteps.
34 induction steps; intros x1 y1 xn Hxy1 Hsteps.
35 - inv Hsteps. exists y1.
36 split.
37 + apply rtc_refl.
38 + by apply rtc_once.
39 - inv Hsteps as [|? ? x2 ? Hx1x2 Hsteps'].
40 destruct (Hstrc x1 y1 x2 Hxy1 Hx1x2) as [y2 [Hy21 Hy22]].
41 inv Hy22.
42 + exists xn. split; [|done].
43 apply rtc_transitive with (y := y2); [done|].
44 rewrite rtc_nsteps. by exists steps.
45 + destruct (IHsteps x2 y2 xn H Hsteps') as [yn [Hy2yn Hxnyn]].
46 exists yn. split; [|done].
47 by apply rtc_transitive with (y := y2).
48Qed.
49
50(* Copied from stdpp, originates from Baader and Nipkow (1998) *)
51Definition cr {A} (R : relation A) :=
52 ∀ x y, rtsc R x y → ∃ z, rtc R x z ∧ rtc R y z.
53
54(* Part of Lemma 2.1.5 from Baader and Nipkow (1998) *)
55Lemma semi_confluence__cr {A} (R : relation A) :
56 semi_confluent R → cr R.
57Proof.
58 intros Hsc.
59 unfold semi_confluent in Hsc.
60 unfold cr.
61 intros x y [steps Hsteps] % rtc_nsteps.
62 revert x y Hsteps.
63 induction steps; intros x y Hsteps.
64 - inv Hsteps. by exists y.
65 - inv Hsteps. rename x into y', y into x, y0 into y.
66 apply IHsteps in H1 as H1'. destruct H1' as [z [Hz1 Hz2]].
67 destruct H0.
68 + exists z. split; [|done].
69 by apply rtc_l with (y := y).
70 + destruct (Hsc y y' z H Hz1) as [z' [Hz'1 Hz'2]].
71 exists z'. split; [done|].
72 by apply rtc_transitive with (y := z).
73Qed.
diff --git a/sem.v b/sem.v
new file mode 100644
index 0000000..6560b82
--- /dev/null
+++ b/sem.v
@@ -0,0 +1,167 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import gmap.
3From mininix Require Import binop expr matching relations.
4
5Definition attrset := is_Some ∘ maybe V_Attrset.
6
7Reserved Infix "-->base" (right associativity, at level 55).
8
9Inductive base_step : expr → expr → Prop :=
10 | E_Force (sv : strong_value) :
11 X_Force sv -->base sv
12 | E_Closed e :
13 X_Closed e -->base e
14 | E_Placeholder x e :
15 X_Placeholder x e -->base e
16 | E_MSelect bs x ys :
17 X_Select (V_Attrset bs) (nonempty_cons x ys) -->base
18 X_Select (X_Select (V_Attrset bs) (nonempty_singleton x)) ys
19 | E_Select e bs x :
20 X_Select (V_Attrset (<[x := e]>bs)) (nonempty_singleton x) -->base e
21 | E_SelectOr bs x e :
22 X_SelectOr (V_Attrset bs) (nonempty_singleton x) e -->base
23 X_Cond (X_HasAttr (V_Attrset bs) x)
24 (* if true *)
25 (X_Select (V_Attrset bs) (nonempty_singleton x))
26 (* if false *)
27 e
28 | E_MSelectOr bs x ys e :
29 X_SelectOr (V_Attrset bs) (nonempty_cons x ys) e -->base
30 X_Cond (X_HasAttr (V_Attrset bs) x)
31 (* if true *)
32 (X_SelectOr
33 (X_Select (V_Attrset bs) (nonempty_singleton x))
34 ys e)
35 (* if false *)
36 e
37 | E_Rec bs :
38 X_Attrset bs -->base V_Attrset (rec_subst bs)
39 | E_Let e bs :
40 X_LetBinding bs e -->base subst (closed (rec_subst bs)) e
41 | E_With e bs :
42 X_Incl (V_Attrset bs) e -->base subst (placeholders bs) e
43 | E_WithNoAttrset v1 e2 :
44 ¬ attrset v1 →
45 X_Incl v1 e2 -->base e2
46 | E_ApplySimple x e1 e2 :
47 X_Apply (V_Fn x e1) e2 -->base subst {[x := X_Closed e2]} e1
48 | E_ApplyAttrset m e bs bs' :
49 bs ~ m ~> bs' →
50 X_Apply (V_AttrsetFn m e) (V_Attrset bs) -->base
51 X_LetBinding bs' e
52 | E_ApplyFunctor e1 e2 bs :
53 X_Apply (V_Attrset (<["__functor" := e2]>bs)) e1 -->base
54 X_Apply (X_Apply e2 (V_Attrset (<["__functor" := e2]>bs))) e1
55 | E_IfTrue e2 e3 :
56 X_Cond true e2 e3 -->base e2
57 | E_IfFalse e2 e3 :
58 X_Cond false e2 e3 -->base e3
59 | E_Op op v1 v2 u :
60 v1 ⟦op⟧ v2 -⊚-> u →
61 X_Op op v1 v2 -->base u
62 | E_OpHasAttrTrue bs x :
63 is_Some (bs !! x) →
64 X_HasAttr (V_Attrset bs) x -->base true
65 | E_OpHasAttrFalse bs x :
66 bs !! x = None →
67 X_HasAttr (V_Attrset bs) x -->base false
68 | E_OpHasAttrNoAttrset v x :
69 ¬ attrset v →
70 X_HasAttr v x -->base false
71 | E_Assert e2 :
72 X_Assert true e2 -->base e2
73where "e -->base e'" := (base_step e e').
74
75Notation "e '-->base*' e'" := (rtc base_step e e')
76 (right associativity, at level 55).
77
78Hint Constructors base_step : core.
79
80Variant is_ctx_item : bool → bool → (expr → expr) → Prop :=
81 | IsCtxItem_Select uf_ext xs :
82 is_ctx_item uf_ext false (λ e1, X_Select e1 xs)
83 | IsCtxItem_SelectOr uf_ext xs e2 :
84 is_ctx_item uf_ext false (λ e1, X_SelectOr e1 xs e2)
85 | IsCtxItem_Incl uf_ext e2 :
86 is_ctx_item uf_ext false (λ e1, X_Incl e1 e2)
87 | IsCtxItem_ApplyL uf_ext e2 :
88 is_ctx_item uf_ext false (λ e1, X_Apply e1 e2)
89 | IsCtxItem_ApplyAttrsetR uf_ext m e1 :
90 is_ctx_item uf_ext false (λ e2, X_Apply (V_AttrsetFn m e1) e2)
91 | IsCtxItem_CondL uf_ext e2 e3 :
92 is_ctx_item uf_ext false (λ e1, X_Cond e1 e2 e3)
93 | IsCtxItem_AssertL uf_ext e2 :
94 is_ctx_item uf_ext false (λ e1, X_Assert e1 e2)
95 | IsCtxItem_OpL uf_ext op e2 :
96 is_ctx_item uf_ext false (λ e1, X_Op op e1 e2)
97 | IsCtxItem_OpR uf_ext op v1 :
98 is_ctx_item uf_ext false (λ e2, X_Op op (X_V v1) e2)
99 | IsCtxItem_OpHasAttrL uf_ext x :
100 is_ctx_item uf_ext false (λ e, X_HasAttr e x)
101 | IsCtxItem_Force uf_ext :
102 is_ctx_item uf_ext true (λ e, X_Force e)
103 | IsCtxItem_ForceAttrset bs x :
104 is_ctx_item true true (λ e, X_V (V_Attrset (<[x := e]>bs))).
105
106Hint Constructors is_ctx_item : core.
107
108Inductive is_ctx : bool → bool → (expr → expr) → Prop :=
109 | IsCtx_Id uf : is_ctx uf uf id
110 | IsCtx_Compose E1 E2 uf_int uf_aux uf_ext :
111 is_ctx_item uf_ext uf_aux E1 →
112 is_ctx uf_aux uf_int E2 →
113 is_ctx uf_ext uf_int (E1 ∘ E2).
114
115Hint Constructors is_ctx : core.
116
117(* /--> This is required because the standard library definition of "-->"
118 | (in Coq.Classes.Morphisms, for `respectful`) defines that this operator
119 | uses right associativity. Our definition must match exactly, as Coq
120 | will give an error otherwise.
121 \-------------------------------------\
122 | | *)
123Reserved Infix "-->" (right associativity, at level 55).
124
125Variant step : expr → expr → Prop :=
126 E_Ctx e1 e2 E uf_int :
127 is_ctx false uf_int E →
128 e1 -->base e2 →
129 E e1 --> E e2
130where "e --> e'" := (step e e').
131
132Hint Constructors step : core.
133
134Notation "e '-->*' e'" := (rtc step e e') (right associativity, at level 55).
135
136(** Theories for contexts *)
137
138Lemma is_ctx_once uf_ext uf_int E :
139 is_ctx_item uf_ext uf_int E → is_ctx uf_ext uf_int E.
140Proof. intros. eapply IsCtx_Compose; [done | constructor]. Qed.
141
142Lemma is_ctx_item_ext_imp E uf_int :
143 is_ctx_item false uf_int E → is_ctx_item true uf_int E.
144Proof. intros H. inv H; constructor. Qed.
145
146Lemma is_ctx_ext_imp E1 E2 uf_aux uf_int :
147 is_ctx_item false uf_aux E1 →
148 is_ctx uf_aux uf_int E2 →
149 is_ctx true uf_int (E1 ∘ E2).
150Proof.
151 intros H1 H2.
152 revert E1 H1.
153 induction H2; intros.
154 - inv H1; eapply IsCtx_Compose; constructor.
155 - eapply IsCtx_Compose.
156 + by apply is_ctx_item_ext_imp in H1.
157 + by eapply IsCtx_Compose.
158Qed.
159
160Lemma is_ctx_uf_false_impl_true E uf_int :
161 is_ctx false uf_int E →
162 is_ctx true uf_int E ∨ E = id.
163Proof.
164 intros Hctx. inv Hctx.
165 - by right.
166 - left. eapply is_ctx_ext_imp; [apply H | apply H0].
167Qed.
diff --git a/semprop.v b/semprop.v
new file mode 100644
index 0000000..3af718d
--- /dev/null
+++ b/semprop.v
@@ -0,0 +1,426 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import gmap option tactics.
3From mininix Require Import binop expr maptools matching relations sem.
4
5Lemma ctx_item_inj E uf_ext uf_int :
6 is_ctx_item uf_ext uf_int E →
7 Inj (=) (=) E.
8Proof.
9 intros Hctx.
10 destruct Hctx; intros e1' e2' Hinj; try congruence.
11 injection Hinj as Hinj.
12 by apply map_insert_rev_1_L in Hinj.
13Qed.
14
15Global Instance id_inj {A} : Inj (=) (=) (@id A).
16Proof. by unfold Inj. Qed.
17
18Lemma ctx_inj E uf_ext uf_int :
19 is_ctx uf_ext uf_int E →
20 Inj (=) (=) E.
21Proof.
22 intros Hctx.
23 induction Hctx.
24 - apply id_inj.
25 - apply ctx_item_inj in H.
26 by apply compose_inj with (=).
27Qed.
28
29Lemma base_step_deterministic : deterministic base_step.
30Proof.
31 unfold deterministic.
32 intros e0 e1 e2 H1 H2.
33 inv H1; inv H2; try done.
34 - destruct ys, ys0. by simplify_eq/=.
35 - destruct ys. by simplify_eq/=.
36 - destruct ys. by simplify_eq/=.
37 - apply map_insert_inv in H0. by destruct H0.
38 - destruct ys. by simplify_eq/=.
39 - destruct ys. by simplify_eq/=.
40 - destruct ys, ys0. by simplify_eq/=.
41 - exfalso. apply H3. by exists bs.
42 - exfalso. apply H. by exists bs.
43 - f_equal. by eapply matches_deterministic.
44 - apply map_insert_inv in H0 as [H01 H02].
45 by simplify_eq /=.
46 - f_equal. by eapply binop_deterministic.
47 - rewrite H4 in H. by apply is_Some_None in H.
48 - exfalso. apply H4. by exists bs.
49 - rewrite H in H4. by apply is_Some_None in H4.
50 - exfalso. apply H. by exists bs.
51Qed.
52
53Reserved Notation "e '-/' uf '/->' e'" (right associativity, at level 55).
54
55Inductive fstep : bool → expr → expr → Prop :=
56 | F_Ctx e1 e2 E uf_ext uf_int :
57 is_ctx uf_ext uf_int E →
58 e1 -->base e2 →
59 E e1 -/uf_ext/-> E e2
60where "e -/ uf /-> e'" := (fstep uf e e').
61
62Hint Constructors fstep : core.
63
64Lemma ufstep e e' : e -/false/-> e' ↔ e --> e'.
65Proof. split; intros; inv H; by econstructor. Qed.
66
67Lemma fstep_strongly_confluent_aux x uf y1 y2 :
68 x -/uf/-> y1 →
69 x -/uf/-> y2 →
70 y1 = y2 ∨ ∃ z, y1 -/uf/-> z ∧ y2 -/uf/-> z.
71Proof.
72 intros Hstep1 Hstep2.
73 inv Hstep1 as [b11 b12 E1 uf_int uf_int1 Hctx1 Hbase1].
74 inv Hstep2 as [b21 b22 E2 uf_int uf_int2 Hctx2 Hbase2].
75 revert b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H0.
76 induction Hctx1 as [|E1 E0];
77 intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2.
78 - (* L: id, R: id *) left. by eapply base_step_deterministic.
79 - (* L: id, R: ∘ *) simplify_eq/=.
80 inv H.
81 + inv Hbase1.
82 * inv H0.
83 -- inv Hbase2.
84 -- inv H.
85 * inv H0.
86 -- inv Hbase2.
87 -- inv H1. inv H.
88 + inv Hbase1.
89 * inv H0.
90 -- inv Hbase2.
91 -- inv H.
92 * inv H0.
93 -- inv Hbase2.
94 -- inv H.
95 + inv Hbase1.
96 * inv H0.
97 -- inv Hbase2.
98 -- inv H.
99 * inv H0.
100 -- inv Hbase2.
101 -- inv H1.
102 + inv Hbase1.
103 * inv H0.
104 -- inv Hbase2.
105 -- inv H.
106 * inv H0.
107 -- inv Hbase2.
108 -- inv H1.
109 * inv H0.
110 -- inv Hbase2.
111 -- inv H1. inv H.
112 + inv Hbase1.
113 inv H0.
114 * inv Hbase2.
115 * inv H.
116 + inv Hbase1.
117 * inv H0.
118 -- inv Hbase2.
119 -- inv H.
120 * inv H0.
121 -- inv Hbase2.
122 -- inv H.
123 + inv Hbase1.
124 inv H0.
125 * inv Hbase2.
126 * inv H.
127 + inv Hbase1.
128 inv H0.
129 * inv Hbase2.
130 * inv H.
131 + inv Hbase1.
132 inv H0.
133 * inv Hbase2.
134 * inv H.
135 + inv Hbase1.
136 * inv H0.
137 -- inv Hbase2.
138 -- inv H1.
139 * inv H0.
140 -- inv Hbase2.
141 -- inv H1.
142 * inv H0.
143 -- inv Hbase2.
144 -- inv H1.
145 + inv Hbase1.
146 inv H0.
147 * inv Hbase2.
148 * inv H.
149 simplify_option_eq.
150 destruct sv; try discriminate.
151 exfalso. clear uf. simplify_option_eq.
152 apply fmap_insert_lookup in H1. simplify_option_eq.
153 revert bs0 x H H1 Heqo.
154 induction H2; intros bs0 x H' H1 Heqo.
155 -- inv Hbase2.
156 -- simplify_option_eq.
157 inv H. destruct H'; try discriminate.
158 inv H1. apply fmap_insert_lookup in H0. simplify_option_eq.
159 by eapply IHis_ctx.
160 + inv Hbase1.
161 - (* L: ∘, R: id *)
162 simplify_eq/=.
163 inv H.
164 + inv Hbase2.
165 * inv Hctx1.
166 -- inv Hbase1.
167 -- inv H.
168 * inv Hctx1.
169 -- inv Hbase1.
170 -- inv H0. inv H.
171 + inv Hbase2.
172 * inv Hctx1.
173 -- inv Hbase1.
174 -- inv H.
175 * inv Hctx1.
176 -- inv Hbase1.
177 -- inv H.
178 + inv Hbase2.
179 * inv Hctx1.
180 -- inv Hbase1.
181 -- inv H.
182 * inv Hctx1.
183 -- inv Hbase1.
184 -- inv H0.
185 + inv Hbase2.
186 * inv Hctx1.
187 -- inv Hbase1.
188 -- inv H.
189 * inv Hctx1.
190 -- inv Hbase1.
191 -- inv H0.
192 * inv Hctx1.
193 -- inv Hbase1.
194 -- inv H0. inv H.
195 + inv Hbase2.
196 inv Hctx1.
197 * inv Hbase1.
198 * inv H.
199 + inv Hbase2.
200 * inv Hctx1.
201 -- inv Hbase1.
202 -- inv H.
203 * inv Hctx1.
204 -- inv Hbase1.
205 -- inv H.
206 + inv Hbase2.
207 inv Hctx1.
208 * inv Hbase1.
209 * inv H.
210 + inv Hbase2.
211 inv Hctx1.
212 * inv Hbase1.
213 * inv H.
214 + inv Hbase2.
215 inv Hctx1.
216 * inv Hbase1.
217 * inv H.
218 + inv Hbase2.
219 * inv Hctx1.
220 -- inv Hbase1.
221 -- inv H0.
222 * inv Hctx1.
223 -- inv Hbase1.
224 -- inv H0.
225 * inv Hctx1.
226 -- inv Hbase1.
227 -- inv H0.
228 + inv Hbase2.
229 inv Hctx1.
230 * inv Hbase1.
231 * clear IHHctx1.
232 inv H.
233 simplify_option_eq.
234 destruct sv; try discriminate.
235 exfalso. simplify_option_eq.
236 apply fmap_insert_lookup in H0. simplify_option_eq.
237 revert bs0 x H H0 Heqo.
238 induction H1; intros bs0 x H' H0 Heqo.
239 -- inv Hbase1.
240 -- simplify_option_eq.
241 inv H. destruct H'; try discriminate.
242 inv H0. apply fmap_insert_lookup in H2. simplify_option_eq.
243 eapply IHis_ctx.
244 ++ apply H2.
245 ++ apply Heqo0.
246 + inv Hbase2.
247 - (* L: ∘, R: ∘ *)
248 simplify_option_eq.
249 inv H; inv H0.
250 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
251 as [IH | [z [IHz1 IHz2]]].
252 * left. congruence.
253 * right. exists (X_Select z xs).
254 split; [inv IHz1 | inv IHz2];
255 eapply F_Ctx with (E := (λ e, X_Select e xs) ∘ E); try done;
256 by eapply IsCtx_Compose.
257 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
258 as [IH | [z [IHz1 IHz2]]].
259 * left. congruence.
260 * right. exists (X_SelectOr z xs e2).
261 split; [inv IHz1 | inv IHz2];
262 eapply F_Ctx with (E := (λ e1, X_SelectOr e1 xs e2) ∘ E); try done;
263 by eapply IsCtx_Compose.
264 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
265 as [IH | [z [IHz1 IHz2]]].
266 * left. congruence.
267 * right. exists (X_Incl z e2).
268 split; [inv IHz1 | inv IHz2];
269 eapply F_Ctx with (E := (λ e1, X_Incl e1 e2) ∘ E); try done;
270 by eapply IsCtx_Compose.
271 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
272 as [IH | [z [IHz1 IHz2]]].
273 * left. congruence.
274 * right. exists (X_Apply z e2).
275 split; [inv IHz1 | inv IHz2];
276 eapply F_Ctx with (E := (λ e1, X_Apply e1 e2) ∘ E); try done;
277 by eapply IsCtx_Compose.
278 + inv Hctx1; simplify_option_eq.
279 * inv Hbase1.
280 * inv H.
281 + inv H1; simplify_option_eq.
282 * inv Hbase2.
283 * inv H.
284 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H0)
285 as [IH | [z [IHz1 IHz2]]].
286 * left. congruence.
287 * right. exists (X_Apply (V_AttrsetFn m e1) z).
288 split; [inv IHz1 | inv IHz2];
289 eapply F_Ctx with (E := (λ e2, X_Apply (V_AttrsetFn m e1) e2) ∘ E);
290 try done;
291 by eapply IsCtx_Compose.
292 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
293 as [IH | [z [IHz1 IHz2]]].
294 * left. congruence.
295 * right. exists (X_Cond z e2 e3).
296 split; [inv IHz1 | inv IHz2];
297 eapply F_Ctx with (E := (λ e1, X_Cond e1 e2 e3) ∘ E); try done;
298 by eapply IsCtx_Compose.
299 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
300 as [IH | [z [IHz1 IHz2]]].
301 * left. congruence.
302 * right. exists (X_Assert z e2).
303 split; [inv IHz1 | inv IHz2];
304 eapply F_Ctx with (E := (λ e1, X_Assert e1 e2) ∘ E); try done;
305 by eapply IsCtx_Compose.
306 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H)
307 as [IH | [z [IHz1 IHz2]]].
308 * left. congruence.
309 * right. exists (X_Op op z e2).
310 split; [inv IHz1 | inv IHz2];
311 eapply F_Ctx with (E := (λ e1, X_Op op e1 e2) ∘ E); try done;
312 by eapply IsCtx_Compose.
313 + inv Hctx1; simplify_option_eq.
314 * inv Hbase1.
315 * inv H0.
316 + inv H1; simplify_option_eq.
317 * inv Hbase2.
318 * inv H0.
319 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H0)
320 as [IH | [z [IHz1 IHz2]]].
321 * left. congruence.
322 * right. exists (X_Op op v1 z).
323 split; [inv IHz1 | inv IHz2];
324 eapply F_Ctx with (E := (λ e2, X_Op op v1 e2) ∘ E); try done;
325 by eapply IsCtx_Compose.
326 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
327 as [IH | [z [IHz1 IHz2]]].
328 * left. congruence.
329 * right. exists (X_HasAttr z x).
330 split; [inv IHz1 | inv IHz2];
331 eapply F_Ctx with (E := (λ e, X_HasAttr e x) ∘ E); try done;
332 by eapply IsCtx_Compose.
333 + destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
334 as [IH | [z [IHz1 IHz2]]].
335 * left. congruence.
336 * right. exists (X_Force z).
337 split.
338 -- inv IHz1.
339 (* apply is_ctx_uf_false_impl_true in H0 as []. *)
340 eapply F_Ctx with (E := X_Force ∘ E); try done;
341 by eapply IsCtx_Compose.
342 -- inv IHz2.
343 eapply F_Ctx with (E := X_Force ∘ E); try done;
344 by eapply IsCtx_Compose.
345 + destruct (decide (x0 = x)).
346 * simplify_option_eq.
347 apply map_insert_rev_L in H2 as [H21 H22].
348 destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H21)
349 as [IH | [z [IHz1 IHz2]]].
350 -- left. rewrite IH. do 2 f_equal.
351 by apply map_insert_L.
352 -- right. exists (V_Attrset (<[x := z]>bs)).
353 split.
354 ++ inv IHz1.
355 eapply F_Ctx
356 with (E := (λ e, X_V $ V_Attrset (<[x := e]>bs)) ∘ E); try done.
357 by eapply IsCtx_Compose.
358 ++ inv IHz2.
359 rewrite (map_insert_L _ _ _ _ _ (eq_refl (E e1)) H22).
360 eapply F_Ctx
361 with (E := (λ e, X_V $ V_Attrset (<[x := e]>bs)) ∘ E); try done.
362 by eapply IsCtx_Compose.
363 * simplify_option_eq.
364 right. exists (V_Attrset (<[x := E0 b12]>(<[x0 := E4 b22]>bs))).
365 split.
366 -- apply map_insert_ne_inv in H2 as H3; try done.
367 destruct H3.
368 replace bs with (<[x0 := E4 b21]>bs) at 1; try by rewrite insert_id.
369 setoid_rewrite insert_commute; try by congruence.
370 eapply F_Ctx
371 with (E := (λ e, X_V $ V_Attrset
372 (<[x0 := e]>(<[x := E0 b12]> bs))) ∘ E4).
373 ++ by eapply IsCtx_Compose.
374 ++ done.
375 -- apply map_insert_ne_inv in H2 as H3; try done.
376 destruct H3 as [H31 [H32 H33]].
377 replace bs0 with (<[x := E0 b11]>bs0) at 1;
378 try by rewrite insert_id.
379 rewrite insert_commute; try by congruence.
380 replace (<[x:=E0 b11]> (<[x0:=E4 b22]> bs0))
381 with (<[x:=E0 b11]> (<[x0:=E4 b22]> bs)).
382 2: {
383 rewrite <-insert_delete_insert.
384 setoid_rewrite <-insert_delete_insert at 2.
385 rewrite delete_insert_ne by congruence.
386 rewrite delete_commute. rewrite <-H33.
387 rewrite insert_delete_insert.
388 rewrite <-delete_insert_ne by congruence.
389 by rewrite insert_delete_insert.
390 }
391 eapply F_Ctx with (E := (λ e, X_V $ V_Attrset
392 (<[x := e]>(<[x0 := E4 b22]>bs))) ∘ E0).
393 ++ by eapply IsCtx_Compose.
394 ++ done.
395Qed.
396
397Lemma step_strongly_confluent_aux x y1 y2 :
398 x --> y1 →
399 x --> y2 →
400 y1 = y2 ∨ ∃ z, y1 --> z ∧ y2 --> z.
401Proof.
402 intros Hstep1 Hstep2.
403 apply ufstep in Hstep1, Hstep2.
404 destruct (fstep_strongly_confluent_aux _ _ _ _ Hstep1 Hstep2) as [|[?[]]].
405 - by left.
406 - right. exists x0. split; by apply ufstep.
407Qed.
408
409Theorem step_strongly_confluent : strongly_confluent step.
410Proof.
411 intros x y1 y2 Hy1 Hy2.
412 destruct (step_strongly_confluent_aux x y1 y2 Hy1 Hy2) as [|[z [Hz1 Hz2]]].
413 - exists y1. by subst.
414 - exists z. split.
415 + by apply rtc_once.
416 + by apply rc_once.
417Qed.
418
419Lemma step_semi_confluent : semi_confluent step.
420Proof. apply strong__semi_confluence. apply step_strongly_confluent. Qed.
421
422Lemma step_cr : cr step.
423Proof. apply semi_confluence__cr. apply step_semi_confluent. Qed.
424
425Theorem step_confluent : confluent step.
426Proof. apply confluent_alt. apply step_cr. Qed.
diff --git a/shared.v b/shared.v
new file mode 100644
index 0000000..8e9484f
--- /dev/null
+++ b/shared.v
@@ -0,0 +1,66 @@
1Require Import Coq.NArith.BinNat.
2Require Import Coq.Strings.Ascii.
3Require Import Coq.Strings.String.
4From stdpp Require Import fin_sets gmap option.
5From mininix Require Import expr maptools.
6
7Open Scope string_scope.
8Open Scope N_scope.
9Open Scope Z_scope.
10Open Scope nat_scope.
11
12Definition nonrecs : gmap string b_rhs → gmap string expr :=
13 omap (λ b, match b with B_Nonrec e => Some e | _ => None end).
14
15Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs.
16Proof.
17 induction bs using map_ind.
18 - done.
19 - unfold nonrecs.
20 rewrite fmap_insert.
21 rewrite omap_insert_Some with (y := x); try done.
22 by f_equal.
23Qed.
24
25Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs.
26Proof.
27 unfold rec_subst.
28 rewrite <-map_fmap_compose.
29 unfold compose.
30 by rewrite map_fmap_id.
31Qed.
32
33Definition ascii_ltb (c1 c2 : ascii) : bool :=
34 bool_decide (N_of_ascii c1 < N_of_ascii c2)%N.
35
36Fixpoint string_lt (s1 s2 : string) : bool :=
37 match s1, s2 with
38 | _, EmptyString => false
39 | EmptyString, String _ _ => true
40 | String c1 s1', String c2 s2' => ascii_ltb c1 c2 || string_lt s1' s2'
41 end.
42
43Fixpoint expr_eq (e1 e2 : expr) : bool :=
44 match e1, e2 with
45 | V_Null, V_Null => false
46 | V_Bool b1, V_Bool b2 => bool_decide (b1 = b2)
47 | V_Int n1, V_Int n2 => bool_decide (n1 = n2)
48 | V_Str s1, V_Str s2 => bool_decide (s1 = s2)
49 | V_Attrset bs1, V_Attrset bs2 => bool_decide (dom bs1 = dom bs2) &&
50 map_fold (λ x e1' acc, match bs2 !! x with
51 | None => false
52 | Some e2' => acc && expr_eq e1' e2'
53 end) true bs1
54 | _, _ => false
55 end.
56
57Definition prelude : gmap string expr :=
58 {[ "true" := X_V true;
59 "false" := X_V false;
60 "null" := X_V V_Null;
61 "builtins" := X_Attrset
62 {[ "true" := B_Nonrec true;
63 "false" := B_Nonrec false;
64 "null" := B_Nonrec V_Null
65 ]}
66 ]}.
diff --git a/sound.v b/sound.v
new file mode 100644
index 0000000..761d7ad
--- /dev/null
+++ b/sound.v
@@ -0,0 +1,630 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import base gmap relations tactics.
3From mininix Require Import
4 binop expr interpreter maptools matching relations sem.
5
6Lemma strong_value_stuck sv : ¬ ∃ e, expr_from_strong_value sv --> e.
7Proof.
8 intros []. destruct sv; inv H; inv H1;
9 simplify_option_eq; (try inv H2); inv H.
10Qed.
11
12Lemma strong_value_stuck_rtc sv e:
13 expr_from_strong_value sv -->* e →
14 e = expr_from_strong_value sv.
15Proof.
16 intros. inv H.
17 - reflexivity.
18 - exfalso. apply strong_value_stuck with (sv := sv). by exists y.
19Qed.
20
21Lemma force__strong_value (e : expr) (v : value) :
22 X_Force e -->* v →
23 ∃ sv, v = value_from_strong_value sv.
24Proof.
25 intros [n Hsteps] % rtc_nsteps.
26 revert e v Hsteps.
27 induction n; intros e v Hsteps; inv Hsteps.
28 inv H0. inv H2; simplify_eq/=.
29 - inv H3.
30 exists sv.
31 apply rtc_nsteps_2 in H1.
32 apply strong_value_stuck_rtc in H1.
33 unfold expr_from_strong_value, compose in H1.
34 congruence.
35 - inv H0.
36 destruct (IHn _ _ H1) as [sv Hsv].
37 by exists sv.
38Qed.
39
40Lemma forall2_force__strong_values es (vs : gmap string value) :
41 map_Forall2 (λ e v', X_Force e -->* X_V v') es vs →
42 ∃ svs, vs = value_from_strong_value <$> svs.
43Proof.
44 revert vs.
45 induction es using map_ind; intros vs HForall2.
46 - apply map_Forall2_empty_l_L in HForall2. by exists ∅.
47 - destruct (map_Forall2_destruct _ _ _ _ _ HForall2)
48 as [v [m2' [Him2' Heqvs]]]. simplify_eq/=.
49 apply map_Forall2_insert_inv_strict in HForall2
50 as [Hstep HForall2]; try done.
51 apply IHes in HForall2 as [svs Hsvs]. simplify_eq/=.
52 apply force__strong_value in Hstep as [sv Hsv]. simplify_eq/=.
53 exists (<[i := sv]>svs). by rewrite fmap_insert.
54Qed.
55
56Lemma force_strong_value_forall2_impl es (svs : gmap string strong_value) :
57 map_Forall2 (λ e v', X_Force e -->* X_V v')
58 es (value_from_strong_value <$> svs) →
59 map_Forall2 (λ e sv', X_Force e -->* expr_from_strong_value sv') es svs.
60Proof. apply map_Forall2_fmap_r_L. Qed.
61
62Lemma force_map_fmap_union_insert (sws : gmap string strong_value) es k e sv :
63 X_Force e -->* expr_from_strong_value sv →
64 X_Force (X_V (V_Attrset (<[k := e]>es ∪
65 (expr_from_strong_value <$> sws)))) -->*
66 X_Force (X_V (V_Attrset (<[k := expr_from_strong_value sv]>es ∪
67 (expr_from_strong_value <$> sws)))).
68Proof.
69 intros [n Hsteps] % rtc_nsteps.
70 revert sws es k e Hsteps.
71 induction n; intros sws es k e Hsteps.
72 - inv Hsteps.
73 - inv Hsteps.
74 inv H0.
75 inv H2.
76 + inv H3. inv H1.
77 * simplify_option_eq. unfold expr_from_strong_value, compose.
78 by rewrite H4.
79 * edestruct strong_value_stuck. exists y. done.
80 + inv H0. simplify_option_eq.
81 apply rtc_transitive
82 with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪
83 (expr_from_strong_value <$> sws))))).
84 * do 2 rewrite <-insert_union_l.
85 apply rtc_once.
86 eapply E_Ctx
87 with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪
88 (expr_from_strong_value <$> sws)))))).
89 -- eapply IsCtx_Compose.
90 ++ constructor.
91 ++ eapply IsCtx_Compose
92 with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪
93 (expr_from_strong_value <$> sws)))))).
94 ** constructor.
95 ** done.
96 -- done.
97 * by apply IHn.
98Qed.
99
100Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x
101 (m1 : gmap string B) (m2 : gmap string A) :
102 m1 !! i = None →
103 <[i := f x]>m1 ∪ (f <$> m2) = m1 ∪ (f <$> <[i := x]>m2).
104Proof.
105 intros Him1.
106 rewrite fmap_insert.
107 rewrite <-insert_union_l.
108 by rewrite <-insert_union_r.
109Qed.
110
111Lemma fmap_insert_union__fmap_union_insert {A B} (f : A → B) i x
112 (m1 : gmap string A) (m2 : gmap string A) :
113 m1 !! i = None →
114 f <$> <[i := x]>m1 ∪ m2 = f <$> m1 ∪ <[i := x]>m2.
115Proof.
116 intros Him1.
117 do 2 rewrite map_fmap_union.
118 rewrite 2 fmap_insert.
119 rewrite <-insert_union_l.
120 rewrite <-insert_union_r; try done.
121 rewrite lookup_fmap.
122 by rewrite Him1.
123Qed.
124
125Lemma force_map_fmap_union (sws svs : gmap string strong_value) es :
126 map_Forall2 (λ e sv, X_Force e -->* expr_from_strong_value sv) es svs →
127 X_Force (X_V (V_Attrset (es ∪ (expr_from_strong_value <$> sws)))) -->*
128 X_Force (X_V (V_Attrset (expr_from_strong_value <$> svs ∪ sws))).
129Proof.
130 revert sws svs.
131 induction es using map_ind; intros sws svs HForall2.
132 - apply map_Forall2_empty_l_L in HForall2.
133 subst. by do 2 rewrite map_empty_union.
134 - apply map_Forall2_destruct in HForall2 as HForall2'.
135 destruct HForall2' as [sv [svs' [Him2' Heqm2']]]. subst.
136 apply map_Forall2_insert_inv_strict
137 in HForall2 as [HForall21 HForall22]; try done.
138 apply rtc_transitive with (X_Force
139 (X_V (V_Attrset (<[i := expr_from_strong_value sv]> m ∪
140 (expr_from_strong_value <$> sws))))).
141 + by apply force_map_fmap_union_insert.
142 + rewrite insert_union_fmap__union_fmap_insert by done.
143 rewrite fmap_insert_union__fmap_union_insert by done.
144 by apply IHes.
145Qed.
146
147(* See 194+2024-0525-2305 for proof sketch *)
148Lemma force_map_fmap (svs : gmap string strong_value) (es : gmap string expr) :
149 map_Forall2 (λ e sv, X_Force e -->* expr_from_strong_value sv) es svs →
150 X_Force (X_V (V_Attrset es)) -->*
151 X_Force (X_V (V_Attrset (expr_from_strong_value <$> svs))).
152Proof.
153 pose proof (force_map_fmap_union ∅ svs es).
154 rewrite fmap_empty in H. by do 2 rewrite map_union_empty in H.
155Qed.
156
157Lemma id_compose_l {A B} (f : A → B) : id ∘ f = f.
158Proof. done. Qed.
159
160Lemma is_ctx_trans uf_ext uf_aux uf_int E1 E2 :
161 is_ctx uf_ext uf_aux E1 →
162 is_ctx uf_aux uf_int E2 →
163 is_ctx uf_ext uf_int (E1 ∘ E2).
164Proof.
165 intros.
166 induction H.
167 - induction H0.
168 + apply IsCtx_Id.
169 + rewrite id_compose_l.
170 by apply IsCtx_Compose with uf_aux.
171 - apply IHis_ctx in H0.
172 replace (E1 ∘ E0 ∘ E2) with (E1 ∘ (E0 ∘ E2)) by done.
173 by apply IsCtx_Compose with uf_aux.
174Qed.
175
176Lemma ctx_mstep e e' E :
177 e -->* e' → is_ctx false false E → E e -->* E e'.
178Proof.
179 intros.
180 induction H.
181 - apply rtc_refl.
182 - inv H.
183 pose proof (is_ctx_trans false false uf_int E E0 H0 H2).
184 eapply rtc_l.
185 + replace (E (E0 e1)) with ((E ∘ E0) e1) by done.
186 eapply E_Ctx; [apply H | apply H3].
187 + assumption.
188Qed.
189
190Definition is_nonempty_ctx (uf_ext uf_int : bool) (E : expr → expr) :=
191 ∃ E1 E2 uf_aux,
192 is_ctx_item uf_ext uf_aux E1 ∧
193 is_ctx uf_aux uf_int E2 ∧ E = E1 ∘ E2.
194
195Lemma nonempty_ctx_mstep e e' uf_int E :
196 e -->* e' → is_nonempty_ctx false uf_int E → E e -->* E e'.
197Proof.
198 intros Hmstep Hctx.
199 destruct Hctx as [E1 [E2 [uf_aux [Hctx1 [Hctx2 Hctx3]]]]].
200 simplify_option_eq.
201 induction Hmstep.
202 + apply rtc_refl.
203 + apply rtc_l with (y := (E1 ∘ E2) y).
204 * inv H.
205 destruct (is_ctx_uf_false_impl_true E uf_int0 H0).
206 +++ apply E_Ctx with (E := E1 ∘ (E2 ∘ E)) (uf_int := uf_int0).
207 ++ eapply IsCtx_Compose.
208 ** apply Hctx1.
209 ** eapply is_ctx_trans.
210 --- apply Hctx2.
211 --- destruct uf_int; assumption.
212 ++ assumption.
213 +++ apply E_Ctx with (E := E1 ∘ (E2 ∘ E)) (uf_int := uf_int).
214 ++ eapply IsCtx_Compose.
215 ** apply Hctx1.
216 ** eapply is_ctx_trans; simplify_option_eq.
217 --- apply Hctx2.
218 --- constructor.
219 ++ assumption.
220 * apply IHHmstep.
221Qed.
222
223Lemma force_strong_value (sv : strong_value) :
224 X_Force sv -->* sv.
225Proof.
226 destruct sv using strong_value_ind';
227 apply rtc_once; eapply E_Ctx with (E := id); constructor.
228Qed.
229
230Lemma id_compose_r {A B} (f : A → B) : f ∘ id = f.
231Proof. done. Qed.
232
233Lemma force_idempotent e (v' : value) :
234 X_Force e -->* v' →
235 X_Force (X_Force e) -->* v'.
236Proof.
237 intros H.
238 destruct (force__strong_value _ _ H) as [sv Hsv]. subst.
239 apply rtc_transitive with (y := X_Force sv).
240 * eapply nonempty_ctx_mstep; try assumption.
241 rewrite <-id_compose_r.
242 exists X_Force, id, true.
243 repeat (split || constructor || done).
244 * apply force_strong_value.
245Qed.
246
247(* Conditional force *)
248Definition cforce (uf : bool) e := if uf then X_Force e else e.
249
250Lemma cforce_strong_value uf (sv : strong_value) :
251 cforce uf sv -->* sv.
252Proof. destruct uf; try done. apply force_strong_value. Qed.
253
254Theorem eval_sound_strong n uf e v' :
255 eval n uf e = Some v' →
256 cforce uf e -->* v'.
257Proof.
258 revert uf e v'.
259 induction n; intros uf e v' Heval.
260 - discriminate.
261 - destruct e; rewrite eval_S in Heval; simplify_option_eq; try done.
262 + (* X_V *)
263 case_match; simplify_option_eq.
264 * (* V_Bool *)
265 replace (V_Bool p) with (value_from_strong_value (SV_Bool p)) by done.
266 apply cforce_strong_value.
267 * (* V_Null *)
268 replace V_Null with (value_from_strong_value SV_Null) by done.
269 apply cforce_strong_value.
270 * (* V_Int *)
271 replace (V_Int n0) with (value_from_strong_value (SV_Int n0)) by done.
272 apply cforce_strong_value.
273 * (* V_Str *)
274 replace (V_Str s) with (value_from_strong_value (SV_Str s)) by done.
275 apply cforce_strong_value.
276 * (* V_Fn *)
277 replace (V_Fn x e) with (value_from_strong_value (SV_Fn x e)) by done.
278 apply cforce_strong_value.
279 * (* V_AttrsetFn *)
280 replace (V_AttrsetFn m e)
281 with (value_from_strong_value (SV_AttrsetFn m e)) by done.
282 apply cforce_strong_value.
283 * (* V_Attrset *)
284 case_match; simplify_option_eq; try done.
285 apply map_mapM_Some_L in Heqo. simplify_option_eq.
286 eapply map_Forall2_impl_L in Heqo. 2: { intros a b. apply IHn. }
287 destruct (forall2_force__strong_values _ _ Heqo). subst.
288 apply force_strong_value_forall2_impl in Heqo.
289 rewrite <-map_fmap_compose. fold expr_from_strong_value.
290 apply force_map_fmap in Heqo.
291 apply rtc_transitive
292 with (y := X_Force (X_V (V_Attrset (expr_from_strong_value <$> x))));
293 try done.
294 apply rtc_once.
295 eapply E_Ctx with (E := id); [constructor|].
296 replace (X_V (V_Attrset (expr_from_strong_value <$> x)))
297 with (expr_from_strong_value (SV_Attrset x)) by reflexivity.
298 apply E_Force.
299 + (* X_Attrset *)
300 apply IHn in Heval.
301 apply rtc_transitive with (y := cforce uf (V_Attrset (rec_subst bs)));
302 [|done].
303 destruct uf; simplify_eq/=.
304 -- eapply nonempty_ctx_mstep with (E := X_Force).
305 ++ by eapply rtc_once, E_Ctx with (E := id).
306 ++ by exists X_Force, id, true.
307 -- apply rtc_once. by eapply E_Ctx with (E := id).
308 + (* X_LetBinding *)
309 apply IHn in Heval.
310 apply rtc_transitive
311 with (y := cforce uf (subst (closed (rec_subst bs)) e)); [|done].
312 destruct uf; simplify_eq/=.
313 -- eapply nonempty_ctx_mstep with (E := X_Force).
314 ++ by eapply rtc_once, E_Ctx with (E := id).
315 ++ by exists X_Force, id, true.
316 -- apply rtc_once. by eapply E_Ctx with (E := id).
317 + (* X_Select *)
318 case_match. simplify_option_eq.
319 apply IHn in Heqo. simplify_eq/=.
320 apply rtc_transitive with (y := cforce uf
321 (X_Select (V_Attrset H0) (Ne_Cons head tail))).
322 -- apply ctx_mstep
323 with (E := cforce uf ∘ (λ e, X_Select e (Ne_Cons head tail))).
324 ++ done.
325 ++ destruct uf; simplify_option_eq.
326 ** eapply IsCtx_Compose; [constructor | by apply is_ctx_once].
327 ** apply is_ctx_once. unfold compose. by simpl.
328 -- case_match; apply IHn in Heval.
329 ++ apply rtc_transitive with (y := cforce uf H); [|done].
330 apply rtc_once.
331 eapply E_Ctx.
332 ** destruct uf; [by apply is_ctx_once | done].
333 ** by replace H0 with (<[head := H]>H0); [|apply insert_id].
334 ++ apply rtc_transitive
335 with (y := cforce uf (X_Select H (Ne_Cons s l))); [|done].
336 ** eapply rtc_l.
337 --- eapply E_Ctx.
338 +++ destruct uf; [by apply is_ctx_once | done].
339 +++ replace (Ne_Cons head (s :: l))
340 with (nonempty_cons head (Ne_Cons s l)) by done.
341 apply E_MSelect.
342 --- eapply rtc_once.
343 eapply E_Ctx
344 with (E := cforce uf ∘ (λ e, X_Select e (Ne_Cons s l))).
345 +++ destruct uf.
346 *** eapply IsCtx_Compose; [done | by apply is_ctx_once].
347 *** apply is_ctx_once. unfold compose. by simpl.
348 +++ by replace H0
349 with (<[head := H]>H0); [|apply insert_id].
350 + (* X_SelectOr *)
351 case_match. simplify_option_eq.
352 apply IHn in Heqo. simplify_eq/=.
353 apply rtc_transitive
354 with (y := cforce uf (X_SelectOr (V_Attrset H0) (Ne_Cons head tail) e2)).
355 -- apply ctx_mstep
356 with (E := cforce uf ∘ (λ e, X_SelectOr e (Ne_Cons head tail) e2)).
357 ++ done.
358 ++ destruct uf; simplify_option_eq.
359 ** eapply IsCtx_Compose; [constructor | by apply is_ctx_once].
360 ** apply is_ctx_once. unfold compose. by simpl.
361 -- case_match; try case_match; apply IHn in Heval.
362 ++ apply rtc_transitive with (y := cforce uf e); [|done].
363 eapply rtc_l.
364 ** eapply E_Ctx.
365 --- destruct uf; [by apply is_ctx_once | done].
366 --- replace (Ne_Cons head []) with (nonempty_singleton head)
367 by done. constructor.
368 ** eapply rtc_l.
369 --- eapply E_Ctx with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
370 +++ destruct uf; simplify_option_eq.
371 *** eapply IsCtx_Compose;
372 [constructor | by apply is_ctx_once].
373 *** apply is_ctx_once. unfold compose. by simpl.
374 +++ by apply E_OpHasAttrTrue.
375 --- simplify_eq/=.
376 eapply rtc_l.
377 +++ eapply E_Ctx with (E := cforce uf).
378 *** destruct uf; [by apply is_ctx_once | done].
379 *** apply E_IfTrue.
380 +++ eapply rtc_once.
381 eapply E_Ctx with (E := cforce uf).
382 *** destruct uf; [by apply is_ctx_once | done].
383 *** by replace H0 with (<[head := e]>H0);
384 [|apply insert_id].
385 ++ apply rtc_transitive
386 with (y := cforce uf (X_SelectOr e (Ne_Cons s l) e2)); [|done].
387 eapply rtc_l.
388 ** eapply E_Ctx.
389 --- destruct uf; [by apply is_ctx_once | done].
390 --- replace (Ne_Cons head (s :: l))
391 with (nonempty_cons head (Ne_Cons s l)) by done.
392 constructor.
393 ** eapply rtc_l.
394 --- eapply E_Ctx with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
395 +++ destruct uf; simplify_option_eq.
396 *** eapply IsCtx_Compose;
397 [constructor | by apply is_ctx_once].
398 *** apply is_ctx_once. unfold compose. by simpl.
399 +++ by apply E_OpHasAttrTrue.
400 --- simplify_eq/=.
401 eapply rtc_l.
402 +++ eapply E_Ctx with (E := cforce uf).
403 *** destruct uf; [by apply is_ctx_once | done].
404 *** apply E_IfTrue.
405 +++ eapply rtc_once.
406 eapply E_Ctx
407 with (E := cforce uf ∘ λ e1,
408 X_SelectOr e1 (Ne_Cons s l) e2).
409 *** destruct uf; simplify_option_eq.
410 ---- eapply IsCtx_Compose;
411 [constructor | by apply is_ctx_once].
412 ---- apply is_ctx_once. unfold compose. by simpl.
413 *** by replace H0 with (<[head := e]>H0);
414 [|apply insert_id].
415 ++ apply rtc_transitive with (y := cforce uf e2); [|done].
416 destruct tail.
417 ** eapply rtc_l.
418 --- eapply E_Ctx.
419 +++ destruct uf; [by apply is_ctx_once | done].
420 +++ replace (Ne_Cons head [])
421 with (nonempty_singleton head) by done.
422 constructor.
423 --- eapply rtc_l.
424 +++ eapply E_Ctx
425 with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
426 *** destruct uf; simplify_option_eq.
427 ---- eapply IsCtx_Compose;
428 [constructor | by apply is_ctx_once].
429 ---- apply is_ctx_once. unfold compose. by simpl.
430 *** by apply E_OpHasAttrFalse.
431 +++ simplify_eq/=.
432 eapply rtc_once.
433 eapply E_Ctx with (E := cforce uf).
434 *** destruct uf; [by apply is_ctx_once | done].
435 *** apply E_IfFalse.
436 ** eapply rtc_l.
437 --- eapply E_Ctx.
438 +++ destruct uf; [by apply is_ctx_once | done].
439 +++ replace (Ne_Cons head (s :: tail))
440 with (nonempty_cons head (Ne_Cons s tail)) by done.
441 constructor.
442 --- eapply rtc_l.
443 +++ eapply E_Ctx
444 with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
445 *** destruct uf; simplify_option_eq.
446 ---- eapply IsCtx_Compose;
447 [constructor | by apply is_ctx_once].
448 ---- apply is_ctx_once. unfold compose. by simpl.
449 *** by apply E_OpHasAttrFalse.
450 +++ simplify_eq/=.
451 eapply rtc_once.
452 eapply E_Ctx with (E := cforce uf).
453 *** destruct uf; [by apply is_ctx_once | done].
454 *** apply E_IfFalse.
455 + (* X_Apply *)
456 case_match; simplify_option_eq; apply IHn in Heqo, Heval.
457 * (* Basic lambda abstraction *)
458 apply rtc_transitive with (y := cforce uf (X_Apply (V_Fn x e) e2)).
459 -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
460 [done|].
461 destruct uf.
462 ++ by eapply IsCtx_Compose; [|apply is_ctx_once].
463 ++ apply is_ctx_once. unfold compose. by simpl.
464 -- apply rtc_transitive
465 with (y := cforce uf (subst {[x := X_Closed e2]} e)); [|done].
466 eapply rtc_once.
467 eapply E_Ctx.
468 ++ destruct uf; [by apply is_ctx_once | done].
469 ++ by constructor.
470 * (* Pattern-matching function *)
471 apply rtc_transitive
472 with (y := cforce uf (X_Apply (V_AttrsetFn m e) e2)).
473 -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
474 [done|].
475 destruct uf.
476 ++ by eapply IsCtx_Compose; [|apply is_ctx_once].
477 ++ apply is_ctx_once. unfold compose. by simpl.
478 -- apply rtc_transitive
479 with (y := cforce uf (X_Apply (V_AttrsetFn m e) (V_Attrset H0))).
480 ++ apply ctx_mstep
481 with (E := cforce uf ∘ λ e2, X_Apply (V_AttrsetFn m e) e2).
482 ** by apply IHn in Heqo0.
483 ** destruct uf.
484 --- by eapply IsCtx_Compose; [|apply is_ctx_once].
485 --- apply is_ctx_once. unfold compose. by simpl.
486 ++ apply rtc_transitive with (y := cforce uf (X_LetBinding H e));
487 [|done].
488 eapply rtc_once.
489 eapply E_Ctx.
490 ** destruct uf; [by apply is_ctx_once | done].
491 ** apply matches_sound in Heqo1. by constructor.
492 * (* __functor *)
493 apply rtc_transitive with (y := cforce uf (X_Apply (V_Attrset bs) e2)).
494 -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
495 [done|].
496 destruct uf.
497 ++ by eapply IsCtx_Compose; [|apply is_ctx_once].
498 ++ apply is_ctx_once. unfold compose. by simpl.
499 -- apply rtc_transitive
500 with (y := cforce uf (X_Apply (X_Apply H (V_Attrset bs)) e2));
501 [|done].
502 eapply rtc_once.
503 eapply E_Ctx.
504 ++ destruct uf; [by apply is_ctx_once | done].
505 ++ by replace bs with (<["__functor" := H]>bs); [|apply insert_id].
506 + (* X_Cond *)
507 simplify_option_eq.
508 apply IHn in Heqo, Heval.
509 apply rtc_transitive with (y := cforce uf (X_Cond (V_Bool H0) e2 e3)).
510 * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Cond e1 e2 e3); [done|].
511 destruct uf.
512 -- by eapply IsCtx_Compose; [|apply is_ctx_once].
513 -- apply is_ctx_once. unfold compose. by simpl.
514 * destruct H0; eapply rtc_l; try done; eapply E_Ctx; try done;
515 by destruct uf; [apply is_ctx_once|].
516 + (* X_Incl *)
517 apply IHn in Heqo.
518 apply rtc_transitive with (y := cforce uf (X_Incl H e2)).
519 * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Incl e1 e2).
520 -- done.
521 -- destruct uf.
522 ++ eapply IsCtx_Compose; [done | by apply is_ctx_once].
523 ++ unfold compose. apply is_ctx_once. by simpl.
524 * destruct (decide (attrset H)).
525 -- destruct H; inv a. simplify_option_eq. apply IHn in Heval.
526 eapply rtc_l; [|done].
527 eapply E_Ctx.
528 ++ destruct uf; [by apply is_ctx_once | done].
529 ++ apply E_With.
530 -- destruct H;
531 try (eapply rtc_l;
532 [ eapply E_Ctx;
533 [ destruct uf; [by apply is_ctx_once | done]
534 | by apply E_WithNoAttrset ]
535 | by apply IHn in Heval ]).
536 destruct n0. by exists bs.
537 + (* X_Assert *)
538 apply IHn in Heqo.
539 apply rtc_transitive with (y := cforce uf (X_Assert H e2)).
540 * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Assert e1 e2); [done|].
541 destruct uf.
542 -- by eapply IsCtx_Compose; [|apply is_ctx_once].
543 -- unfold compose. apply is_ctx_once. by simpl.
544 * destruct H; try discriminate. destruct p; try discriminate.
545 apply IHn in Heval. eapply rtc_l; [|done].
546 eapply E_Ctx; [|done].
547 by destruct uf; [apply is_ctx_once|].
548 + (* X_Binop *)
549 apply IHn in Heqo, Heqo0.
550 apply rtc_transitive with (y := cforce uf (X_Op op (X_V H) e2)).
551 * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Op op e1 e2).
552 -- done.
553 -- destruct uf.
554 ++ eapply IsCtx_Compose; [done | by apply is_ctx_once].
555 ++ unfold compose. apply is_ctx_once. by simpl.
556 * apply rtc_transitive with (y := cforce uf (X_Op op (X_V H) (X_V H0))).
557 -- apply ctx_mstep with (E := cforce uf ∘ λ e2, X_Op op (X_V H) e2).
558 ++ done.
559 ++ destruct uf.
560 ** eapply IsCtx_Compose; [done | by apply is_ctx_once].
561 ** unfold compose. apply is_ctx_once. by simpl.
562 -- eapply rtc_l.
563 ++ eapply E_Ctx with (E := cforce uf).
564 ** destruct uf; [by apply is_ctx_once | done].
565 ** apply E_Op. by apply binop_eval_sound.
566 ++ by apply IHn.
567 + (* X_HasAttr *)
568 apply IHn in Heqo.
569 apply rtc_transitive with (y := cforce uf (X_HasAttr H x)).
570 * apply ctx_mstep with (E := cforce uf ∘ λ e, X_HasAttr e x); [done|].
571 destruct uf.
572 -- by eapply IsCtx_Compose; [|apply is_ctx_once].
573 -- unfold compose. apply is_ctx_once. by simpl.
574 * destruct (decide (attrset H)).
575 -- case_match; inv a. simplify_option_eq.
576 apply rtc_transitive
577 with (y := cforce uf (bool_decide (is_Some (x0 !! x)))).
578 ++ apply rtc_once. eapply E_Ctx.
579 ** destruct uf; [by apply is_ctx_once | done].
580 ** destruct (decide (is_Some (x0 !! x))).
581 --- rewrite bool_decide_true by done. by constructor.
582 --- rewrite bool_decide_false by done. constructor.
583 by apply eq_None_not_Some in n0.
584 ++ destruct uf; [|done].
585 apply rtc_once. simpl.
586 replace (V_Bool (bool_decide (is_Some (x0 !! x))))
587 with (value_from_strong_value
588 (SV_Bool (bool_decide (is_Some (x0 !! x)))))
589 by done.
590 by eapply E_Ctx with (E := id).
591 -- apply rtc_transitive with (y := cforce uf false).
592 ++ apply rtc_once. eapply E_Ctx.
593 ** destruct uf; [by apply is_ctx_once | done].
594 ** by constructor.
595 ++ assert (Hforce : cforce true false -->* false).
596 { apply rtc_once.
597 simpl.
598 replace (V_Bool false)
599 with (value_from_strong_value (SV_Bool false)) by done.
600 eapply E_Ctx with (E := id); done. }
601 destruct H; try (by destruct uf; [apply Hforce | done]).
602 exfalso. apply n0. by exists bs.
603 + (* X_Force *)
604 apply IHn in Heval. clear IHn n.
605 destruct uf; try done. simplify_eq/=.
606 by apply force_idempotent.
607 + (* X_Closed *)
608 apply IHn in Heval.
609 eapply rtc_l; [|done].
610 eapply E_Ctx; [|done].
611 * by destruct uf; [apply is_ctx_once|].
612 + (* X_Placeholder *)
613 apply IHn in Heval. clear IHn n.
614 destruct uf; simplify_eq/=; eapply rtc_l; try done.
615 -- eapply E_Ctx with (E := X_Force); [by apply is_ctx_once | done].
616 -- by eapply E_Ctx with (E := id).
617Qed.
618
619Lemma value_stuck v : ¬ ∃ e', X_V v --> e'.
620Proof.
621 induction v; intros [e' He']; inversion He';
622 subst; (inv H0; [inv H1 | inv H2]).
623Qed.
624
625Theorem eval_sound_weak e v' n : eval n false e = Some v' → is_nf_of step e v'.
626Proof.
627 intros Heval.
628 pose proof (eval_sound_strong _ _ _ _ Heval).
629 split; [done | apply value_stuck].
630Qed.
generated by cgit v1.2.3 (git 2.45.2) at 2024-12-25 19:32:05 +0000