diff options
author | Rutger Broekhoff | 2024-06-26 20:50:18 +0200 |
---|---|---|
committer | Rutger Broekhoff | 2024-06-26 20:50:18 +0200 |
commit | 73df1945b31c0beee88cf4476df4ccd09d31403b (patch) | |
tree | ed00db26b711442e643f38b66888a3df56e33ebd | |
download | mininix-formalization-73df1945b31c0beee88cf4476df4ccd09d31403b.tar.gz mininix-formalization-73df1945b31c0beee88cf4476df4ccd09d31403b.zip |
Import Coq project
-rw-r--r-- | .envrc | 1 | ||||
-rw-r--r-- | .gitignore | 12 | ||||
-rw-r--r-- | Makefile | 20 | ||||
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | binop.v | 87 | ||||
-rw-r--r-- | complete.v | 413 | ||||
-rw-r--r-- | correct.v | 299 | ||||
-rw-r--r-- | expr.v | 250 | ||||
-rw-r--r-- | flake.lock | 61 | ||||
-rw-r--r-- | flake.nix | 23 | ||||
-rw-r--r-- | interpreter.v | 103 | ||||
-rw-r--r-- | maptools.v | 476 | ||||
-rw-r--r-- | matching.v | 609 | ||||
-rw-r--r-- | relations.v | 73 | ||||
-rw-r--r-- | sem.v | 167 | ||||
-rw-r--r-- | semprop.v | 426 | ||||
-rw-r--r-- | shared.v | 66 | ||||
-rw-r--r-- | sound.v | 630 |
18 files changed, 3717 insertions, 0 deletions
@@ -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 | ||
11 | Makefile.coq | ||
12 | Makefile.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 | |||
3 | COQMFFLAGS := -Q . mininix | ||
4 | |||
5 | ALLVFILES := 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 | |||
8 | build: Makefile.coq | ||
9 | $(MAKE) -f Makefile.coq | ||
10 | |||
11 | clean:: | ||
12 | if [ -e Makefile.coq ]; then $(MAKE) -f Makefile.coq cleanall; fi | ||
13 | $(RM) $(wildcard Makefile.coq Makefile.coq.conf) | ||
14 | |||
15 | Makefile.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 | |||
@@ -0,0 +1,87 @@ | |||
1 | Require Import Coq.NArith.BinNat. | ||
2 | Require Import Coq.Strings.Ascii. | ||
3 | Require Import Coq.Strings.String. | ||
4 | From stdpp Require Import fin_sets gmap option. | ||
5 | From mininix Require Import expr maptools shared. | ||
6 | |||
7 | Open Scope string_scope. | ||
8 | Open Scope N_scope. | ||
9 | Open Scope Z_scope. | ||
10 | Open Scope nat_scope. | ||
11 | |||
12 | Definition right_union {A} (bs1 bs2 : gmap string A) : gmap string A := | ||
13 | bs2 ∪ bs1. | ||
14 | |||
15 | Variant 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 | |||
27 | Notation "u1 '⟦' op '⟧' u2 '-⊚->' v" := (binop_r op u1 u2 v) (at level 55). | ||
28 | |||
29 | Definition 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 | |||
65 | Theorem binop_eval_sound op u1 u2 v : | ||
66 | binop_eval op u1 u2 = Some v → binop_r op u1 u2 v. | ||
67 | Proof. | ||
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. | ||
72 | Qed. | ||
73 | |||
74 | Theorem binop_eval_complete op u1 u2 v : | ||
75 | binop_r op u1 u2 v → binop_eval op u1 u2 = Some v. | ||
76 | Proof. | ||
77 | intros Heval. inv Heval; try done. | ||
78 | unfold binop_eval. by apply decide_False. | ||
79 | Qed. | ||
80 | |||
81 | Theorem binop_deterministic op u1 u2 v1 v2 : | ||
82 | u1 ⟦op⟧ u2 -⊚-> v1 → u1 ⟦op⟧ u2 -⊚-> v2 → v1 = v2. | ||
83 | Proof. | ||
84 | intros Heval1 Heval2. | ||
85 | apply binop_eval_complete in Heval1, Heval2. | ||
86 | congruence. | ||
87 | Qed. | ||
diff --git a/complete.v b/complete.v new file mode 100644 index 0000000..9939b50 --- /dev/null +++ b/complete.v | |||
@@ -0,0 +1,413 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From stdpp Require Import gmap relations. | ||
3 | From mininix Require Import binop expr interpreter maptools matching sem. | ||
4 | |||
5 | Lemma eval_le n uf e v' : | ||
6 | eval n uf e = Some v' → | ||
7 | ∀ m, n ≤ m → eval m uf e = Some v'. | ||
8 | Proof. | ||
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. | ||
21 | Qed. | ||
22 | |||
23 | Lemma eval_value n (v : value) : 0 < n → eval n false v = Some v. | ||
24 | Proof. destruct n, v; by try lia. Qed. | ||
25 | |||
26 | Lemma eval_strong_value n (sv : strong_value) : | ||
27 | 0 < n → | ||
28 | eval n false sv = Some (value_from_strong_value sv). | ||
29 | Proof. destruct n, sv; by try lia. Qed. | ||
30 | |||
31 | Lemma eval_force_strong_value v : ∃ n, | ||
32 | eval n true (expr_from_strong_value v) = Some (value_from_strong_value v). | ||
33 | Proof. | ||
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). | ||
67 | Qed. | ||
68 | |||
69 | Lemma eval_force_strong_value' v : | ||
70 | ∃ n, eval n false (X_Force (expr_from_strong_value v)) = | ||
71 | Some (value_from_strong_value v). | ||
72 | Proof. | ||
73 | destruct (eval_force_strong_value v) as [n Heval]. | ||
74 | exists (S n). by rewrite eval_S. | ||
75 | Qed. | ||
76 | |||
77 | Lemma rec_subst_lookup bs x e : | ||
78 | bs !! x = Some (B_Nonrec e) → rec_subst bs !! x = Some e. | ||
79 | Proof. unfold rec_subst. rewrite lookup_fmap. by intros ->. Qed. | ||
80 | |||
81 | Lemma rec_subst_lookup_fmap bs x e : | ||
82 | bs !! x = Some e → rec_subst (B_Nonrec <$> bs) !! x = Some e. | ||
83 | Proof. unfold rec_subst. do 2 rewrite lookup_fmap. by intros ->. Qed. | ||
84 | |||
85 | Lemma rec_subst_lookup_fmap' bs x : | ||
86 | is_Some (bs !! x) ↔ is_Some (rec_subst (B_Nonrec <$> bs) !! x). | ||
87 | Proof. | ||
88 | unfold rec_subst. split; | ||
89 | do 2 rewrite lookup_fmap in *; | ||
90 | intros [b H]; by simplify_option_eq. | ||
91 | Qed. | ||
92 | |||
93 | Lemma 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''. | ||
97 | Proof. | ||
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]. | ||
236 | Qed. | ||
237 | |||
238 | Lemma 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''. | ||
243 | Proof. | ||
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. | ||
394 | Qed. | ||
395 | |||
396 | Lemma eval_step e e' v'' n : | ||
397 | e --> e' → | ||
398 | eval n false e' = Some v'' → | ||
399 | ∃ m, eval m false e = Some v''. | ||
400 | Proof. | ||
401 | intros. inv H. | ||
402 | apply (eval_step_ctx e1 e2 E false uf_int n v'' H1 H2 H0). | ||
403 | Qed. | ||
404 | |||
405 | Theorem eval_complete e (v' : value) : | ||
406 | e -->* v' → ∃ n, eval n false e = Some v'. | ||
407 | Proof. | ||
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. | ||
413 | Qed. | ||
diff --git a/correct.v b/correct.v new file mode 100644 index 0000000..89f5894 --- /dev/null +++ b/correct.v | |||
@@ -0,0 +1,299 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From stdpp Require Import gmap. | ||
3 | From mininix Require Import | ||
4 | expr relations sem interpreter complete sound shared. | ||
5 | |||
6 | Theorem correct e v' : (∃ n, eval n false e = Some v') ↔ e -->* v'. | ||
7 | Proof. | ||
8 | split. | ||
9 | - intros [n Heval]. by apply (eval_sound_strong n false). | ||
10 | - intros Heval. by apply eval_complete. | ||
11 | Qed. | ||
12 | |||
13 | (* Top-level program reduction/evaluation: | ||
14 | we make the prelude available here. *) | ||
15 | |||
16 | Definition with_prelude (e : expr) : expr := | ||
17 | subst (closed prelude) e. | ||
18 | |||
19 | Definition tl_reds (e e' : expr) := | ||
20 | with_prelude e -->* e'. | ||
21 | |||
22 | Definition tl_eval (n : nat) (e : expr) : option value := | ||
23 | eval n false (subst (closed prelude) e). | ||
24 | |||
25 | Definition tl_evals e e' := ∃ n, tl_eval n e = Some e'. | ||
26 | |||
27 | (* Macros *) | ||
28 | |||
29 | Definition μ_neq e1 e2 := X_Cond (X_Op O_Eq e1 e2) false true. | ||
30 | Definition μ_or e1 e2 := X_Cond e1 true e2. | ||
31 | Definition μ_and e1 e2 := X_Cond e1 e2 false. | ||
32 | Definition μ_impl e1 e2 := X_Cond e1 e2 true. | ||
33 | Definition μ_neg e := X_Cond e false true. | ||
34 | |||
35 | Definition μ_le n m := μ_or (X_Op O_Eq n m) (X_Op O_Lt n m). | ||
36 | Definition μ_gt n m := X_Op O_Lt m n. | ||
37 | Definition μ_ge n m := μ_or (X_Op O_Eq n m) (μ_gt n m). | ||
38 | |||
39 | (* Tests/examples *) | ||
40 | |||
41 | Definition ex1 := X_LetBinding {[ "a" := B_Rec 1%Z ]} "a". | ||
42 | |||
43 | (* [let a = 1; in a] gives 1 *) | ||
44 | Theorem ex1_step : tl_reds ex1 1%Z. | ||
45 | Proof. | ||
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). | ||
52 | Qed. | ||
53 | |||
54 | Example ex1_eval : tl_evals ex1 (V_Int 1). | ||
55 | Proof. by exists 3. Qed. | ||
56 | |||
57 | (* Definition ex2 := <{ let a = 1 in with { a = 2 }; a }>. *) | ||
58 | Definition 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 *) | ||
62 | Theorem ex2_step : tl_reds ex2 1%Z. | ||
63 | Proof. | ||
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). | ||
72 | Qed. | ||
73 | |||
74 | Example ex2_eval : tl_evals ex2 (V_Int 1). | ||
75 | Proof. by exists 4. Qed. | ||
76 | |||
77 | (* [with { a = 1; }; with { a = 2; }; a] gives 2 *) | ||
78 | Definition ex3 := | ||
79 | X_Incl (V_Attrset {[ "a" := X_V 1%Z ]}) | ||
80 | (X_Incl (V_Attrset {[ "a" := X_V 2%Z ]}) "a"). | ||
81 | |||
82 | Theorem ex3_step : tl_reds ex3 2%Z. | ||
83 | Proof. | ||
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). | ||
92 | Qed. | ||
93 | |||
94 | Example ex3_eval : tl_evals ex3 (V_Int 2). | ||
95 | Proof. by exists 4. Qed. | ||
96 | |||
97 | (* [({ x, y ? x } : y) { x = 1; }] gives 1 *) | ||
98 | Definition 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 | |||
109 | Example ex4_eval : tl_evals ex4 (V_Int 1). | ||
110 | Proof. by exists 7. Qed. | ||
111 | |||
112 | (* [({ x ? y, y ? x } : y) { x = 1; }] gives 1 *) | ||
113 | Definition 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 | |||
124 | Example ex5_eval : tl_evals ex5 (V_Int 1). | ||
125 | Proof. 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)" *) | ||
137 | Definition 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 | |||
188 | Example ex6_eval : tl_evals ex6 (V_Str "x: 110, y: 110, z: (no z)"). | ||
189 | Proof. 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 *) | ||
194 | Definition 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 | |||
202 | Example ex7_eval : tl_evals ex7 (V_Int 1). | ||
203 | Proof. by exists 7. Qed. | ||
204 | |||
205 | Definition 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 | |||
245 | Example ex8_eval : tl_evals ex8 (V_Int 5). | ||
246 | Proof. by exists 170. Qed. | ||
247 | |||
248 | Example 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 | |||
265 | Example ex9_eval : tl_evals ex9 (V_Int 610). | ||
266 | Proof. by exists 78. Qed. | ||
267 | |||
268 | Example ex10 := | ||
269 | X_LetBinding | ||
270 | {[ "true" := B_Rec 42 ]}%Z | ||
271 | (X_Op O_Eq "true" 42)%Z. | ||
272 | |||
273 | Example ex10_eval : tl_evals ex10 (V_Bool true). | ||
274 | Proof. by exists 4. Qed. | ||
275 | |||
276 | Definition ex11 := | ||
277 | X_LetBinding | ||
278 | {[ "x" := B_Rec "y" ]}%Z | ||
279 | (X_LetBinding {[ "y" := B_Rec 10 ]} "x")%Z. | ||
280 | |||
281 | Example ex11_eval : tl_eval 1000 ex11 = None. | ||
282 | Proof. done. Qed. | ||
283 | |||
284 | Definition 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 | |||
296 | Example ex12_eval : tl_eval 1000 ex12 = Some (V_Int 1). | ||
297 | Proof. done. Qed. | ||
298 | |||
299 | (* Aio, quantitas magna frumentorum est. *) | ||
@@ -0,0 +1,250 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From 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 *) | ||
8 | Variant op : Type := | ||
9 | | O_Eq (* = *) | ||
10 | | O_Lt (* < *) | ||
11 | | O_Plus (* + *) | ||
12 | | O_Min (* - *) | ||
13 | | O_Div (* / *) | ||
14 | | O_Upd. (* // *) | ||
15 | |||
16 | Hint Constructors op : core. | ||
17 | |||
18 | Variant nonempty A := Ne_Cons (head : A) (tail : list A). | ||
19 | Arguments Ne_Cons {A} _ _. | ||
20 | Hint Constructors nonempty : core. | ||
21 | |||
22 | Inductive 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) *) | ||
38 | with b_rhs := | ||
39 | | B_Rec (e : expr) (* := e *) | ||
40 | | B_Nonrec (e : expr) (* :=ᵣ e *) | ||
41 | with matcher := | ||
42 | | M_Matcher (ms : gmap string m_rhs) (strict : bool) | ||
43 | with m_rhs := | ||
44 | | M_Mandatory | ||
45 | | M_Optional (e : expr) (* ? e *) | ||
46 | with 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 | |||
55 | Hint Constructors expr : core. | ||
56 | |||
57 | Instance Maybe_X_Attrset : Maybe X_Attrset := λ e, | ||
58 | match e with | ||
59 | | X_Attrset bs => Some bs | ||
60 | | _ => None | ||
61 | end. | ||
62 | |||
63 | Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs, | ||
64 | match rhs with | ||
65 | | B_Nonrec e => Some e | ||
66 | | _ => None | ||
67 | end. | ||
68 | |||
69 | Instance Maybe_B_Rec : Maybe B_Rec := λ rhs, | ||
70 | match rhs with | ||
71 | | B_Rec e => Some e | ||
72 | | _ => None | ||
73 | end. | ||
74 | |||
75 | Lemma maybe_b_rhs_excl b : | ||
76 | is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b) → False. | ||
77 | Proof. intros [e2 Hnonrec] [e1 Hrec]. simplify_option_eq. Qed. | ||
78 | |||
79 | Lemma no_b_nonrec__b_rec b : | ||
80 | ¬ is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b). | ||
81 | Proof. | ||
82 | destruct b; try by eauto. | ||
83 | simplify_eq/=. intros contra. apply is_Some_alt. eauto. | ||
84 | Qed. | ||
85 | |||
86 | Lemma no_b_rec__b_nonrec b : | ||
87 | ¬ is_Some (maybe B_Rec b) → is_Some (maybe B_Nonrec b). | ||
88 | Proof. | ||
89 | destruct b; try by eauto. | ||
90 | simplify_eq/=. intros contra. apply is_Some_alt. eauto. | ||
91 | Qed. | ||
92 | |||
93 | Instance Maybe_V_Attrset : Maybe V_Attrset := λ e, | ||
94 | match e with | ||
95 | | V_Attrset bs => Some bs | ||
96 | | _ => None | ||
97 | end. | ||
98 | |||
99 | Instance Maybe_V_Bool : Maybe V_Bool := λ e, | ||
100 | match e with | ||
101 | | V_Bool p => Some p | ||
102 | | _ => None | ||
103 | end. | ||
104 | |||
105 | Global Instance B_Nonrec_inj : Inj (=) (=) B_Nonrec. | ||
106 | Proof. intros [] [] ?; by simplify_eq. Qed. | ||
107 | |||
108 | Definition matcher_keys (m : matcher) : gset string := | ||
109 | match m with M_Matcher ms _ => dom ms end. | ||
110 | |||
111 | Definition 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 | |||
121 | Local 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 | |||
125 | Local 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) *) | ||
132 | Fixpoint 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 | |||
163 | Definition closed (bs : gmap string expr) : gmap string expr := | ||
164 | X_Closed <$> bs. | ||
165 | |||
166 | Definition placeholders (bs : gmap string expr) : gmap string expr := | ||
167 | map_imap (λ (x : string) (e : expr), Some (X_Placeholder x e)) bs. | ||
168 | |||
169 | Definition nonempty_singleton {A} (a : A): nonempty A := Ne_Cons a nil. | ||
170 | |||
171 | Definition 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 | |||
174 | Definition 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 | |||
178 | Definition 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 | |||
185 | Inductive 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 | |||
194 | Fixpoint 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 | |||
205 | Global Instance X_V_inj : Inj (=) (=) X_V. | ||
206 | Proof. intros [] [] ?; by simplify_eq. Qed. | ||
207 | |||
208 | Definition expr_from_strong_value : strong_value → expr := | ||
209 | X_V ∘ value_from_strong_value. | ||
210 | |||
211 | (* Based on the fin_maps test from stdpp *) | ||
212 | Fixpoint 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 *) | ||
220 | Lemma 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. | ||
231 | Proof. | ||
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. | ||
241 | Qed. | ||
242 | |||
243 | Coercion X_Id : string >-> expr. | ||
244 | Coercion 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. *) | ||
248 | Coercion V_Bool : bool >-> value. | ||
249 | Coercion X_V : value >-> expr. | ||
250 | Coercion 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 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From stdpp Require Import fin_maps. | ||
3 | From mininix Require Import binop expr maptools matching. | ||
4 | |||
5 | Open Scope string_scope. | ||
6 | |||
7 | Definition 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 | |||
90 | Fixpoint 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 *) | ||
101 | Global Opaque eval. | ||
102 | Lemma eval_S n : eval (S n) = eval1 (eval n). | ||
103 | Proof. 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 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From stdpp Require Import countable fin_maps fin_map_dom. | ||
3 | |||
4 | (** Generic lemmas for finite maps and their domains *) | ||
5 | |||
6 | Lemma 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. | ||
9 | Proof. | ||
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. | ||
16 | Qed. | ||
17 | |||
18 | Lemma 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). | ||
24 | Proof. | ||
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. | ||
41 | Qed. | ||
42 | |||
43 | Lemma 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. | ||
47 | Proof. | ||
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. | ||
59 | Qed. | ||
60 | |||
61 | Lemma 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. | ||
65 | Proof. | ||
66 | intros Hmap. | ||
67 | rewrite <-lookup_fmap. | ||
68 | rewrite Hmap. | ||
69 | apply lookup_insert. | ||
70 | Qed. | ||
71 | |||
72 | Lemma 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). | ||
76 | Proof. | ||
77 | intros Hdel. | ||
78 | setoid_rewrite <-insert_delete_insert at 1 2. | ||
79 | rewrite 2 dom_insert_L. | ||
80 | set_solver. | ||
81 | Qed. | ||
82 | |||
83 | Lemma 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). | ||
87 | Proof. | ||
88 | intros Hdel. | ||
89 | setoid_rewrite <-insert_delete_insert at 1 2. | ||
90 | rewrite 2 dom_insert_L. | ||
91 | set_solver. | ||
92 | Qed. | ||
93 | |||
94 | Lemma map_dom_empty_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} | ||
95 | (m : M A) : dom (∅ : M A) = dom m → m = ∅. | ||
96 | Proof. | ||
97 | intros Hdom. | ||
98 | rewrite dom_empty_L in Hdom. | ||
99 | symmetry in Hdom. | ||
100 | by apply dom_empty_inv_L. | ||
101 | Qed. | ||
102 | |||
103 | Lemma 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. | ||
107 | Proof. set_solver. Qed. | ||
108 | |||
109 | (** map_mapM *) | ||
110 | |||
111 | Definition 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 | |||
115 | Lemma 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. | ||
118 | Proof. | ||
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. | ||
137 | Qed. | ||
138 | |||
139 | Lemma 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). | ||
145 | Proof. | ||
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. | ||
165 | Qed. | ||
166 | |||
167 | (** map_Forall2 *) | ||
168 | |||
169 | Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B} | ||
170 | (R : A → B → Prop) := | ||
171 | map_relation (M := M) R (λ _, False) (λ _, False). | ||
172 | |||
173 | Global 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). | ||
175 | Proof. apply map_relation_dec; intros; try done; apply False_dec. Qed. | ||
176 | |||
177 | Lemma 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). | ||
184 | Proof. | ||
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. | ||
190 | Qed. | ||
191 | |||
192 | Lemma 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). | ||
197 | Proof. | ||
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. | ||
206 | Qed. | ||
207 | |||
208 | Lemma 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'. | ||
212 | Proof. | ||
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. | ||
224 | Qed. | ||
225 | |||
226 | Lemma 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). | ||
230 | Proof. | ||
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. | ||
255 | Qed. | ||
256 | |||
257 | Lemma 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. | ||
263 | Proof. | ||
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. | ||
269 | Qed. | ||
270 | |||
271 | Lemma 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. | ||
274 | Proof. | ||
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. | ||
286 | Qed. | ||
287 | |||
288 | Lemma 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 = ∅. | ||
291 | Proof. | ||
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. | ||
297 | Qed. | ||
298 | |||
299 | Lemma 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 = ∅. | ||
302 | Proof. | ||
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. | ||
307 | Qed. | ||
308 | |||
309 | Lemma map_Forall2_empty `{FinMap K M} {A B} (R : A → B → Prop): | ||
310 | map_Forall2 R (∅ : M A) (∅ : M B). | ||
311 | Proof. | ||
312 | unfold map_Forall2, map_relation. | ||
313 | intros i. by rewrite 2 lookup_empty. | ||
314 | Qed. | ||
315 | |||
316 | Lemma 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. | ||
321 | Proof. | ||
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. | ||
327 | Qed. | ||
328 | |||
329 | Lemma 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. | ||
332 | Proof. | ||
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/=. | ||
338 | Qed. | ||
339 | |||
340 | Lemma map_Forall2_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} | ||
341 | (m1 m2 : M A) : | ||
342 | m1 = m2 ↔ map_Forall2 (=) m1 m2. | ||
343 | Proof. | ||
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. | ||
355 | Qed. | ||
356 | |||
357 | Lemma 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. | ||
362 | Proof. | ||
363 | intros Heq Hdel. | ||
364 | apply map_Forall2_eq_L. | ||
365 | eapply map_Forall2_insert_weak; [done|]. | ||
366 | by apply map_Forall2_eq_L. | ||
367 | Qed. | ||
368 | |||
369 | Lemma 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. | ||
372 | Proof. | ||
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. | ||
376 | Qed. | ||
377 | |||
378 | Lemma 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. | ||
381 | Proof. apply map_insert_rev_L. Qed. | ||
382 | |||
383 | Lemma 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. | ||
386 | Proof. apply map_insert_rev_L. Qed. | ||
387 | |||
388 | Lemma 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. | ||
392 | Proof. | ||
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. | ||
414 | Qed. | ||
415 | |||
416 | (** Relation between map_mapM and map_Forall2 *) | ||
417 | |||
418 | Lemma 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. | ||
421 | Proof. | ||
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. | ||
447 | Qed. | ||
448 | |||
449 | Lemma 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. | ||
452 | Proof. | ||
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. | ||
471 | Qed. | ||
472 | |||
473 | Lemma 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. | ||
476 | Proof. 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 @@ | |||
1 | Require Import Coq.Strings.Ascii. | ||
2 | Require Import Coq.Strings.String. | ||
3 | Require Import Coq.NArith.BinNat. | ||
4 | From stdpp Require Import fin_sets gmap option. | ||
5 | From mininix Require Import expr maptools. | ||
6 | |||
7 | Open Scope string_scope. | ||
8 | Open Scope N_scope. | ||
9 | Open Scope Z_scope. | ||
10 | Open Scope nat_scope. | ||
11 | |||
12 | Reserved Notation "bs '~' m '~>' brs" (at level 55). | ||
13 | |||
14 | Inductive 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' | ||
34 | where "bs ~ m ~> brs" := (matches_r bs m brs). | ||
35 | |||
36 | Definition 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 | |||
40 | Definition 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 | |||
55 | Definition 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 | |||
59 | Definition 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 *) | ||
69 | Lemma dom_subseteq_size' `{FinMapDom K M D} {A B} (m1 : M A) (m2 : M B) : | ||
70 | dom m2 ⊆ dom m1 → size m2 ≤ size m1. | ||
71 | Proof. | ||
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. | ||
81 | Qed. | ||
82 | |||
83 | Lemma dom_empty_subset `{Countable K} `{FinMapDom K M D} {A B} (m : M A) : | ||
84 | dom m ⊆ dom (∅ : M B) → m = ∅. | ||
85 | Proof. | ||
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. | ||
91 | Qed. | ||
92 | |||
93 | Lemma matches_aux_empty bs : matches_aux ∅ bs = Some (bs, ∅). | ||
94 | Proof. done. Qed. | ||
95 | |||
96 | Lemma 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). | ||
104 | Proof. | ||
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. | ||
111 | Qed. | ||
112 | |||
113 | Lemma 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). | ||
116 | Proof. | ||
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. | ||
122 | Qed. | ||
123 | |||
124 | Lemma matches_aux_bs m bs bs' brs : | ||
125 | matches_aux m bs = Some (bs', brs) → bs = bs'. | ||
126 | Proof. | ||
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). | ||
136 | Qed. | ||
137 | |||
138 | Lemma 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). | ||
143 | Proof. | ||
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. | ||
163 | Qed. | ||
164 | |||
165 | Lemma 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). | ||
170 | Proof. | ||
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. | ||
190 | Qed. | ||
191 | |||
192 | Lemma matches_aux_dom m bs brs : | ||
193 | matches_aux m bs = Some (bs, brs) → dom m = dom brs. | ||
194 | Proof. | ||
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. | ||
202 | Qed. | ||
203 | |||
204 | Lemma 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). | ||
209 | Proof. | ||
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. | ||
228 | Qed. | ||
229 | |||
230 | Lemma disjoint_union_subseteq_l `{FinSet A C} `{!LeibnizEquiv C} (X Y Z : C) : | ||
231 | X ## Y → X ## Z → X ∪ Y ⊆ X ∪ Z → Y ⊆ Z. | ||
232 | Proof. | ||
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. | ||
238 | Qed. | ||
239 | |||
240 | Lemma singleton_notin_union_disjoint `{FinMapDom K M D} {A} (m : M A) (i : K) : | ||
241 | m !! i = None → | ||
242 | {[i]} ## dom m. | ||
243 | Proof. | ||
244 | intros Hlookup. apply disjoint_singleton_l. | ||
245 | by apply not_elem_of_dom in Hlookup. | ||
246 | Qed. | ||
247 | |||
248 | Lemma 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). | ||
251 | Proof. | ||
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. | ||
289 | Qed. | ||
290 | |||
291 | Lemma 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'. | ||
296 | Proof. | ||
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. | ||
302 | Qed. | ||
303 | |||
304 | Lemma 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). | ||
308 | Proof. | ||
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. | ||
350 | Qed. | ||
351 | |||
352 | Lemma 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'). | ||
360 | Proof. | ||
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. | ||
375 | Qed. | ||
376 | |||
377 | Lemma 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. | ||
382 | Proof. | ||
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. | ||
396 | Qed. | ||
397 | |||
398 | Lemma 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). | ||
403 | Proof. | ||
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. | ||
423 | Qed. | ||
424 | |||
425 | Lemma 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. | ||
430 | Proof. | ||
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. | ||
444 | Qed. | ||
445 | |||
446 | Lemma 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). | ||
451 | Proof. | ||
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. | ||
469 | Qed. | ||
470 | |||
471 | Lemma 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. | ||
476 | Proof. | ||
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. | ||
490 | Qed. | ||
491 | |||
492 | Theorem matches_sound m bs brs : matches m bs = Some brs → bs ~ m ~> brs. | ||
493 | Proof. | ||
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. | ||
519 | Qed. | ||
520 | |||
521 | Theorem matches_complete m bs brs : bs ~ m ~> brs → matches m bs = Some brs. | ||
522 | Proof. | ||
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. | ||
602 | Qed. | ||
603 | |||
604 | Theorem matches_correct m bs brs : matches m bs = Some brs ↔ bs ~ m ~> brs. | ||
605 | Proof. split; [apply matches_sound | apply matches_complete]. Qed. | ||
606 | |||
607 | Theorem matches_deterministic m bs brs1 brs2 : | ||
608 | bs ~ m ~> brs1 → bs ~ m ~> brs2 → brs1 = brs2. | ||
609 | Proof. 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 @@ | |||
1 | From stdpp Require Import relations. | ||
2 | |||
3 | Definition 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. *) | ||
8 | Definition is_nf_of `(R : relation A) x y := (rtc R x y) ∧ nf R y. | ||
9 | |||
10 | (** The reflexive closure. *) | ||
11 | Inductive 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 | |||
15 | Hint Constructors rc : core. | ||
16 | |||
17 | (* Baader and Nipkow, Definition 2.7.3. *) | ||
18 | Definition 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. *) | ||
22 | Definition 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 *) | ||
26 | Lemma strong__semi_confluence {A} (R : relation A) : | ||
27 | strongly_confluent R → semi_confluent R. | ||
28 | Proof. | ||
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). | ||
48 | Qed. | ||
49 | |||
50 | (* Copied from stdpp, originates from Baader and Nipkow (1998) *) | ||
51 | Definition 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) *) | ||
55 | Lemma semi_confluence__cr {A} (R : relation A) : | ||
56 | semi_confluent R → cr R. | ||
57 | Proof. | ||
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). | ||
73 | Qed. | ||
@@ -0,0 +1,167 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From stdpp Require Import gmap. | ||
3 | From mininix Require Import binop expr matching relations. | ||
4 | |||
5 | Definition attrset := is_Some ∘ maybe V_Attrset. | ||
6 | |||
7 | Reserved Infix "-->base" (right associativity, at level 55). | ||
8 | |||
9 | Inductive 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 | ||
73 | where "e -->base e'" := (base_step e e'). | ||
74 | |||
75 | Notation "e '-->base*' e'" := (rtc base_step e e') | ||
76 | (right associativity, at level 55). | ||
77 | |||
78 | Hint Constructors base_step : core. | ||
79 | |||
80 | Variant 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 | |||
106 | Hint Constructors is_ctx_item : core. | ||
107 | |||
108 | Inductive 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 | |||
115 | Hint 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 | | | *) | ||
123 | Reserved Infix "-->" (right associativity, at level 55). | ||
124 | |||
125 | Variant 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 | ||
130 | where "e --> e'" := (step e e'). | ||
131 | |||
132 | Hint Constructors step : core. | ||
133 | |||
134 | Notation "e '-->*' e'" := (rtc step e e') (right associativity, at level 55). | ||
135 | |||
136 | (** Theories for contexts *) | ||
137 | |||
138 | Lemma is_ctx_once uf_ext uf_int E : | ||
139 | is_ctx_item uf_ext uf_int E → is_ctx uf_ext uf_int E. | ||
140 | Proof. intros. eapply IsCtx_Compose; [done | constructor]. Qed. | ||
141 | |||
142 | Lemma is_ctx_item_ext_imp E uf_int : | ||
143 | is_ctx_item false uf_int E → is_ctx_item true uf_int E. | ||
144 | Proof. intros H. inv H; constructor. Qed. | ||
145 | |||
146 | Lemma 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). | ||
150 | Proof. | ||
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. | ||
158 | Qed. | ||
159 | |||
160 | Lemma 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. | ||
163 | Proof. | ||
164 | intros Hctx. inv Hctx. | ||
165 | - by right. | ||
166 | - left. eapply is_ctx_ext_imp; [apply H | apply H0]. | ||
167 | Qed. | ||
diff --git a/semprop.v b/semprop.v new file mode 100644 index 0000000..3af718d --- /dev/null +++ b/semprop.v | |||
@@ -0,0 +1,426 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From stdpp Require Import gmap option tactics. | ||
3 | From mininix Require Import binop expr maptools matching relations sem. | ||
4 | |||
5 | Lemma ctx_item_inj E uf_ext uf_int : | ||
6 | is_ctx_item uf_ext uf_int E → | ||
7 | Inj (=) (=) E. | ||
8 | Proof. | ||
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. | ||
13 | Qed. | ||
14 | |||
15 | Global Instance id_inj {A} : Inj (=) (=) (@id A). | ||
16 | Proof. by unfold Inj. Qed. | ||
17 | |||
18 | Lemma ctx_inj E uf_ext uf_int : | ||
19 | is_ctx uf_ext uf_int E → | ||
20 | Inj (=) (=) E. | ||
21 | Proof. | ||
22 | intros Hctx. | ||
23 | induction Hctx. | ||
24 | - apply id_inj. | ||
25 | - apply ctx_item_inj in H. | ||
26 | by apply compose_inj with (=). | ||
27 | Qed. | ||
28 | |||
29 | Lemma base_step_deterministic : deterministic base_step. | ||
30 | Proof. | ||
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. | ||
51 | Qed. | ||
52 | |||
53 | Reserved Notation "e '-/' uf '/->' e'" (right associativity, at level 55). | ||
54 | |||
55 | Inductive 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 | ||
60 | where "e -/ uf /-> e'" := (fstep uf e e'). | ||
61 | |||
62 | Hint Constructors fstep : core. | ||
63 | |||
64 | Lemma ufstep e e' : e -/false/-> e' ↔ e --> e'. | ||
65 | Proof. split; intros; inv H; by econstructor. Qed. | ||
66 | |||
67 | Lemma 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. | ||
71 | Proof. | ||
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. | ||
395 | Qed. | ||
396 | |||
397 | Lemma step_strongly_confluent_aux x y1 y2 : | ||
398 | x --> y1 → | ||
399 | x --> y2 → | ||
400 | y1 = y2 ∨ ∃ z, y1 --> z ∧ y2 --> z. | ||
401 | Proof. | ||
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. | ||
407 | Qed. | ||
408 | |||
409 | Theorem step_strongly_confluent : strongly_confluent step. | ||
410 | Proof. | ||
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. | ||
417 | Qed. | ||
418 | |||
419 | Lemma step_semi_confluent : semi_confluent step. | ||
420 | Proof. apply strong__semi_confluence. apply step_strongly_confluent. Qed. | ||
421 | |||
422 | Lemma step_cr : cr step. | ||
423 | Proof. apply semi_confluence__cr. apply step_semi_confluent. Qed. | ||
424 | |||
425 | Theorem step_confluent : confluent step. | ||
426 | Proof. 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 @@ | |||
1 | Require Import Coq.NArith.BinNat. | ||
2 | Require Import Coq.Strings.Ascii. | ||
3 | Require Import Coq.Strings.String. | ||
4 | From stdpp Require Import fin_sets gmap option. | ||
5 | From mininix Require Import expr maptools. | ||
6 | |||
7 | Open Scope string_scope. | ||
8 | Open Scope N_scope. | ||
9 | Open Scope Z_scope. | ||
10 | Open Scope nat_scope. | ||
11 | |||
12 | Definition nonrecs : gmap string b_rhs → gmap string expr := | ||
13 | omap (λ b, match b with B_Nonrec e => Some e | _ => None end). | ||
14 | |||
15 | Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs. | ||
16 | Proof. | ||
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. | ||
23 | Qed. | ||
24 | |||
25 | Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs. | ||
26 | Proof. | ||
27 | unfold rec_subst. | ||
28 | rewrite <-map_fmap_compose. | ||
29 | unfold compose. | ||
30 | by rewrite map_fmap_id. | ||
31 | Qed. | ||
32 | |||
33 | Definition ascii_ltb (c1 c2 : ascii) : bool := | ||
34 | bool_decide (N_of_ascii c1 < N_of_ascii c2)%N. | ||
35 | |||
36 | Fixpoint 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 | |||
43 | Fixpoint 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 | |||
57 | Definition 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 | ]}. | ||
@@ -0,0 +1,630 @@ | |||
1 | Require Import Coq.Strings.String. | ||
2 | From stdpp Require Import base gmap relations tactics. | ||
3 | From mininix Require Import | ||
4 | binop expr interpreter maptools matching relations sem. | ||
5 | |||
6 | Lemma strong_value_stuck sv : ¬ ∃ e, expr_from_strong_value sv --> e. | ||
7 | Proof. | ||
8 | intros []. destruct sv; inv H; inv H1; | ||
9 | simplify_option_eq; (try inv H2); inv H. | ||
10 | Qed. | ||
11 | |||
12 | Lemma strong_value_stuck_rtc sv e: | ||
13 | expr_from_strong_value sv -->* e → | ||
14 | e = expr_from_strong_value sv. | ||
15 | Proof. | ||
16 | intros. inv H. | ||
17 | - reflexivity. | ||
18 | - exfalso. apply strong_value_stuck with (sv := sv). by exists y. | ||
19 | Qed. | ||
20 | |||
21 | Lemma force__strong_value (e : expr) (v : value) : | ||
22 | X_Force e -->* v → | ||
23 | ∃ sv, v = value_from_strong_value sv. | ||
24 | Proof. | ||
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. | ||
38 | Qed. | ||
39 | |||
40 | Lemma 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. | ||
43 | Proof. | ||
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. | ||
54 | Qed. | ||
55 | |||
56 | Lemma 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. | ||
60 | Proof. apply map_Forall2_fmap_r_L. Qed. | ||
61 | |||
62 | Lemma 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)))). | ||
68 | Proof. | ||
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. | ||
98 | Qed. | ||
99 | |||
100 | Lemma 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). | ||
104 | Proof. | ||
105 | intros Him1. | ||
106 | rewrite fmap_insert. | ||
107 | rewrite <-insert_union_l. | ||
108 | by rewrite <-insert_union_r. | ||
109 | Qed. | ||
110 | |||
111 | Lemma 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. | ||
115 | Proof. | ||
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. | ||
123 | Qed. | ||
124 | |||
125 | Lemma 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))). | ||
129 | Proof. | ||
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. | ||
145 | Qed. | ||
146 | |||
147 | (* See 194+2024-0525-2305 for proof sketch *) | ||
148 | Lemma 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))). | ||
152 | Proof. | ||
153 | pose proof (force_map_fmap_union ∅ svs es). | ||
154 | rewrite fmap_empty in H. by do 2 rewrite map_union_empty in H. | ||
155 | Qed. | ||
156 | |||
157 | Lemma id_compose_l {A B} (f : A → B) : id ∘ f = f. | ||
158 | Proof. done. Qed. | ||
159 | |||
160 | Lemma 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). | ||
164 | Proof. | ||
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. | ||
174 | Qed. | ||
175 | |||
176 | Lemma ctx_mstep e e' E : | ||
177 | e -->* e' → is_ctx false false E → E e -->* E e'. | ||
178 | Proof. | ||
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. | ||
188 | Qed. | ||
189 | |||
190 | Definition 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 | |||
195 | Lemma nonempty_ctx_mstep e e' uf_int E : | ||
196 | e -->* e' → is_nonempty_ctx false uf_int E → E e -->* E e'. | ||
197 | Proof. | ||
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. | ||
221 | Qed. | ||
222 | |||
223 | Lemma force_strong_value (sv : strong_value) : | ||
224 | X_Force sv -->* sv. | ||
225 | Proof. | ||
226 | destruct sv using strong_value_ind'; | ||
227 | apply rtc_once; eapply E_Ctx with (E := id); constructor. | ||
228 | Qed. | ||
229 | |||
230 | Lemma id_compose_r {A B} (f : A → B) : f ∘ id = f. | ||
231 | Proof. done. Qed. | ||
232 | |||
233 | Lemma force_idempotent e (v' : value) : | ||
234 | X_Force e -->* v' → | ||
235 | X_Force (X_Force e) -->* v'. | ||
236 | Proof. | ||
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. | ||
245 | Qed. | ||
246 | |||
247 | (* Conditional force *) | ||
248 | Definition cforce (uf : bool) e := if uf then X_Force e else e. | ||
249 | |||
250 | Lemma cforce_strong_value uf (sv : strong_value) : | ||
251 | cforce uf sv -->* sv. | ||
252 | Proof. destruct uf; try done. apply force_strong_value. Qed. | ||
253 | |||
254 | Theorem eval_sound_strong n uf e v' : | ||
255 | eval n uf e = Some v' → | ||
256 | cforce uf e -->* v'. | ||
257 | Proof. | ||
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). | ||
617 | Qed. | ||
618 | |||
619 | Lemma value_stuck v : ¬ ∃ e', X_V v --> e'. | ||
620 | Proof. | ||
621 | induction v; intros [e' He']; inversion He'; | ||
622 | subst; (inv H0; [inv H1 | inv H2]). | ||
623 | Qed. | ||
624 | |||
625 | Theorem eval_sound_weak e v' n : eval n false e = Some v' → is_nf_of step e v'. | ||
626 | Proof. | ||
627 | intros Heval. | ||
628 | pose proof (eval_sound_strong _ _ _ _ Heval). | ||
629 | split; [done | apply value_stuck]. | ||
630 | Qed. | ||