diff options
author | Rutger Broekhoff | 2024-06-27 01:56:05 +0200 |
---|---|---|
committer | Rutger Broekhoff | 2024-06-27 01:56:05 +0200 |
commit | 4598e77a9406d8040357c943a05dd1ab939932db (patch) | |
tree | e990beaa94803da3585547f22e186e8819f6a887 | |
parent | 73df1945b31c0beee88cf4476df4ccd09d31403b (diff) | |
download | mininix-formalization-4598e77a9406d8040357c943a05dd1ab939932db.tar.gz mininix-formalization-4598e77a9406d8040357c943a05dd1ab939932db.zip |
Tidy up project
* Write README.md
* Add LICENSE
* Clean up some theorems and proofs
-rw-r--r-- | LICENSE | 30 | ||||
-rw-r--r-- | README.md | 38 | ||||
-rw-r--r-- | complete.v | 58 | ||||
-rw-r--r-- | expr.v | 6 | ||||
-rw-r--r-- | flake.nix | 1 | ||||
-rw-r--r-- | maptools.v | 63 | ||||
-rw-r--r-- | matching.v | 29 | ||||
-rw-r--r-- | relations.v | 19 | ||||
-rw-r--r-- | semprop.v | 197 | ||||
-rw-r--r-- | shared.v | 11 | ||||
-rw-r--r-- | sound.v | 56 |
11 files changed, 221 insertions, 287 deletions
@@ -0,0 +1,30 @@ | |||
1 | All files in this repository are available for use under the BSD 3-Clause "New" | ||
2 | or "Revised License". The terms of the license are included below. | ||
3 | SPDX license identifier: BSD-3-Clause. | ||
4 | |||
5 | ===================================== | ||
6 | |||
7 | Copyright (c) 2024 Rutger Broekhoff. | ||
8 | |||
9 | Redistribution and use in source and binary forms, with or without | ||
10 | modification, are permitted provided that the following conditions are met: | ||
11 | |||
12 | 1. Redistributions of source code must retain the above copyright notice, this | ||
13 | list of conditions and the following disclaimer. | ||
14 | 2. Redistributions in binary form must reproduce the above copyright notice, | ||
15 | this list of conditions and the following disclaimer in the documentation | ||
16 | and/or other materials provided with the distribution. | ||
17 | 3. Neither the name of the copyright holder nor the names of its contributors | ||
18 | may be used to endorse or promote products derived from this software | ||
19 | without specific prior written permission. | ||
20 | |||
21 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND | ||
22 | ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED | ||
23 | WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE | ||
24 | DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE | ||
25 | FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL | ||
26 | DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR | ||
27 | SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER | ||
28 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, | ||
29 | OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE | ||
30 | OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. | ||
diff --git a/README.md b/README.md new file mode 100644 index 0000000..125ea10 --- /dev/null +++ b/README.md | |||
@@ -0,0 +1,38 @@ | |||
1 | Coq Formalization for Mininix | ||
2 | ============================= | ||
3 | |||
4 | [![License](https://img.shields.io/badge/License-BSD_3--Clause-blue.svg)](https://opensource.org/licenses/BSD-3-Clause) | ||
5 | |||
6 | Mininix is a smaller version of the Nix expression language. This repository | ||
7 | provides the mechanization of the semantics and reference interpreter for this | ||
8 | language in the [Coq](https://coq.inria.fr/) proof assistant. For more details, | ||
9 | I refer to my bachelor' thesis. I will link to it when it is made available on | ||
10 | the [thesis archive](https://www.cs.ru.nl/bachelors-theses/) page of | ||
11 | [iCIS](https://www.ru.nl/en/institute-for-computing-and-information-sciences). | ||
12 | |||
13 | ## Development | ||
14 | |||
15 | During my thesis, I used Nix to manage the Coq installation for this thesis. | ||
16 | If you use Nix, it should be easy to build/check the codebase. If not, this | ||
17 | might be a bit more tricky. | ||
18 | |||
19 | ### Using Nix | ||
20 | |||
21 | I have attached a `flake.nix` and `flake.lock` file, which should make my setup | ||
22 | reproducible. Assuming a working Nix installation with flake support and the | ||
23 | Nix command enabled, simply running `nix develop` followed by `make` should run | ||
24 | `coqc` on all files. If you have a working [direnv](https://direnv.net/) | ||
25 | installation, simply running `direnv allow` (after inspecting the `.envrc` | ||
26 | file) should make the right version of Coq available. | ||
27 | |||
28 | ### Without Nix | ||
29 | |||
30 | There are two things you need to have available. The current `flake.lock` | ||
31 | ensures that we have the following software: | ||
32 | |||
33 | - Coq, version 8.19.2. | ||
34 | - [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp), version 1.10.0. | ||
35 | You may be able to install Coq-std++ via opam, as described in the README of | ||
36 | Coq-std++. However, your operating system's package repositories may also | ||
37 | provide a package. Consider taking a look at [the Repology | ||
38 | page](https://repology.org/project/coq-stdpp/packages). | ||
@@ -34,36 +34,34 @@ Proof. | |||
34 | induction v using strong_value_ind'; try by exists 2. | 34 | induction v using strong_value_ind'; try by exists 2. |
35 | unfold expr_from_strong_value. simpl. | 35 | unfold expr_from_strong_value. simpl. |
36 | fold expr_from_strong_value. | 36 | fold expr_from_strong_value. |
37 | induction bs using map_ind. | 37 | induction bs using map_ind; [by exists 2|]. |
38 | + by exists 2. | 38 | apply map_Forall_insert in H as [[n Hn] H2]; try done. |
39 | + apply map_Forall_insert in H as [[n Hn] H2]; try done. | 39 | apply IHbs in H2 as [o Ho]. clear IHbs. |
40 | apply IHbs in H2 as [o Ho]. clear IHbs. | 40 | exists (S (n `max` o)). |
41 | exists (S (n `max` o)). | 41 | rewrite eval_S. csimpl. |
42 | rewrite eval_S. csimpl. | 42 | setoid_rewrite map_mapM_Some_2_L |
43 | setoid_rewrite map_mapM_Some_2_L | 43 | with (m2 := value_from_strong_value <$> <[i := x]>m); |
44 | with (m2 := value_from_strong_value <$> <[i := x]>m); csimpl. | 44 | csimpl; [by rewrite <-map_fmap_compose|]. |
45 | * by rewrite <-map_fmap_compose. | 45 | destruct o as [|o]; csimpl in *; try discriminate. |
46 | * destruct o as [|o]; csimpl in *; try discriminate. | 46 | apply map_Forall2_alt_L. |
47 | apply map_Forall2_alt_L. | 47 | split; [set_solver|]. |
48 | split. | 48 | intros j u v ??. rewrite eval_S in Ho. |
49 | -- set_solver. | 49 | apply bind_Some in Ho as [vs [Ho1 Ho2]]. |
50 | -- intros j u v ??. rewrite eval_S in Ho. | 50 | setoid_rewrite map_mapM_Some_L in Ho1. simplify_eq. |
51 | apply bind_Some in Ho as [vs [Ho1 Ho2]]. | 51 | unfold expr_from_strong_value in Ho2. |
52 | setoid_rewrite map_mapM_Some_L in Ho1. simplify_eq. | 52 | rewrite map_fmap_compose in Ho2. |
53 | unfold expr_from_strong_value in Ho2. | 53 | simplify_eq. |
54 | rewrite map_fmap_compose in Ho2. | 54 | destruct (decide (i = j)). |
55 | simplify_eq. | 55 | - simplify_eq. |
56 | destruct (decide (i = j)). | 56 | repeat rewrite lookup_fmap, lookup_insert in *. |
57 | ++ simplify_eq. | 57 | simplify_eq/=. |
58 | repeat rewrite lookup_fmap, lookup_insert in *. | 58 | apply eval_le with (n := n); lia || done. |
59 | simplify_eq/=. | 59 | - repeat rewrite lookup_fmap, lookup_insert_ne in * by done. |
60 | apply eval_le with (n := n); lia || done. | 60 | repeat rewrite <-lookup_fmap in *. |
61 | ++ repeat rewrite lookup_fmap, lookup_insert_ne in * by done. | 61 | apply map_Forall2_alt_L in Ho1. |
62 | repeat rewrite <-lookup_fmap in *. | 62 | destruct Ho1 as [Ho1 Ho2]. |
63 | apply map_Forall2_alt_L in Ho1. | 63 | apply eval_le with (n := o); try lia. |
64 | destruct Ho1 as [Ho1 Ho2]. | 64 | by apply Ho2 with (i := j). |
65 | apply eval_le with (n := o); try lia. | ||
66 | by apply Ho2 with (i := j). | ||
67 | Qed. | 65 | Qed. |
68 | 66 | ||
69 | Lemma eval_force_strong_value' v : | 67 | Lemma eval_force_strong_value' v : |
@@ -60,6 +60,12 @@ Instance Maybe_X_Attrset : Maybe X_Attrset := λ e, | |||
60 | | _ => None | 60 | | _ => None |
61 | end. | 61 | end. |
62 | 62 | ||
63 | Instance Maybe_X_V : Maybe X_V := λ e, | ||
64 | match e with | ||
65 | | X_V v => Some v | ||
66 | | _ => None | ||
67 | end. | ||
68 | |||
63 | Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs, | 69 | Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs, |
64 | match rhs with | 70 | match rhs with |
65 | | B_Nonrec e => Some e | 71 | | B_Nonrec e => Some e |
@@ -12,7 +12,6 @@ | |||
12 | { | 12 | { |
13 | devShells.default = with pkgs; mkShell { | 13 | devShells.default = with pkgs; mkShell { |
14 | buildInputs = [ | 14 | buildInputs = [ |
15 | coqPackages.coqide | ||
16 | coqPackages.stdpp | 15 | coqPackages.stdpp |
17 | coq | 16 | coq |
18 | ]; | 17 | ]; |
@@ -4,8 +4,8 @@ From stdpp Require Import countable fin_maps fin_map_dom. | |||
4 | (** Generic lemmas for finite maps and their domains *) | 4 | (** Generic lemmas for finite maps and their domains *) |
5 | 5 | ||
6 | Lemma map_insert_empty_lookup {A} `{FinMap K M} | 6 | Lemma map_insert_empty_lookup {A} `{FinMap K M} |
7 | (i j : K) (u v : A) : | 7 | (i j : K) (x y : A) : |
8 | <[i := u]> (∅ : M A) !! j = Some v → i = j ∧ v = u. | 8 | <[i := x]> (∅ : M A) !! j = Some y → i = j ∧ y = x. |
9 | Proof. | 9 | Proof. |
10 | intros Hiel. | 10 | intros Hiel. |
11 | destruct (decide (i = j)). | 11 | destruct (decide (i = j)). |
@@ -106,6 +106,32 @@ Lemma map_dom_insert_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} | |||
106 | dom (delete i m1) = dom (delete i m2) ∧ i ∈ dom m2. | 106 | dom (delete i m1) = dom (delete i m2) ∧ i ∈ dom m2. |
107 | Proof. set_solver. Qed. | 107 | Proof. set_solver. Qed. |
108 | 108 | ||
109 | (* Copied from stdpp and changed so that the value types | ||
110 | of m1 and m2 are decoupled *) | ||
111 | Lemma map_dom_subseteq_size `{FinMapDom K M D} {A B} (m1 : M A) (m2 : M B) : | ||
112 | dom m2 ⊆ dom m1 → size m2 ≤ size m1. | ||
113 | Proof. | ||
114 | revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom. | ||
115 | { rewrite map_size_empty. lia. } | ||
116 | rewrite dom_insert in Hdom. | ||
117 | assert (i ∉ dom m2) by (by apply not_elem_of_dom). | ||
118 | assert (i ∈ dom m1) as [x' Hx'] % elem_of_dom by set_solver. | ||
119 | rewrite <-(insert_delete m1 i x') by done. | ||
120 | rewrite !map_size_insert_None, <-Nat.succ_le_mono | ||
121 | by (by rewrite ?lookup_delete). | ||
122 | apply IH. rewrite dom_delete. set_solver. | ||
123 | Qed. | ||
124 | |||
125 | Lemma map_dom_empty_subset `{Countable K} `{FinMapDom K M D} {A B} (m : M A) : | ||
126 | dom m ⊆ dom (∅ : M B) → m = ∅. | ||
127 | Proof. | ||
128 | intros Hdom. | ||
129 | apply map_dom_subseteq_size in Hdom. | ||
130 | rewrite map_size_empty in Hdom. | ||
131 | inv Hdom. | ||
132 | by apply map_size_empty_inv. | ||
133 | Qed. | ||
134 | |||
109 | (** map_mapM *) | 135 | (** map_mapM *) |
110 | 136 | ||
111 | Definition map_mapM {M : Type → Type} `{MBind F} `{MRet F} `{FinMap K M} {A B} | 137 | Definition map_mapM {M : Type → Type} `{MBind F} `{MRet F} `{FinMap K M} {A B} |
@@ -137,11 +163,10 @@ Proof. | |||
137 | Qed. | 163 | Qed. |
138 | 164 | ||
139 | Lemma map_mapM_option_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} | 165 | 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) | 166 | (f : A → option B) (m1 : M A) (m2 m2' : M B) (i : K) (x : A) : |
141 | (i : K) (x : A) (x' : B) : | 167 | m1 !! i = None → |
142 | m1 !! i = None → | 168 | map_mapM f (<[i := x]>m1) = Some m2 → |
143 | map_mapM f (<[i := x]>m1) = Some m2 → | 169 | ∃ x', f x = Some x' ∧ map_mapM f m1 = Some (delete i m2). |
144 | ∃ x', f x = Some x' ∧ map_mapM f m1 = Some (delete i m2). | ||
145 | Proof. | 170 | Proof. |
146 | intros Helem HmapM. | 171 | intros Helem HmapM. |
147 | unfold map_mapM in HmapM. | 172 | unfold map_mapM in HmapM. |
@@ -315,7 +340,7 @@ Qed. | |||
315 | 340 | ||
316 | Lemma map_Forall2_impl_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} | 341 | Lemma map_Forall2_impl_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} |
317 | (R1 R2 : A → B → Prop) : | 342 | (R1 R2 : A → B → Prop) : |
318 | (∀ a b, R1 a b → R2 a b) → | 343 | (∀ x y, R1 x y → R2 x y) → |
319 | ∀ (m1 : M A) (m2 : M B), | 344 | ∀ (m1 : M A) (m2 : M B), |
320 | map_Forall2 R1 m1 m2 → map_Forall2 R2 m1 m2. | 345 | map_Forall2 R1 m1 m2 → map_Forall2 R2 m1 m2. |
321 | Proof. | 346 | Proof. |
@@ -327,8 +352,8 @@ Proof. | |||
327 | Qed. | 352 | Qed. |
328 | 353 | ||
329 | Lemma map_Forall2_fmap_r_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B C} | 354 | 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) : | 355 | (R : 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. | 356 | map_Forall2 R m1 (f <$> m2) → map_Forall2 (λ x y, R x (f y)) m1 m2. |
332 | Proof. | 357 | Proof. |
333 | intros HForall2. | 358 | intros HForall2. |
334 | unfold map_Forall2, map_relation, option_relation in *. | 359 | unfold map_Forall2, map_relation, option_relation in *. |
@@ -355,10 +380,10 @@ Proof. | |||
355 | Qed. | 380 | Qed. |
356 | 381 | ||
357 | Lemma map_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} | 382 | Lemma map_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} |
358 | (i : K) (x1 x2 : A) (m1 m2 : M A) : | 383 | (i : K) (x y : A) (m1 m2 : M A) : |
359 | x1 = x2 → | 384 | x = y → |
360 | delete i m1 = delete i m2 → | 385 | delete i m1 = delete i m2 → |
361 | <[i := x1]>m1 = <[i := x2]>m2. | 386 | <[i := x]>m1 = <[i := y]>m2. |
362 | Proof. | 387 | Proof. |
363 | intros Heq Hdel. | 388 | intros Heq Hdel. |
364 | apply map_Forall2_eq_L. | 389 | apply map_Forall2_eq_L. |
@@ -367,8 +392,8 @@ Proof. | |||
367 | Qed. | 392 | Qed. |
368 | 393 | ||
369 | Lemma map_insert_rev_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} | 394 | Lemma map_insert_rev_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} |
370 | (i : K) (x1 x2 : A) (m1 m2 : M A) : | 395 | (m1 m2 : M A) (i : K) (x y : A) : |
371 | <[i := x1]>m1 = <[i := x2]>m2 → x1 = x2 ∧ delete i m1 = delete i m2. | 396 | <[i := x]>m1 = <[i := y]>m2 → x = y ∧ delete i m1 = delete i m2. |
372 | Proof. | 397 | Proof. |
373 | intros Heq. apply map_Forall2_eq_L in Heq. | 398 | intros Heq. apply map_Forall2_eq_L in Heq. |
374 | apply map_Forall2_insert_inv in Heq as [Heq1 Heq2]. | 399 | apply map_Forall2_insert_inv in Heq as [Heq1 Heq2]. |
@@ -376,13 +401,13 @@ Proof. | |||
376 | Qed. | 401 | Qed. |
377 | 402 | ||
378 | Lemma map_insert_rev_1_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} | 403 | Lemma map_insert_rev_1_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} |
379 | (i : K) (x1 x2 : A) (m1 m2 : M A) : | 404 | (m1 m2 : M A) (i : K) (x y : A) : |
380 | <[i := x1]>m1 = <[i := x2]>m2 → x1 = x2. | 405 | <[i := x]>m1 = <[i := y]>m2 → x = y. |
381 | Proof. apply map_insert_rev_L. Qed. | 406 | Proof. apply map_insert_rev_L. Qed. |
382 | 407 | ||
383 | Lemma map_insert_rev_2_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} | 408 | Lemma map_insert_rev_2_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} |
384 | (i : K) (x1 x2 : A) (m1 m2 : M A) : | 409 | (m1 m2 : M A) (i : K) (x y : A) : |
385 | <[i := x1]>m1 = <[i := x2]>m2 → delete i m1 = delete i m2. | 410 | <[i := x]>m1 = <[i := y]>m2 → delete i m1 = delete i m2. |
386 | Proof. apply map_insert_rev_L. Qed. | 411 | Proof. apply map_insert_rev_L. Qed. |
387 | 412 | ||
388 | Lemma map_Forall2_alt_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} | 413 | Lemma map_Forall2_alt_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} |
@@ -64,32 +64,6 @@ Definition matches (m : matcher) (bs : gmap string expr) : | |||
64 | snd <$> matches_aux ms bs | 64 | snd <$> matches_aux ms bs |
65 | end. | 65 | end. |
66 | 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, ∅). | 67 | Lemma matches_aux_empty bs : matches_aux ∅ bs = Some (bs, ∅). |
94 | Proof. done. Qed. | 68 | Proof. done. Qed. |
95 | 69 | ||
@@ -496,8 +470,7 @@ Proof. | |||
496 | revert strict bs brs Hmatches. | 470 | revert strict bs brs Hmatches. |
497 | induction ms using map_ind; intros strict bs brs Hmatches. | 471 | induction ms using map_ind; intros strict bs brs Hmatches. |
498 | - destruct strict; simplify_option_eq. | 472 | - destruct strict; simplify_option_eq. |
499 | + apply dom_empty_subset in H0. simplify_eq. | 473 | + apply map_dom_empty_subset in H0. simplify_eq. constructor. |
500 | constructor. | ||
501 | + constructor. | 474 | + constructor. |
502 | - destruct x. | 475 | - destruct x. |
503 | + apply matches_step' in Hmatches as He. | 476 | + apply matches_step' in Hmatches as He. |
diff --git a/relations.v b/relations.v index 9bfb7e6..7523c96 100644 --- a/relations.v +++ b/relations.v | |||
@@ -1,10 +1,14 @@ | |||
1 | (** This files contains definitions for determinism, strong confluence, | ||
2 | * semi-confluence, the Church-Rosser property and proofs about relationships | ||
3 | * of these properties. We use definitions and proofs from 'Term Rewriting and | ||
4 | * All That' by Franz Baader and Tobias Nipkow (1998). *) | ||
1 | From stdpp Require Import relations. | 5 | From stdpp Require Import relations. |
2 | 6 | ||
3 | Definition deterministic {A} (R : relation A) := | 7 | Definition deterministic {A} (R : relation A) := |
4 | ∀ x y1 y2, R x y1 → R x y2 → y1 = y2. | 8 | ∀ x y1 y2, R x y1 → R x y2 → y1 = y2. |
5 | 9 | ||
6 | (* As in Baader and Nipkow (1998): *) | 10 | (** Baader and Nipkow (1998), p. 9: |
7 | (* y is a normal form of x if x -->* y and y is in normal form. *) | 11 | * 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. | 12 | Definition is_nf_of `(R : relation A) x y := (rtc R x y) ∧ nf R y. |
9 | 13 | ||
10 | (** The reflexive closure. *) | 14 | (** The reflexive closure. *) |
@@ -14,15 +18,15 @@ Inductive rc {A} (R : relation A) : relation A := | |||
14 | 18 | ||
15 | Hint Constructors rc : core. | 19 | Hint Constructors rc : core. |
16 | 20 | ||
17 | (* Baader and Nipkow, Definition 2.7.3. *) | 21 | (** Baader and Nipkow, Definition 2.7.3. *) |
18 | Definition strongly_confluent {A} (R : relation A) := | 22 | 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. | 23 | ∀ x y1 y2, R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rc R y2 z. |
20 | 24 | ||
21 | (* Baader and Nipkow, Definition 2.1.4. *) | 25 | (** Baader and Nipkow, Definition 2.1.4. *) |
22 | Definition semi_confluent {A} (R : relation A) := | 26 | 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. | 27 | ∀ x y1 y2, R x y1 → rtc R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z. |
24 | 28 | ||
25 | (* Lemma 2.7.4 from Baader and Nipkow *) | 29 | (** Lemma 2.7.4 from Baader and Nipkow *) |
26 | Lemma strong__semi_confluence {A} (R : relation A) : | 30 | Lemma strong__semi_confluence {A} (R : relation A) : |
27 | strongly_confluent R → semi_confluent R. | 31 | strongly_confluent R → semi_confluent R. |
28 | Proof. | 32 | Proof. |
@@ -47,11 +51,12 @@ Proof. | |||
47 | by apply rtc_transitive with (y := y2). | 51 | by apply rtc_transitive with (y := y2). |
48 | Qed. | 52 | Qed. |
49 | 53 | ||
50 | (* Copied from stdpp, originates from Baader and Nipkow (1998) *) | 54 | (** Baader and Nipkow, Definition 2.1.3. |
55 | * Copied from stdpp v1.10.0 (confluent_alt). *) | ||
51 | Definition cr {A} (R : relation A) := | 56 | Definition cr {A} (R : relation A) := |
52 | ∀ x y, rtsc R x y → ∃ z, rtc R x z ∧ rtc R y z. | 57 | ∀ x y, rtsc R x y → ∃ z, rtc R x z ∧ rtc R y z. |
53 | 58 | ||
54 | (* Part of Lemma 2.1.5 from Baader and Nipkow (1998) *) | 59 | (** Part of Lemma 2.1.5 from Baader and Nipkow (1998) *) |
55 | Lemma semi_confluence__cr {A} (R : relation A) : | 60 | Lemma semi_confluence__cr {A} (R : relation A) : |
56 | semi_confluent R → cr R. | 61 | semi_confluent R → cr R. |
57 | Proof. | 62 | Proof. |
@@ -77,173 +77,36 @@ Proof. | |||
77 | intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2. | 77 | intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2. |
78 | - (* L: id, R: id *) left. by eapply base_step_deterministic. | 78 | - (* L: id, R: id *) left. by eapply base_step_deterministic. |
79 | - (* L: id, R: ∘ *) simplify_eq/=. | 79 | - (* L: id, R: ∘ *) simplify_eq/=. |
80 | inv H. | 80 | inv H; try inv select (_ -->base b12); |
81 | + inv Hbase1. | 81 | (inv select (is_ctx _ _ _); |
82 | * inv H0. | 82 | [inv select (b21 -->base b22) |
83 | -- inv Hbase2. | 83 | |inv select (is_ctx_item _ _ _)]). |
84 | -- inv H. | 84 | simplify_option_eq. |
85 | * inv H0. | 85 | destruct sv; try discriminate. |
86 | -- inv Hbase2. | 86 | exfalso. clear uf. simplify_option_eq. |
87 | -- inv H1. inv H. | 87 | apply fmap_insert_lookup in H1. simplify_option_eq. |
88 | + inv Hbase1. | 88 | revert bs0 x H H1 Heqo. |
89 | * inv H0. | 89 | induction H2; intros bs0 x H' H1 Heqo; [inv Hbase2|]. |
90 | -- inv Hbase2. | 90 | simplify_option_eq. |
91 | -- inv H. | 91 | inv H. destruct H'; try discriminate. |
92 | * inv H0. | 92 | inv H1. apply fmap_insert_lookup in H0. simplify_option_eq. |
93 | -- inv Hbase2. | 93 | by eapply IHis_ctx. |
94 | -- inv H. | 94 | - (* L: ∘, R: id *) simplify_eq/=. |
95 | + inv Hbase1. | 95 | inv H; try inv select (_ -->base b22); |
96 | * inv H0. | 96 | (inv select (is_ctx _ _ _); |
97 | -- inv Hbase2. | 97 | [inv select (b11 -->base b12) |
98 | -- inv H. | 98 | |inv select (is_ctx_item _ _ _)]). |
99 | * inv H0. | 99 | clear IHHctx1. |
100 | -- inv Hbase2. | 100 | simplify_option_eq. |
101 | -- inv H1. | 101 | destruct sv; try discriminate. |
102 | + inv Hbase1. | 102 | exfalso. simplify_option_eq. |
103 | * inv H0. | 103 | apply fmap_insert_lookup in H0. simplify_option_eq. |
104 | -- inv Hbase2. | 104 | revert bs0 x H H0 Heqo. |
105 | -- inv H. | 105 | induction H1; intros bs0 x H' H0 Heqo; [inv Hbase1|]. |
106 | * inv H0. | 106 | simplify_option_eq. |
107 | -- inv Hbase2. | 107 | inv H. destruct H'; try discriminate. |
108 | -- inv H1. | 108 | inv H0. apply fmap_insert_lookup in H2. simplify_option_eq. |
109 | * inv H0. | 109 | by eapply IHis_ctx. |
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: ∘ *) | 110 | - (* L: ∘, R: ∘ *) |
248 | simplify_option_eq. | 111 | simplify_option_eq. |
249 | inv H; inv H0. | 112 | inv H; inv H0. |
@@ -14,12 +14,11 @@ Definition nonrecs : gmap string b_rhs → gmap string expr := | |||
14 | 14 | ||
15 | Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs. | 15 | Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs. |
16 | Proof. | 16 | Proof. |
17 | induction bs using map_ind. | 17 | induction bs using map_ind; [done|]. |
18 | - done. | 18 | unfold nonrecs. |
19 | - unfold nonrecs. | 19 | rewrite fmap_insert. |
20 | rewrite fmap_insert. | 20 | rewrite omap_insert_Some with (y := x); try done. |
21 | rewrite omap_insert_Some with (y := x); try done. | 21 | by f_equal. |
22 | by f_equal. | ||
23 | Qed. | 22 | Qed. |
24 | 23 | ||
25 | Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs. | 24 | Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs. |
@@ -13,9 +13,8 @@ Lemma strong_value_stuck_rtc sv e: | |||
13 | expr_from_strong_value sv -->* e → | 13 | expr_from_strong_value sv -->* e → |
14 | e = expr_from_strong_value sv. | 14 | e = expr_from_strong_value sv. |
15 | Proof. | 15 | Proof. |
16 | intros. inv H. | 16 | intros. inv H; [done|]. |
17 | - reflexivity. | 17 | exfalso. apply strong_value_stuck with (sv := sv). by exists y. |
18 | - exfalso. apply strong_value_stuck with (sv := sv). by exists y. | ||
19 | Qed. | 18 | Qed. |
20 | 19 | ||
21 | Lemma force__strong_value (e : expr) (v : value) : | 20 | Lemma force__strong_value (e : expr) (v : value) : |
@@ -68,33 +67,32 @@ Lemma force_map_fmap_union_insert (sws : gmap string strong_value) es k e sv : | |||
68 | Proof. | 67 | Proof. |
69 | intros [n Hsteps] % rtc_nsteps. | 68 | intros [n Hsteps] % rtc_nsteps. |
70 | revert sws es k e Hsteps. | 69 | revert sws es k e Hsteps. |
71 | induction n; intros sws es k e Hsteps. | 70 | induction n; intros sws es k e Hsteps; [inv Hsteps|]. |
72 | - inv Hsteps. | 71 | inv Hsteps. |
73 | - inv Hsteps. | 72 | inv H0. |
74 | inv H0. | 73 | inv H2. |
75 | inv H2. | 74 | - inv H3. inv H1. |
76 | + inv H3. inv H1. | 75 | + simplify_option_eq. unfold expr_from_strong_value, compose. |
77 | * simplify_option_eq. unfold expr_from_strong_value, compose. | 76 | by rewrite H4. |
78 | by rewrite H4. | 77 | + edestruct strong_value_stuck. exists y. done. |
79 | * edestruct strong_value_stuck. exists y. done. | 78 | - inv H0. simplify_option_eq. |
80 | + inv H0. simplify_option_eq. | 79 | apply rtc_transitive |
81 | apply rtc_transitive | 80 | with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪ |
82 | with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪ | 81 | (expr_from_strong_value <$> sws))))). |
83 | (expr_from_strong_value <$> sws))))). | 82 | + do 2 rewrite <-insert_union_l. |
84 | * do 2 rewrite <-insert_union_l. | 83 | apply rtc_once. |
85 | apply rtc_once. | 84 | eapply E_Ctx |
86 | eapply E_Ctx | 85 | with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪ |
87 | with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪ | 86 | (expr_from_strong_value <$> sws)))))). |
88 | (expr_from_strong_value <$> sws)))))). | 87 | * eapply IsCtx_Compose. |
89 | -- eapply IsCtx_Compose. | 88 | -- constructor. |
89 | -- eapply IsCtx_Compose | ||
90 | with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪ | ||
91 | (expr_from_strong_value <$> sws)))))). | ||
90 | ++ constructor. | 92 | ++ constructor. |
91 | ++ eapply IsCtx_Compose | 93 | ++ done. |
92 | with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪ | 94 | * done. |
93 | (expr_from_strong_value <$> sws)))))). | 95 | + by apply IHn. |
94 | ** constructor. | ||
95 | ** done. | ||
96 | -- done. | ||
97 | * by apply IHn. | ||
98 | Qed. | 96 | Qed. |
99 | 97 | ||
100 | Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x | 98 | Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x |