11 files changed, 221 insertions, 287 deletions

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