From 4598e77a9406d8040357c943a05dd1ab939932db Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Thu, 27 Jun 2024 01:56:05 +0200 Subject: Tidy up project * Write README.md * Add LICENSE * Clean up some theorems and proofs --- LICENSE | 30 +++++++++ README.md | 38 ++++++++++++ complete.v | 58 +++++++++--------- expr.v | 6 ++ flake.nix | 1 - maptools.v | 63 +++++++++++++------ matching.v | 29 +-------- relations.v | 19 +++--- semprop.v | 197 +++++++++--------------------------------------------------- shared.v | 11 ++-- sound.v | 56 +++++++++-------- 11 files changed, 221 insertions(+), 287 deletions(-) create mode 100644 LICENSE create mode 100644 README.md diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..c1ab0b4 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +All files in this repository are available for use under the BSD 3-Clause "New" +or "Revised License". The terms of the license are included below. +SPDX license identifier: BSD-3-Clause. + +===================================== + +Copyright (c) 2024 Rutger Broekhoff. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. +3. Neither the name of the copyright holder nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +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 @@ +Coq Formalization for Mininix +============================= + +[![License](https://img.shields.io/badge/License-BSD_3--Clause-blue.svg)](https://opensource.org/licenses/BSD-3-Clause) + +Mininix is a smaller version of the Nix expression language. This repository +provides the mechanization of the semantics and reference interpreter for this +language in the [Coq](https://coq.inria.fr/) proof assistant. For more details, +I refer to my bachelor' thesis. I will link to it when it is made available on +the [thesis archive](https://www.cs.ru.nl/bachelors-theses/) page of +[iCIS](https://www.ru.nl/en/institute-for-computing-and-information-sciences). + +## Development + +During my thesis, I used Nix to manage the Coq installation for this thesis. +If you use Nix, it should be easy to build/check the codebase. If not, this +might be a bit more tricky. + +### Using Nix + +I have attached a `flake.nix` and `flake.lock` file, which should make my setup +reproducible. Assuming a working Nix installation with flake support and the +Nix command enabled, simply running `nix develop` followed by `make` should run +`coqc` on all files. If you have a working [direnv](https://direnv.net/) +installation, simply running `direnv allow` (after inspecting the `.envrc` +file) should make the right version of Coq available. + +### Without Nix + +There are two things you need to have available. The current `flake.lock` +ensures that we have the following software: + +- Coq, version 8.19.2. +- [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp), version 1.10.0. + You may be able to install Coq-std++ via opam, as described in the README of + Coq-std++. However, your operating system's package repositories may also + provide a package. Consider taking a look at [the Repology + page](https://repology.org/project/coq-stdpp/packages). diff --git a/complete.v b/complete.v index 9939b50..5a2ccdc 100644 --- a/complete.v +++ b/complete.v @@ -34,36 +34,34 @@ Proof. induction v using strong_value_ind'; try by exists 2. unfold expr_from_strong_value. simpl. fold expr_from_strong_value. - induction bs using map_ind. - + by exists 2. - + apply map_Forall_insert in H as [[n Hn] H2]; try done. - apply IHbs in H2 as [o Ho]. clear IHbs. - exists (S (n `max` o)). - rewrite eval_S. csimpl. - setoid_rewrite map_mapM_Some_2_L - with (m2 := value_from_strong_value <$> <[i := x]>m); csimpl. - * by rewrite <-map_fmap_compose. - * destruct o as [|o]; csimpl in *; try discriminate. - apply map_Forall2_alt_L. - split. - -- set_solver. - -- intros j u v ??. rewrite eval_S in Ho. - apply bind_Some in Ho as [vs [Ho1 Ho2]]. - setoid_rewrite map_mapM_Some_L in Ho1. simplify_eq. - unfold expr_from_strong_value in Ho2. - rewrite map_fmap_compose in Ho2. - simplify_eq. - destruct (decide (i = j)). - ++ simplify_eq. - repeat rewrite lookup_fmap, lookup_insert in *. - simplify_eq/=. - apply eval_le with (n := n); lia || done. - ++ repeat rewrite lookup_fmap, lookup_insert_ne in * by done. - repeat rewrite <-lookup_fmap in *. - apply map_Forall2_alt_L in Ho1. - destruct Ho1 as [Ho1 Ho2]. - apply eval_le with (n := o); try lia. - by apply Ho2 with (i := j). + induction bs using map_ind; [by exists 2|]. + apply map_Forall_insert in H as [[n Hn] H2]; try done. + apply IHbs in H2 as [o Ho]. clear IHbs. + exists (S (n `max` o)). + rewrite eval_S. csimpl. + setoid_rewrite map_mapM_Some_2_L + with (m2 := value_from_strong_value <$> <[i := x]>m); + csimpl; [by rewrite <-map_fmap_compose|]. + destruct o as [|o]; csimpl in *; try discriminate. + apply map_Forall2_alt_L. + split; [set_solver|]. + intros j u v ??. rewrite eval_S in Ho. + apply bind_Some in Ho as [vs [Ho1 Ho2]]. + setoid_rewrite map_mapM_Some_L in Ho1. simplify_eq. + unfold expr_from_strong_value in Ho2. + rewrite map_fmap_compose in Ho2. + simplify_eq. + destruct (decide (i = j)). + - simplify_eq. + repeat rewrite lookup_fmap, lookup_insert in *. + simplify_eq/=. + apply eval_le with (n := n); lia || done. + - repeat rewrite lookup_fmap, lookup_insert_ne in * by done. + repeat rewrite <-lookup_fmap in *. + apply map_Forall2_alt_L in Ho1. + destruct Ho1 as [Ho1 Ho2]. + apply eval_le with (n := o); try lia. + by apply Ho2 with (i := j). Qed. Lemma eval_force_strong_value' v : diff --git a/expr.v b/expr.v index 11c0737..e770345 100644 --- a/expr.v +++ b/expr.v @@ -60,6 +60,12 @@ Instance Maybe_X_Attrset : Maybe X_Attrset := λ e, | _ => None end. +Instance Maybe_X_V : Maybe X_V := λ e, + match e with + | X_V v => Some v + | _ => None + end. + Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs, match rhs with | B_Nonrec e => Some e diff --git a/flake.nix b/flake.nix index e9c35a4..25361d2 100644 --- a/flake.nix +++ b/flake.nix @@ -12,7 +12,6 @@ { devShells.default = with pkgs; mkShell { buildInputs = [ - coqPackages.coqide coqPackages.stdpp coq ]; diff --git a/maptools.v b/maptools.v index 2478430..ce4022a 100644 --- a/maptools.v +++ b/maptools.v @@ -4,8 +4,8 @@ From stdpp Require Import countable fin_maps fin_map_dom. (** Generic lemmas for finite maps and their domains *) Lemma map_insert_empty_lookup {A} `{FinMap K M} - (i j : K) (u v : A) : - <[i := u]> (∅ : M A) !! j = Some v → i = j ∧ v = u. + (i j : K) (x y : A) : + <[i := x]> (∅ : M A) !! j = Some y → i = j ∧ y = x. Proof. intros Hiel. destruct (decide (i = j)). @@ -106,6 +106,32 @@ Lemma map_dom_insert_eq_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} dom (delete i m1) = dom (delete i m2) ∧ i ∈ dom m2. Proof. set_solver. Qed. +(* Copied from stdpp and changed so that the value types + of m1 and m2 are decoupled *) +Lemma map_dom_subseteq_size `{FinMapDom K M D} {A B} (m1 : M A) (m2 : M B) : + dom m2 ⊆ dom m1 → size m2 ≤ size m1. +Proof. + revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom. + { rewrite map_size_empty. lia. } + rewrite dom_insert in Hdom. + assert (i ∉ dom m2) by (by apply not_elem_of_dom). + assert (i ∈ dom m1) as [x' Hx'] % elem_of_dom by set_solver. + rewrite <-(insert_delete m1 i x') by done. + rewrite !map_size_insert_None, <-Nat.succ_le_mono + by (by rewrite ?lookup_delete). + apply IH. rewrite dom_delete. set_solver. +Qed. + +Lemma map_dom_empty_subset `{Countable K} `{FinMapDom K M D} {A B} (m : M A) : + dom m ⊆ dom (∅ : M B) → m = ∅. +Proof. + intros Hdom. + apply map_dom_subseteq_size in Hdom. + rewrite map_size_empty in Hdom. + inv Hdom. + by apply map_size_empty_inv. +Qed. + (** map_mapM *) Definition map_mapM {M : Type → Type} `{MBind F} `{MRet F} `{FinMap K M} {A B} @@ -137,11 +163,10 @@ Proof. Qed. Lemma map_mapM_option_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} - (f : A → option B) (m1 : M A) (m2 m2' : M B) - (i : K) (x : A) (x' : B) : - m1 !! i = None → - map_mapM f (<[i := x]>m1) = Some m2 → - ∃ x', f x = Some x' ∧ map_mapM f m1 = Some (delete i m2). + (f : A → option B) (m1 : M A) (m2 m2' : M B) (i : K) (x : A) : + m1 !! i = None → + map_mapM f (<[i := x]>m1) = Some m2 → + ∃ x', f x = Some x' ∧ map_mapM f m1 = Some (delete i m2). Proof. intros Helem HmapM. unfold map_mapM in HmapM. @@ -315,7 +340,7 @@ Qed. Lemma map_Forall2_impl_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} (R1 R2 : A → B → Prop) : - (∀ a b, R1 a b → R2 a b) → + (∀ x y, R1 x y → R2 x y) → ∀ (m1 : M A) (m2 : M B), map_Forall2 R1 m1 m2 → map_Forall2 R2 m1 m2. Proof. @@ -327,8 +352,8 @@ Proof. Qed. Lemma map_Forall2_fmap_r_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B C} - (P : A → C → Prop) (m1 : M A) (m2 : M B) (f : B → C) : - map_Forall2 P m1 (f <$> m2) → map_Forall2 (λ l r, P l (f r)) m1 m2. + (R : A → C → Prop) (m1 : M A) (m2 : M B) (f : B → C) : + map_Forall2 R m1 (f <$> m2) → map_Forall2 (λ x y, R x (f y)) m1 m2. Proof. intros HForall2. unfold map_Forall2, map_relation, option_relation in *. @@ -355,10 +380,10 @@ Proof. Qed. Lemma map_insert_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} - (i : K) (x1 x2 : A) (m1 m2 : M A) : - x1 = x2 → + (i : K) (x y : A) (m1 m2 : M A) : + x = y → delete i m1 = delete i m2 → - <[i := x1]>m1 = <[i := x2]>m2. + <[i := x]>m1 = <[i := y]>m2. Proof. intros Heq Hdel. apply map_Forall2_eq_L. @@ -367,8 +392,8 @@ Proof. Qed. Lemma map_insert_rev_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} - (i : K) (x1 x2 : A) (m1 m2 : M A) : - <[i := x1]>m1 = <[i := x2]>m2 → x1 = x2 ∧ delete i m1 = delete i m2. + (m1 m2 : M A) (i : K) (x y : A) : + <[i := x]>m1 = <[i := y]>m2 → x = y ∧ delete i m1 = delete i m2. Proof. intros Heq. apply map_Forall2_eq_L in Heq. apply map_Forall2_insert_inv in Heq as [Heq1 Heq2]. @@ -376,13 +401,13 @@ Proof. Qed. Lemma map_insert_rev_1_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} - (i : K) (x1 x2 : A) (m1 m2 : M A) : - <[i := x1]>m1 = <[i := x2]>m2 → x1 = x2. + (m1 m2 : M A) (i : K) (x y : A) : + <[i := x]>m1 = <[i := y]>m2 → x = y. Proof. apply map_insert_rev_L. Qed. Lemma map_insert_rev_2_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A} - (i : K) (x1 x2 : A) (m1 m2 : M A) : - <[i := x1]>m1 = <[i := x2]>m2 → delete i m1 = delete i m2. + (m1 m2 : M A) (i : K) (x y : A) : + <[i := x]>m1 = <[i := y]>m2 → delete i m1 = delete i m2. Proof. apply map_insert_rev_L. Qed. Lemma map_Forall2_alt_L `{FinMapDom K M D} `{!LeibnizEquiv D} {A B} diff --git a/matching.v b/matching.v index 494bb92..cb09690 100644 --- a/matching.v +++ b/matching.v @@ -64,32 +64,6 @@ Definition matches (m : matcher) (bs : gmap string expr) : snd <$> matches_aux ms bs end. -(* Copied from stdpp and changed so that the value types - of m1 and m2 are decoupled *) -Lemma dom_subseteq_size' `{FinMapDom K M D} {A B} (m1 : M A) (m2 : M B) : - dom m2 ⊆ dom m1 → size m2 ≤ size m1. -Proof. - revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom. - { rewrite map_size_empty. lia. } - rewrite dom_insert in Hdom. - assert (i ∉ dom m2) by (by apply not_elem_of_dom). - assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver. - rewrite <-(insert_delete m1 i x') by done. - rewrite !map_size_insert_None, <-Nat.succ_le_mono - by (by rewrite ?lookup_delete). - apply IH. rewrite dom_delete. set_solver. -Qed. - -Lemma dom_empty_subset `{Countable K} `{FinMapDom K M D} {A B} (m : M A) : - dom m ⊆ dom (∅ : M B) → m = ∅. -Proof. - intros Hdom. - apply dom_subseteq_size' in Hdom. - rewrite map_size_empty in Hdom. - inv Hdom. - by apply map_size_empty_inv. -Qed. - Lemma matches_aux_empty bs : matches_aux ∅ bs = Some (bs, ∅). Proof. done. Qed. @@ -496,8 +470,7 @@ Proof. revert strict bs brs Hmatches. induction ms using map_ind; intros strict bs brs Hmatches. - destruct strict; simplify_option_eq. - + apply dom_empty_subset in H0. simplify_eq. - constructor. + + apply map_dom_empty_subset in H0. simplify_eq. constructor. + constructor. - destruct x. + 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 @@ +(** This files contains definitions for determinism, strong confluence, + * semi-confluence, the Church-Rosser property and proofs about relationships + * of these properties. We use definitions and proofs from 'Term Rewriting and + * All That' by Franz Baader and Tobias Nipkow (1998). *) From stdpp Require Import relations. Definition deterministic {A} (R : relation A) := ∀ x y1 y2, R x y1 → R x y2 → y1 = y2. -(* As in Baader and Nipkow (1998): *) -(* y is a normal form of x if x -->* y and y is in normal form. *) +(** Baader and Nipkow (1998), p. 9: + * y is a normal form of x if x -->* y and y is in normal form. *) Definition is_nf_of `(R : relation A) x y := (rtc R x y) ∧ nf R y. (** The reflexive closure. *) @@ -14,15 +18,15 @@ Inductive rc {A} (R : relation A) : relation A := Hint Constructors rc : core. -(* Baader and Nipkow, Definition 2.7.3. *) +(** Baader and Nipkow, Definition 2.7.3. *) Definition strongly_confluent {A} (R : relation A) := ∀ x y1 y2, R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rc R y2 z. -(* Baader and Nipkow, Definition 2.1.4. *) +(** Baader and Nipkow, Definition 2.1.4. *) Definition semi_confluent {A} (R : relation A) := ∀ x y1 y2, R x y1 → rtc R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z. -(* Lemma 2.7.4 from Baader and Nipkow *) +(** Lemma 2.7.4 from Baader and Nipkow *) Lemma strong__semi_confluence {A} (R : relation A) : strongly_confluent R → semi_confluent R. Proof. @@ -47,11 +51,12 @@ Proof. by apply rtc_transitive with (y := y2). Qed. -(* Copied from stdpp, originates from Baader and Nipkow (1998) *) +(** Baader and Nipkow, Definition 2.1.3. + * Copied from stdpp v1.10.0 (confluent_alt). *) Definition cr {A} (R : relation A) := ∀ x y, rtsc R x y → ∃ z, rtc R x z ∧ rtc R y z. -(* Part of Lemma 2.1.5 from Baader and Nipkow (1998) *) +(** Part of Lemma 2.1.5 from Baader and Nipkow (1998) *) Lemma semi_confluence__cr {A} (R : relation A) : semi_confluent R → cr R. Proof. diff --git a/semprop.v b/semprop.v index 3af718d..2fe30af 100644 --- a/semprop.v +++ b/semprop.v @@ -77,173 +77,36 @@ Proof. intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2. - (* L: id, R: id *) left. by eapply base_step_deterministic. - (* L: id, R: ∘ *) simplify_eq/=. - inv H. - + inv Hbase1. - * inv H0. - -- inv Hbase2. - -- inv H. - * inv H0. - -- inv Hbase2. - -- inv H1. inv H. - + inv Hbase1. - * inv H0. - -- inv Hbase2. - -- inv H. - * inv H0. - -- inv Hbase2. - -- inv H. - + inv Hbase1. - * inv H0. - -- inv Hbase2. - -- inv H. - * inv H0. - -- inv Hbase2. - -- inv H1. - + inv Hbase1. - * inv H0. - -- inv Hbase2. - -- inv H. - * inv H0. - -- inv Hbase2. - -- inv H1. - * inv H0. - -- inv Hbase2. - -- inv H1. inv H. - + inv Hbase1. - inv H0. - * inv Hbase2. - * inv H. - + inv Hbase1. - * inv H0. - -- inv Hbase2. - -- inv H. - * inv H0. - -- inv Hbase2. - -- inv H. - + inv Hbase1. - inv H0. - * inv Hbase2. - * inv H. - + inv Hbase1. - inv H0. - * inv Hbase2. - * inv H. - + inv Hbase1. - inv H0. - * inv Hbase2. - * inv H. - + inv Hbase1. - * inv H0. - -- inv Hbase2. - -- inv H1. - * inv H0. - -- inv Hbase2. - -- inv H1. - * inv H0. - -- inv Hbase2. - -- inv H1. - + inv Hbase1. - inv H0. - * inv Hbase2. - * inv H. - simplify_option_eq. - destruct sv; try discriminate. - exfalso. clear uf. simplify_option_eq. - apply fmap_insert_lookup in H1. simplify_option_eq. - revert bs0 x H H1 Heqo. - induction H2; intros bs0 x H' H1 Heqo. - -- inv Hbase2. - -- simplify_option_eq. - inv H. destruct H'; try discriminate. - inv H1. apply fmap_insert_lookup in H0. simplify_option_eq. - by eapply IHis_ctx. - + inv Hbase1. - - (* L: ∘, R: id *) - simplify_eq/=. - inv H. - + inv Hbase2. - * inv Hctx1. - -- inv Hbase1. - -- inv H. - * inv Hctx1. - -- inv Hbase1. - -- inv H0. inv H. - + inv Hbase2. - * inv Hctx1. - -- inv Hbase1. - -- inv H. - * inv Hctx1. - -- inv Hbase1. - -- inv H. - + inv Hbase2. - * inv Hctx1. - -- inv Hbase1. - -- inv H. - * inv Hctx1. - -- inv Hbase1. - -- inv H0. - + inv Hbase2. - * inv Hctx1. - -- inv Hbase1. - -- inv H. - * inv Hctx1. - -- inv Hbase1. - -- inv H0. - * inv Hctx1. - -- inv Hbase1. - -- inv H0. inv H. - + inv Hbase2. - inv Hctx1. - * inv Hbase1. - * inv H. - + inv Hbase2. - * inv Hctx1. - -- inv Hbase1. - -- inv H. - * inv Hctx1. - -- inv Hbase1. - -- inv H. - + inv Hbase2. - inv Hctx1. - * inv Hbase1. - * inv H. - + inv Hbase2. - inv Hctx1. - * inv Hbase1. - * inv H. - + inv Hbase2. - inv Hctx1. - * inv Hbase1. - * inv H. - + inv Hbase2. - * inv Hctx1. - -- inv Hbase1. - -- inv H0. - * inv Hctx1. - -- inv Hbase1. - -- inv H0. - * inv Hctx1. - -- inv Hbase1. - -- inv H0. - + inv Hbase2. - inv Hctx1. - * inv Hbase1. - * clear IHHctx1. - inv H. - simplify_option_eq. - destruct sv; try discriminate. - exfalso. simplify_option_eq. - apply fmap_insert_lookup in H0. simplify_option_eq. - revert bs0 x H H0 Heqo. - induction H1; intros bs0 x H' H0 Heqo. - -- inv Hbase1. - -- simplify_option_eq. - inv H. destruct H'; try discriminate. - inv H0. apply fmap_insert_lookup in H2. simplify_option_eq. - eapply IHis_ctx. - ++ apply H2. - ++ apply Heqo0. - + inv Hbase2. + inv H; try inv select (_ -->base b12); + (inv select (is_ctx _ _ _); + [inv select (b21 -->base b22) + |inv select (is_ctx_item _ _ _)]). + simplify_option_eq. + destruct sv; try discriminate. + exfalso. clear uf. simplify_option_eq. + apply fmap_insert_lookup in H1. simplify_option_eq. + revert bs0 x H H1 Heqo. + induction H2; intros bs0 x H' H1 Heqo; [inv Hbase2|]. + simplify_option_eq. + inv H. destruct H'; try discriminate. + inv H1. apply fmap_insert_lookup in H0. simplify_option_eq. + by eapply IHis_ctx. + - (* L: ∘, R: id *) simplify_eq/=. + inv H; try inv select (_ -->base b22); + (inv select (is_ctx _ _ _); + [inv select (b11 -->base b12) + |inv select (is_ctx_item _ _ _)]). + clear IHHctx1. + simplify_option_eq. + destruct sv; try discriminate. + exfalso. simplify_option_eq. + apply fmap_insert_lookup in H0. simplify_option_eq. + revert bs0 x H H0 Heqo. + induction H1; intros bs0 x H' H0 Heqo; [inv Hbase1|]. + simplify_option_eq. + inv H. destruct H'; try discriminate. + inv H0. apply fmap_insert_lookup in H2. simplify_option_eq. + by eapply IHis_ctx. - (* L: ∘, R: ∘ *) simplify_option_eq. inv H; inv H0. diff --git a/shared.v b/shared.v index 8e9484f..2365c9d 100644 --- a/shared.v +++ b/shared.v @@ -14,12 +14,11 @@ Definition nonrecs : gmap string b_rhs → gmap string expr := Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs. Proof. - induction bs using map_ind. - - done. - - unfold nonrecs. - rewrite fmap_insert. - rewrite omap_insert_Some with (y := x); try done. - by f_equal. + induction bs using map_ind; [done|]. + unfold nonrecs. + rewrite fmap_insert. + rewrite omap_insert_Some with (y := x); try done. + by f_equal. Qed. Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs. diff --git a/sound.v b/sound.v index 761d7ad..2ae5001 100644 --- a/sound.v +++ b/sound.v @@ -13,9 +13,8 @@ Lemma strong_value_stuck_rtc sv e: expr_from_strong_value sv -->* e → e = expr_from_strong_value sv. Proof. - intros. inv H. - - reflexivity. - - exfalso. apply strong_value_stuck with (sv := sv). by exists y. + intros. inv H; [done|]. + exfalso. apply strong_value_stuck with (sv := sv). by exists y. Qed. 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 : Proof. intros [n Hsteps] % rtc_nsteps. revert sws es k e Hsteps. - induction n; intros sws es k e Hsteps. - - inv Hsteps. - - inv Hsteps. - inv H0. - inv H2. - + inv H3. inv H1. - * simplify_option_eq. unfold expr_from_strong_value, compose. - by rewrite H4. - * edestruct strong_value_stuck. exists y. done. - + inv H0. simplify_option_eq. - apply rtc_transitive - with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪ - (expr_from_strong_value <$> sws))))). - * do 2 rewrite <-insert_union_l. - apply rtc_once. - eapply E_Ctx - with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪ - (expr_from_strong_value <$> sws)))))). - -- eapply IsCtx_Compose. + induction n; intros sws es k e Hsteps; [inv Hsteps|]. + inv Hsteps. + inv H0. + inv H2. + - inv H3. inv H1. + + simplify_option_eq. unfold expr_from_strong_value, compose. + by rewrite H4. + + edestruct strong_value_stuck. exists y. done. + - inv H0. simplify_option_eq. + apply rtc_transitive + with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪ + (expr_from_strong_value <$> sws))))). + + do 2 rewrite <-insert_union_l. + apply rtc_once. + eapply E_Ctx + with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪ + (expr_from_strong_value <$> sws)))))). + * eapply IsCtx_Compose. + -- constructor. + -- eapply IsCtx_Compose + with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪ + (expr_from_strong_value <$> sws)))))). ++ constructor. - ++ eapply IsCtx_Compose - with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪ - (expr_from_strong_value <$> sws)))))). - ** constructor. - ** done. - -- done. - * by apply IHn. + ++ done. + * done. + + by apply IHn. Qed. Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x -- cgit v1.2.3