From ebef160fc470b38bd04420ea54a7169cbc1750bc Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 15 Jul 2025 05:29:49 -0400
Subject: [PATCH 01/21] confluence

---
 .../Untyped/LocallyNameless/Basic.lean        |   3 +
 .../LocallyNameless/BetaReduction.lean        | 126 +++++++++
 .../LocallyNameless/ConfluenceBeta.lean       | 245 ++++++++++++++++++
 Cslib/Utils/Relation.lean                     |  47 ++++
 4 files changed, 421 insertions(+)
 create mode 100644 Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean
 create mode 100644 Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
 create mode 100644 Cslib/Utils/Relation.lean

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
index 7b3038e2..8457db72 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
@@ -82,6 +82,9 @@ def Term.subst (m : Term Var) (x : Var) (sub : Term Var) : Term Var :=
 instance instHasSubstitutionTerm : HasSubstitution (Term Var) Var where
   subst := Term.subst
 
+omit [HasFresh Var] in
+lemma Term.subst_def (m : Term Var) (x : Var) (n : Term Var) : m.subst x n = m[x := n] := by rfl
+
 /-- Free variables of a term. -/
 @[simp]
 def Term.fv : Term Var → Finset Var
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean
new file mode 100644
index 00000000..550a7549
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean
@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Henson
+-/
+
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
+
+/-! # β-reduction for the λ-calculus
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*] [Chargueraud2012]
+* See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which
+  this is partially adapted
+
+-/
+
+universe u
+
+variable {Var : Type u} 
+
+namespace LambdaCalculus.LocallyNameless.Term
+
+/-- A single β-reduction step. -/
+inductive Step : Term Var → Term Var → Prop
+/-- Reduce an application to a lambda term. -/
+| β : LC (abs M)→ LC N → Step (app (abs M) N) (M ^ N)
+/-- Left congruence rule for application. -/
+| ξₗ: LC Z → Step M N → Step (app Z M) (app Z N)
+/-- Right congruence rule for application. -/
+| ξᵣ : LC Z → Step M N → Step (app M Z) (app N Z)
+/-- Congruence rule for lambda terms. -/
+| ξ (xs : Finset Var) : (∀ x ∉ xs, Step (M ^ fvar x) (N ^ fvar x)) → Step (abs M) (abs N) 
+
+/-- Notation for a single reduction step. -/
+notation:39 t " ⇢β " t' => Step t t'
+
+/-- Notation for multiple reduction steps (the reflexive transitive closure). -/
+notation:39 t " ↠β " t' => Relation.ReflTransGen Step t t'
+
+open Step
+
+variable {M M' N N' : Term Var}
+
+/-- The left side of a reduction is locally closed. -/
+lemma step_lc_l (step : M ⇢β M') : LC M := by
+  induction step <;> constructor
+  all_goals assumption
+
+/-- Left congruence rule for application in multiple reduction.-/
+theorem redex_app_l_cong : (M ↠β M') → LC N → (app M N ↠β app M' N) := by
+  intros redex lc_N 
+  induction' redex
+  case refl => rfl
+  case tail ih r => exact Relation.ReflTransGen.tail r (ξᵣ lc_N ih)
+
+/-- Right congruence rule for application in multiple reduction.-/
+theorem redex_app_r_cong : (M ↠β M') → LC N → (app N M ↠β app N M') := by
+  intros redex lc_N 
+  induction' redex
+  case refl => rfl
+  case tail ih r => exact Relation.ReflTransGen.tail r (ξₗ lc_N ih)
+
+variable [HasFresh Var] [DecidableEq Var]
+
+/-- The right side of a reduction is locally closed. -/
+lemma step_lc_r (step : M ⇢β M') : LC M' := by
+  induction step
+  case β => apply beta_lc <;> assumption
+  all_goals try constructor <;> assumption 
+
+/-- Substitution respects a single reduction step. -/
+lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⇢β s') -> (s [ x := fvar y ]) ⇢β (s' [ x := fvar y ]) := by
+  intros step
+  induction step
+  case ξₗ ih => exact ξₗ (subst_lc (by assumption) (by constructor)) ih 
+  case ξᵣ ih => exact ξᵣ (subst_lc (by assumption) (by constructor)) ih  
+  case β m n abs_lc n_lc => 
+    cases abs_lc with | abs xs _ mem =>
+      simp only [open']
+      rw [subst_open x (fvar y) 0 n m (by constructor)]
+      refine β ?_ (subst_lc n_lc (by constructor))
+      exact subst_lc (LC.abs xs m mem) (LC.fvar y)
+  case ξ m' m xs mem ih => 
+    apply ξ ({x} ∪ xs)
+    intros z z_mem
+    simp only [open']
+    rw [
+      subst_def, subst_def,
+      ←subst_fresh x (fvar z) (fvar y), ←subst_open x (fvar y) 0 (fvar z) m (by constructor),
+      subst_fresh x (fvar z) (fvar y), ←subst_fresh x (fvar z) (fvar y),
+      ←subst_open x (fvar y) 0 (fvar z) m' (by constructor), subst_fresh x (fvar z) (fvar y)
+    ]
+    apply ih
+    all_goals aesop
+
+/-- Abstracting then closing preserves a single reduction. -/
+lemma step_abs_close {x : Var} : (M ⇢β M') → (abs (M⟦0 ↜ x⟧) ⇢β abs (M'⟦0 ↜ x⟧)) := by
+  intros step
+  apply ξ ∅
+  intros y _
+  simp only [open']
+  repeat rw [open_close_to_subst]
+  exact redex_subst_cong M M' x y step
+  exact step_lc_r step
+  exact step_lc_l step
+
+/-- Abstracting then closing preserves multiple reductions. -/
+lemma redex_abs_close {x : Var} : (M ↠β M') → (abs (M⟦0 ↜ x⟧) ↠β abs (M'⟦0 ↜ x⟧)) :=  by
+  intros step
+  induction step using Relation.ReflTransGen.trans_induction_on
+  case ih₁ => rfl
+  case ih₂ ih => exact Relation.ReflTransGen.single (step_abs_close ih)
+  case ih₃ l r => trans; exact l; exact r
+
+/-- Multiple reduction of opening implies multiple reduction of abstraction. -/
+theorem redex_abs_cong (xs : Finset Var) : (∀ x ∉ xs, (M ^ fvar x) ↠β (M' ^ fvar x)) → abs M ↠β abs M' := by
+  intros mem
+  have ⟨fresh, union⟩ := fresh_exists (xs ∪ M.fv ∪ M'.fv)
+  simp only [Finset.union_assoc, Finset.mem_union, not_or] at union
+  obtain ⟨_, _, _⟩ := union
+  rw [←open_close fresh M 0 ?_, ←open_close fresh M' 0 ?_]
+  refine redex_abs_close (mem fresh ?_)
+  all_goals assumption
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
new file mode 100644
index 00000000..e549c43e
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -0,0 +1,245 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Henson
+-/
+
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.BetaReduction
+import Cslib.Utils.Relation
+
+/-! # β-confluence for the λ-calculus -/
+
+universe u
+
+variable {Var : Type u} 
+
+namespace LambdaCalculus.LocallyNameless.Term
+
+/-- A parallel β-reduction step. -/
+@[aesop safe [constructors]]
+inductive Parallel : Term Var → Term Var → Prop
+/-- Free variables parallel step to themselves. -/
+| fvar (x : Var) : Parallel (fvar x) (fvar x)
+/-- A parallel left and right congruence rule for application. -/
+| app : Parallel L L' → Parallel M M' → Parallel (app L M) (app L' M')
+/-- Congruence rule for lambda terms. -/
+| abs (xs : Finset Var) : (∀ x ∉ xs, Parallel (m ^ fvar x) (m' ^ fvar x)) → Parallel (abs m) (abs m')
+/-- A parallel β-reduction. -/
+| beta (xs : Finset Var) : 
+    (∀ x ∉ xs, Parallel (m ^ fvar x) (m' ^ fvar x) ) →
+    Parallel n n' → 
+    Parallel (app (abs m) n) (m' ^ n')
+
+notation:39 t " ⇉ "  t' =>                       Parallel t t'
+notation:39 t " ⇉* " t' => Relation.ReflTransGen Parallel t t'
+
+variable {M M' N N' : Term Var}
+
+/-- The left side of a parallel reduction is locally closed. -/
+lemma para_lc_l (step : M ⇉ N) : LC M  := by
+  induction step
+  case abs _ _ xs _ ih => exact LC.abs xs _ ih
+  case beta => refine LC.app (LC.abs ?_ _ ?_) ?_ <;> assumption
+  all_goals constructor <;> assumption
+
+variable [HasFresh Var] [DecidableEq Var]
+
+/-- The right side of a parallel reduction is locally closed. -/
+lemma para_lc_r (step : M ⇉ N) : LC N := by
+  induction step
+  case abs _ _ xs _ ih => exact LC.abs xs _ ih
+  case beta => refine beta_lc (LC.abs ?_ _ ?_) ?_ <;> assumption
+  all_goals constructor <;> assumption
+
+/-- Parallel reduction is reflexive for locally closed terms. -/
+@[aesop safe]
+def Parallel.lc_refl (M : Term Var) : LC M → M ⇉ M := by
+  intros lc
+  induction lc
+  all_goals constructor <;> assumption
+
+omit [HasFresh Var] [DecidableEq Var] in
+/-- A single β-reduction implies a single parallel reduction. -/
+lemma step_to_para (step : M ⇢β N) : (M ⇉ N) := by
+  induction step
+  case β _ abs_lc _ => cases abs_lc with | abs xs _ => apply Parallel.beta xs <;> aesop
+  all_goals aesop (config := {enableSimp := false})
+
+/-- A single parallel reduction implies a multiple β-reduction. -/
+lemma para_to_redex (para : M ⇉ N) : (M ↠β N) := by
+  induction para
+  case app _ _ _ _ l_para m_para redex_l redex_m =>
+    trans
+    exact redex_app_l_cong redex_l (para_lc_l m_para)
+    exact redex_app_r_cong redex_m (para_lc_r l_para)
+  case abs t t' xs _ ih =>
+    apply redex_abs_cong xs
+    intros x mem
+    exact ih x mem
+  case beta m m' n n' xs para_ih para_n redex_ih redex_n =>
+    have m'_abs_lc : LC m'.abs := by
+      apply LC.abs xs
+      intros _ mem
+      exact para_lc_r (para_ih _ mem)
+    calc
+      m.abs.app n ↠β m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
+      _           ↠β m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
+      _           ↠β m' ^ n'       := Relation.ReflTransGen.single (Step.β m'_abs_lc (para_lc_r para_n))
+  case fvar => constructor
+
+/-- Multiple parallel reduction is equivalent to multiple β-reduction. -/
+theorem parachain_iff_redex : (M ⇉* N) ↔ (M ↠β N) := by
+  refine Iff.intro ?chain_to_redex ?redex_to_chain <;> intros h <;> induction' h <;> try rfl
+  case redex_to_chain.tail redex chain => exact Relation.ReflTransGen.tail chain (step_to_para redex)
+  case chain_to_redex.tail para  redex => exact Relation.ReflTransGen.trans redex (para_to_redex para)
+
+/-- Parallel reduction respects substitution. -/
+lemma para_subst (x : Var) : (M ⇉ M') → (N ⇉ N') → (M[x := N] ⇉ M'[x := N']) := by
+  intros pm pn
+  induction pm <;> simp
+  case fvar x' =>
+    split
+    assumption
+    constructor
+  case beta _ _ _ _ xs _ _ ih _ => 
+    repeat rw [subst_def]
+    rw [subst_open _ _ _ _ _ (para_lc_r pn)]
+    apply Parallel.beta (xs ∪ {x})
+    intros y ymem
+    simp only [Finset.mem_union, Finset.mem_singleton, not_or] at ymem
+    push_neg at ymem
+    rw [subst_open_var _ _ _ _ _ (para_lc_r pn), subst_open_var _ _ _ _ _ (para_lc_l pn)]
+    apply ih
+    all_goals aesop
+  case app => constructor <;> assumption
+  case abs u u' xs mem ih => 
+    apply Parallel.abs (xs ∪ {x})
+    intros y ymem
+    simp only [Finset.mem_union, Finset.mem_singleton, not_or] at ymem
+    repeat rw [subst_def]
+    rw [subst_open_var _ _ _ _ ?_ (para_lc_l pn), subst_open_var _ _ _ _ ?_ (para_lc_r pn)]
+    push_neg at ymem
+    apply ih
+    all_goals aesop
+
+/-- Parallel substitution respects closing and opening. -/
+lemma para_open_close (x y z) : 
+  (M ⇉ M') → 
+  y ∉ (M.fv ∪ M'.fv ∪ {x}) → 
+  M⟦z ↜ x⟧⟦z ↝ fvar y⟧ ⇉ M'⟦z ↜ x⟧⟦z ↝ fvar y⟧ 
+  := by
+  intros para vars
+  simp only [Finset.union_assoc, Finset.mem_union, Finset.mem_singleton, not_or] at vars
+  rw [open_close_to_subst, open_close_to_subst] 
+  apply para_subst
+  exact para
+  constructor
+  exact para_lc_r para
+  exact para_lc_l para
+
+/-- Parallel substitution respects fresh opening. -/
+lemma para_open_out (L : Finset Var) :
+    (∀ x, x ∉ L → (M ^ fvar x) ⇉ (N ^ fvar x))
+    → (M' ⇉ N') → (M ^ M') ⇉ (N ^ N') := by
+    intros mem para
+    let ⟨x, qx⟩ := fresh_exists (L ∪ N.fv ∪ M.fv)
+    simp at qx
+    obtain ⟨q1, q2, q3⟩ := qx
+    rw [subst_intro x M' _ q3 (para_lc_l para), subst_intro x N' _ q2 (para_lc_r para)]
+    exact para_subst x (mem x q1) para
+
+/-- Parallel reduction has the diamond property. -/
+theorem para_diamond : Diamond (@Parallel Var) := by
+  simp [Diamond]
+  intros t t1 t2 tpt1
+  revert t2
+  induction tpt1 <;> intros t2 tpt2
+  case fvar x =>
+    exists t2
+    and_intros
+    · assumption
+    · apply Parallel.lc_refl
+      exact para_lc_r tpt2
+  case abs s1 s2' xs mem ih => 
+    cases tpt2
+    case abs t2' xs' mem' =>
+      have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ t2'.fv ∪ s2'.fv)
+      simp at qx
+      have ⟨q1, q2, q3, q4⟩ := qx
+      have ⟨t', qt'_l, qt'_r⟩ := ih x q1 (mem' _ q2)
+      exists abs (t' ^* x)
+      constructor
+      · apply Parallel.abs ((s2' ^ fvar x).fv ∪ t'.fv ∪ {x})
+        intros y qy
+        simp
+        rw [←open_close x s2' 0 q4]
+        exact para_open_close x y 0 qt'_l qy
+      · apply Parallel.abs ((t2' ^ fvar x).fv ∪ t'.fv ∪ {x})
+        intros y qy
+        simp
+        rw [←open_close x t2' 0 q3]
+        exact para_open_close x y 0 qt'_r qy 
+  case beta s1 s1' s2 s2' xs mem ps ih1 ih2 => 
+    cases tpt2
+    case app u2 u2' s1pu2 s2pu2' => 
+      cases s1pu2
+      case abs s1'' xs' mem' =>
+        have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ s1''.fv ∪ s1'.fv)
+        simp at qx
+        obtain ⟨q1, q2, q3, q4⟩ := qx
+        have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2'
+        have ⟨t'', qt''_l, qt''_r⟩ := @ih1 x q1 _ (mem' _ q2)
+        exists (t'' ^* x) ^ t'
+        constructor
+        · rw [subst_intro x s2' _ q4 (para_lc_l qt'_l), subst_intro x t' _ (close_var_not_fvar x t'') (para_lc_r qt'_l)]
+          simp
+          rw [close_open _ _ _ (para_lc_r qt''_l)]
+          exact para_subst x qt''_l qt'_l
+        · apply Parallel.beta ((s1'' ^ fvar x).fv ∪ t''.fv ∪ {x})
+          intros y qy
+          rw [←open_close x s1'' 0]
+          apply para_open_close
+          all_goals aesop
+    case beta u1' u2' xs' mem' s2pu2' => 
+      have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ u1'.fv ∪ s1'.fv ∪ s2'.fv ∪ u2'.fv)
+      simp at qx
+      have ⟨q1, q2, q3, q4, q5, q6⟩ := qx
+      have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2'
+      have ⟨t'', qt''_l, qt''_r⟩ := @ih1 x q1 _ (mem' _ q2)
+      rw [subst_intro x u2' u1' _ (para_lc_l qt'_r), subst_intro x s2' s1' _ (para_lc_l qt'_l)]
+      exists t'' [x := t']
+      exact ⟨para_subst x qt''_l qt'_l, para_subst x qt''_r qt'_r⟩
+      all_goals aesop
+  case app s1 s1' s2 s2' s1ps1' _ ih1 ih2  =>
+    cases tpt2
+    case app u1 u2' s1 s2 =>
+      have ⟨l, _, _⟩ := ih1 s1
+      have ⟨r, _, _⟩ := ih2 s2
+      exists app l r
+      and_intros <;> constructor <;> assumption
+    case beta t1' u1' u2' xs mem s2pu2' => 
+      cases s1ps1'
+      case abs s1'' xs' mem' =>
+        have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ s1''.fv ∪ u1'.fv)
+        simp at qx
+        obtain ⟨q1, q2, q3, q4⟩ := qx
+        have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2'
+        have ⟨t'', qt''_l, qt''_r⟩ := @ih1 (abs u1') (Parallel.abs xs mem)
+        cases qt''_l
+        next w1 xs'' mem'' =>
+        cases qt''_r
+        case abs xs''' mem''' =>
+          exists w1 ^ t'
+          constructor
+          · apply Parallel.beta xs''
+            exact fun x a ↦ mem'' x a
+            exact qt'_l
+          · exact para_open_out xs''' mem''' qt'_r
+
+/-- Parallel reduction is confluent. -/
+theorem para_confluence : Confluence (@Parallel Var) := Relation.ReflTransGen.diamond para_diamond
+
+/-- β-reduction is confluent. -/
+theorem confluence_beta : Confluence (@Step Var) := diamond_bisim parachain_iff_redex (@para_confluence Var _ _)
diff --git a/Cslib/Utils/Relation.lean b/Cslib/Utils/Relation.lean
new file mode 100644
index 00000000..01f74fc6
--- /dev/null
+++ b/Cslib/Utils/Relation.lean
@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2025 Thomas Waring. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Waring, Chris Henson
+-/
+import Mathlib.Logic.Relation
+
+universe u
+
+variable {α : Type u} {R R' : α → α → Prop}
+
+/-- A relation has the diamond property when all reductions with a common origin are joinable -/
+abbrev Diamond (R : α → α → Prop) := ∀ {A B C : α}, R A B → R A C → (∃ D, R B D ∧ R C D)
+
+/-- A relation is confluent when its reflexive transitive closure has the diamond property. -/
+abbrev Confluence (R : α → α → Prop) := Diamond (Relation.ReflTransGen R)
+
+/-- Extending a multistep reduction by a single step preserves multi-joinability. -/
+lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) : 
+  Relation.ReflTransGen R A B → 
+  R A C → 
+  ∃ D, Relation.ReflTransGen R B D ∧ Relation.ReflTransGen R C D := by
+  intros AB _
+  revert C
+  induction AB using Relation.ReflTransGen.head_induction_on <;> intros C AC
+  case refl => exact ⟨C, ⟨single AC, by rfl⟩⟩
+  case head A'_C' _ ih =>
+    obtain ⟨D, ⟨CD, C'_D⟩⟩ := h AC A'_C'
+    obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D
+    exact ⟨D', ⟨B_D', head CD D_D'⟩⟩
+
+/-- The dismond property implies confluence. -/
+theorem Relation.ReflTransGen.diamond (h : Diamond R) : Confluence R := by
+  intros A B C AB BC
+  revert C
+  induction AB using Relation.ReflTransGen.head_induction_on <;> intros C BC
+  case refl => exists C
+  case head _ _ A'_C' _ ih =>
+    obtain ⟨D, ⟨CD, C'_D⟩⟩ := diamond_extend h BC A'_C'
+    obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D
+    exact ⟨D', ⟨B_D', trans CD D_D'⟩⟩
+
+/-- Equivalence of relations preserves the diamond property. -/
+theorem diamond_bisim (sim : ∀ {M N : α}, R M N ↔ R' M N) (h : Diamond R) : Diamond R' := by
+  intros L M₁ M₂ L_M₁ L_M₂
+  have ⟨N, ⟨M₁_chain_N, M₂_chain_N⟩⟩ := h (sim.mpr L_M₁) (sim.mpr L_M₂)
+  exact ⟨N, ⟨sim.mp M₁_chain_N, sim.mp M₂_chain_N⟩⟩

From b898302705426809e0d3c5c7ba94f9945912a455 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 15 Jul 2025 06:00:32 -0400
Subject: [PATCH 02/21] non-terminal simps

---
 .../LocallyNameless/ConfluenceBeta.lean       | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index e549c43e..bad33525 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -98,7 +98,7 @@ theorem parachain_iff_redex : (M ⇉* N) ↔ (M ↠β N) := by
 /-- Parallel reduction respects substitution. -/
 lemma para_subst (x : Var) : (M ⇉ M') → (N ⇉ N') → (M[x := N] ⇉ M'[x := N']) := by
   intros pm pn
-  induction pm <;> simp
+  induction pm <;> simp only [instHasSubstitutionTerm, subst, open']
   case fvar x' =>
     split
     assumption
@@ -145,14 +145,13 @@ lemma para_open_out (L : Finset Var) :
     → (M' ⇉ N') → (M ^ M') ⇉ (N ^ N') := by
     intros mem para
     let ⟨x, qx⟩ := fresh_exists (L ∪ N.fv ∪ M.fv)
-    simp at qx
+    simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx
     obtain ⟨q1, q2, q3⟩ := qx
     rw [subst_intro x M' _ q3 (para_lc_l para), subst_intro x N' _ q2 (para_lc_r para)]
     exact para_subst x (mem x q1) para
 
 /-- Parallel reduction has the diamond property. -/
 theorem para_diamond : Diamond (@Parallel Var) := by
-  simp [Diamond]
   intros t t1 t2 tpt1
   revert t2
   induction tpt1 <;> intros t2 tpt2
@@ -166,19 +165,19 @@ theorem para_diamond : Diamond (@Parallel Var) := by
     cases tpt2
     case abs t2' xs' mem' =>
       have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ t2'.fv ∪ s2'.fv)
-      simp at qx
+      simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx
       have ⟨q1, q2, q3, q4⟩ := qx
       have ⟨t', qt'_l, qt'_r⟩ := ih x q1 (mem' _ q2)
       exists abs (t' ^* x)
       constructor
       · apply Parallel.abs ((s2' ^ fvar x).fv ∪ t'.fv ∪ {x})
         intros y qy
-        simp
+        simp only [open', close]
         rw [←open_close x s2' 0 q4]
         exact para_open_close x y 0 qt'_l qy
       · apply Parallel.abs ((t2' ^ fvar x).fv ∪ t'.fv ∪ {x})
         intros y qy
-        simp
+        simp only [open', close]
         rw [←open_close x t2' 0 q3]
         exact para_open_close x y 0 qt'_r qy 
   case beta s1 s1' s2 s2' xs mem ps ih1 ih2 => 
@@ -187,14 +186,14 @@ theorem para_diamond : Diamond (@Parallel Var) := by
       cases s1pu2
       case abs s1'' xs' mem' =>
         have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ s1''.fv ∪ s1'.fv)
-        simp at qx
+        simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx
         obtain ⟨q1, q2, q3, q4⟩ := qx
         have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2'
         have ⟨t'', qt''_l, qt''_r⟩ := @ih1 x q1 _ (mem' _ q2)
         exists (t'' ^* x) ^ t'
         constructor
         · rw [subst_intro x s2' _ q4 (para_lc_l qt'_l), subst_intro x t' _ (close_var_not_fvar x t'') (para_lc_r qt'_l)]
-          simp
+          simp only [instHasSubstitutionTerm, open', close]
           rw [close_open _ _ _ (para_lc_r qt''_l)]
           exact para_subst x qt''_l qt'_l
         · apply Parallel.beta ((s1'' ^ fvar x).fv ∪ t''.fv ∪ {x})
@@ -204,7 +203,7 @@ theorem para_diamond : Diamond (@Parallel Var) := by
           all_goals aesop
     case beta u1' u2' xs' mem' s2pu2' => 
       have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ u1'.fv ∪ s1'.fv ∪ s2'.fv ∪ u2'.fv)
-      simp at qx
+      simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx
       have ⟨q1, q2, q3, q4, q5, q6⟩ := qx
       have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2'
       have ⟨t'', qt''_l, qt''_r⟩ := @ih1 x q1 _ (mem' _ q2)
@@ -223,7 +222,7 @@ theorem para_diamond : Diamond (@Parallel Var) := by
       cases s1ps1'
       case abs s1'' xs' mem' =>
         have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ s1''.fv ∪ u1'.fv)
-        simp at qx
+        simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx
         obtain ⟨q1, q2, q3, q4⟩ := qx
         have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2'
         have ⟨t'', qt''_l, qt''_r⟩ := @ih1 (abs u1') (Parallel.abs xs mem)

From 9a61813fc366bde7bdf6f35914ae7b9531ce9c08 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 16 Jul 2025 19:37:40 -0400
Subject: [PATCH 03/21] style

---
 .../Untyped/LocallyNameless/ConfluenceBeta.lean             | 6 ++++--
 Cslib/Utils/Relation.lean                                   | 2 +-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index bad33525..490af567 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -238,7 +238,9 @@ theorem para_diamond : Diamond (@Parallel Var) := by
           · exact para_open_out xs''' mem''' qt'_r
 
 /-- Parallel reduction is confluent. -/
-theorem para_confluence : Confluence (@Parallel Var) := Relation.ReflTransGen.diamond para_diamond
+theorem para_confluence : Confluence (@Parallel Var) := 
+  Relation.ReflTransGen.diamond_confluence para_diamond
 
 /-- β-reduction is confluent. -/
-theorem confluence_beta : Confluence (@Step Var) := diamond_bisim parachain_iff_redex (@para_confluence Var _ _)
+theorem confluence_beta : Confluence (@Step Var) := 
+  diamond_bisim parachain_iff_redex (@para_confluence Var _ _)
diff --git a/Cslib/Utils/Relation.lean b/Cslib/Utils/Relation.lean
index 11b2c0d5..d35bf3fa 100644
--- a/Cslib/Utils/Relation.lean
+++ b/Cslib/Utils/Relation.lean
@@ -30,7 +30,7 @@ lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) :
     exact ⟨D', ⟨B_D', head CD D_D'⟩⟩
 
 /-- The dismond property implies confluence. -/
-theorem Relation.ReflTransGen.diamond (h : Diamond R) : Confluence R := by
+theorem Relation.ReflTransGen.diamond_confluence (h : Diamond R) : Confluence R := by
   intros A B C AB BC
   revert C
   induction AB using Relation.ReflTransGen.head_induction_on <;> intros C BC

From 333a23687c4d4eee4de578678dc3f2857ae8243d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Thu, 17 Jul 2025 17:28:57 -0400
Subject: [PATCH 04/21] use reduction_sys

---
 .../LocallyNameless/BetaReduction.lean        | 22 +++----
 .../LocallyNameless/ConfluenceBeta.lean       | 61 ++++++++++++-------
 2 files changed, 49 insertions(+), 34 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean
index 550a7549..c6c61a61 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean
@@ -6,6 +6,7 @@ Authors: Chris Henson
 
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
+import Cslib.Semantics.ReductionSystem.Basic
 
 /-! # β-reduction for the λ-calculus
 
@@ -24,6 +25,7 @@ variable {Var : Type u}
 namespace LambdaCalculus.LocallyNameless.Term
 
 /-- A single β-reduction step. -/
+@[reduction_sys beta_rs "β"]
 inductive Step : Term Var → Term Var → Prop
 /-- Reduce an application to a lambda term. -/
 | β : LC (abs M)→ LC N → Step (app (abs M) N) (M ^ N)
@@ -34,18 +36,12 @@ inductive Step : Term Var → Term Var → Prop
 /-- Congruence rule for lambda terms. -/
 | ξ (xs : Finset Var) : (∀ x ∉ xs, Step (M ^ fvar x) (N ^ fvar x)) → Step (abs M) (abs N) 
 
-/-- Notation for a single reduction step. -/
-notation:39 t " ⇢β " t' => Step t t'
-
-/-- Notation for multiple reduction steps (the reflexive transitive closure). -/
-notation:39 t " ↠β " t' => Relation.ReflTransGen Step t t'
-
 open Step
 
 variable {M M' N N' : Term Var}
 
 /-- The left side of a reduction is locally closed. -/
-lemma step_lc_l (step : M ⇢β M') : LC M := by
+lemma step_lc_l (step : M ⭢β M') : LC M := by
   induction step <;> constructor
   all_goals assumption
 
@@ -66,22 +62,22 @@ theorem redex_app_r_cong : (M ↠β M') → LC N → (app N M ↠β app N M') :=
 variable [HasFresh Var] [DecidableEq Var]
 
 /-- The right side of a reduction is locally closed. -/
-lemma step_lc_r (step : M ⇢β M') : LC M' := by
+lemma step_lc_r (step : M ⭢β M') : LC M' := by
   induction step
-  case β => apply beta_lc <;> assumption
+  case «β» => apply beta_lc <;> assumption
   all_goals try constructor <;> assumption 
 
 /-- Substitution respects a single reduction step. -/
-lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⇢β s') -> (s [ x := fvar y ]) ⇢β (s' [ x := fvar y ]) := by
+lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢β s') -> (s [ x := fvar y ]) ⭢β (s' [ x := fvar y ]) := by
   intros step
   induction step
   case ξₗ ih => exact ξₗ (subst_lc (by assumption) (by constructor)) ih 
   case ξᵣ ih => exact ξᵣ (subst_lc (by assumption) (by constructor)) ih  
-  case β m n abs_lc n_lc => 
+  case «β» m n abs_lc n_lc => 
     cases abs_lc with | abs xs _ mem =>
       simp only [open']
       rw [subst_open x (fvar y) 0 n m (by constructor)]
-      refine β ?_ (subst_lc n_lc (by constructor))
+      refine «β» ?_ (subst_lc n_lc (by constructor))
       exact subst_lc (LC.abs xs m mem) (LC.fvar y)
   case ξ m' m xs mem ih => 
     apply ξ ({x} ∪ xs)
@@ -97,7 +93,7 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⇢β s') -> (s [ x :=
     all_goals aesop
 
 /-- Abstracting then closing preserves a single reduction. -/
-lemma step_abs_close {x : Var} : (M ⇢β M') → (abs (M⟦0 ↜ x⟧) ⇢β abs (M'⟦0 ↜ x⟧)) := by
+lemma step_abs_close {x : Var} : (M ⭢β M') → (abs (M⟦0 ↜ x⟧) ⭢β abs (M'⟦0 ↜ x⟧)) := by
   intros step
   apply ξ ∅
   intros y _
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index 490af567..82fd7113 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -18,7 +18,7 @@ variable {Var : Type u}
 namespace LambdaCalculus.LocallyNameless.Term
 
 /-- A parallel β-reduction step. -/
-@[aesop safe [constructors]]
+@[aesop safe [constructors], reduction_sys para_rs "ₚ"]
 inductive Parallel : Term Var → Term Var → Prop
 /-- Free variables parallel step to themselves. -/
 | fvar (x : Var) : Parallel (fvar x) (fvar x)
@@ -32,13 +32,14 @@ inductive Parallel : Term Var → Term Var → Prop
     Parallel n n' → 
     Parallel (app (abs m) n) (m' ^ n')
 
-notation:39 t " ⇉ "  t' =>                       Parallel t t'
-notation:39 t " ⇉* " t' => Relation.ReflTransGen Parallel t t'
+-- TODO: API for these???
+lemma para_rs_Red_eq {α}: (@para_rs α).Red = Parallel := by rfl
+lemma para_rs_MRed_eq {α}: (@para_rs α).MRed = Relation.ReflTransGen Parallel := by rfl
 
 variable {M M' N N' : Term Var}
 
 /-- The left side of a parallel reduction is locally closed. -/
-lemma para_lc_l (step : M ⇉ N) : LC M  := by
+lemma para_lc_l (step : M ⭢ₚ N) : LC M  := by
   induction step
   case abs _ _ xs _ ih => exact LC.abs xs _ ih
   case beta => refine LC.app (LC.abs ?_ _ ?_) ?_ <;> assumption
@@ -47,7 +48,7 @@ lemma para_lc_l (step : M ⇉ N) : LC M  := by
 variable [HasFresh Var] [DecidableEq Var]
 
 /-- The right side of a parallel reduction is locally closed. -/
-lemma para_lc_r (step : M ⇉ N) : LC N := by
+lemma para_lc_r (step : M ⭢ₚ N) : LC N := by
   induction step
   case abs _ _ xs _ ih => exact LC.abs xs _ ih
   case beta => refine beta_lc (LC.abs ?_ _ ?_) ?_ <;> assumption
@@ -55,21 +56,30 @@ lemma para_lc_r (step : M ⇉ N) : LC N := by
 
 /-- Parallel reduction is reflexive for locally closed terms. -/
 @[aesop safe]
-def Parallel.lc_refl (M : Term Var) : LC M → M ⇉ M := by
+def Parallel.lc_refl (M : Term Var) : LC M → M ⭢ₚ M := by
   intros lc
   induction lc
   all_goals constructor <;> assumption
 
+-- TODO: better ways to handle this?
+-- The problem is that sometimes when we apply a theorem we get out of our notation, so aesop can't
+-- see they are the same, including constructors.
+@[aesop safe]
+private def Parallel.lc_refl' (M : Term Var) : LC M → Parallel M M := by 
+  apply Parallel.lc_refl
+
 omit [HasFresh Var] [DecidableEq Var] in
 /-- A single β-reduction implies a single parallel reduction. -/
-lemma step_to_para (step : M ⇢β N) : (M ⇉ N) := by
-  induction step
-  case β _ abs_lc _ => cases abs_lc with | abs xs _ => apply Parallel.beta xs <;> aesop
+lemma step_to_para (step : M ⭢β N) : (M ⭢ₚ N) := by
+  induction step <;> simp [para_rs_Red_eq]
+  case «β» _ abs_lc _ => cases abs_lc with | abs xs _ => 
+    apply Parallel.beta xs <;> intros <;> apply Parallel.lc_refl <;> aesop
   all_goals aesop (config := {enableSimp := false})
 
 /-- A single parallel reduction implies a multiple β-reduction. -/
-lemma para_to_redex (para : M ⇉ N) : (M ↠β N) := by
+lemma para_to_redex (para : M ⭢ₚ N) : (M ↠β N) := by
   induction para
+  case fvar => constructor
   case app _ _ _ _ l_para m_para redex_l redex_m =>
     trans
     exact redex_app_l_cong redex_l (para_lc_l m_para)
@@ -83,20 +93,26 @@ lemma para_to_redex (para : M ⇉ N) : (M ↠β N) := by
       apply LC.abs xs
       intros _ mem
       exact para_lc_r (para_ih _ mem)
-    calc
-      m.abs.app n ↠β m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
-      _           ↠β m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
-      _           ↠β m' ^ n'       := Relation.ReflTransGen.single (Step.β m'_abs_lc (para_lc_r para_n))
-  case fvar => constructor
+    trans
+    exact redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
+    exact Relation.ReflTransGen.tail 
+      (redex_app_r_cong redex_n m'_abs_lc) 
+      (Step.β m'_abs_lc (para_lc_r para_n))
+    -- TODO: the `Trans` instances in Cslib/Semantics/ReductionSystem/Basic.lean cause problems here
+    -- it ends up trying to take the transitive closure of the transitve closure
+    --calc
+    --  m.abs.app n ↠β m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
+    --  _           ↠β m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
+    --  _           ↠β m' ^ n'       := Relation.ReflTransGen.single (Step.β m'_abs_lc (para_lc_r para_n))
 
 /-- Multiple parallel reduction is equivalent to multiple β-reduction. -/
-theorem parachain_iff_redex : (M ⇉* N) ↔ (M ↠β N) := by
+theorem parachain_iff_redex : (M ↠ₚ N) ↔ (M ↠β N) := by
   refine Iff.intro ?chain_to_redex ?redex_to_chain <;> intros h <;> induction' h <;> try rfl
   case redex_to_chain.tail redex chain => exact Relation.ReflTransGen.tail chain (step_to_para redex)
   case chain_to_redex.tail para  redex => exact Relation.ReflTransGen.trans redex (para_to_redex para)
 
 /-- Parallel reduction respects substitution. -/
-lemma para_subst (x : Var) : (M ⇉ M') → (N ⇉ N') → (M[x := N] ⇉ M'[x := N']) := by
+lemma para_subst (x : Var) : (M ⭢ₚ M') → (N ⭢ₚ N') → (M[x := N] ⭢ₚ M'[x := N']) := by
   intros pm pn
   induction pm <;> simp only [instHasSubstitutionTerm, subst, open']
   case fvar x' =>
@@ -126,9 +142,9 @@ lemma para_subst (x : Var) : (M ⇉ M') → (N ⇉ N') → (M[x := N] ⇉ M'[x :
 
 /-- Parallel substitution respects closing and opening. -/
 lemma para_open_close (x y z) : 
-  (M ⇉ M') → 
+  (M ⭢ₚ M') → 
   y ∉ (M.fv ∪ M'.fv ∪ {x}) → 
-  M⟦z ↜ x⟧⟦z ↝ fvar y⟧ ⇉ M'⟦z ↜ x⟧⟦z ↝ fvar y⟧ 
+  M⟦z ↜ x⟧⟦z ↝ fvar y⟧ ⭢ₚ M'⟦z ↜ x⟧⟦z ↝ fvar y⟧ 
   := by
   intros para vars
   simp only [Finset.union_assoc, Finset.mem_union, Finset.mem_singleton, not_or] at vars
@@ -141,8 +157,8 @@ lemma para_open_close (x y z) :
 
 /-- Parallel substitution respects fresh opening. -/
 lemma para_open_out (L : Finset Var) :
-    (∀ x, x ∉ L → (M ^ fvar x) ⇉ (N ^ fvar x))
-    → (M' ⇉ N') → (M ^ M') ⇉ (N ^ N') := by
+    (∀ x, x ∉ L → (M ^ fvar x) ⭢ₚ (N ^ fvar x))
+    → (M' ⭢ₚ N') → (M ^ M') ⭢ₚ (N ^ N') := by
     intros mem para
     let ⟨x, qx⟩ := fresh_exists (L ∪ N.fv ∪ M.fv)
     simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx
@@ -150,6 +166,9 @@ lemma para_open_out (L : Finset Var) :
     rw [subst_intro x M' _ q3 (para_lc_l para), subst_intro x N' _ q2 (para_lc_r para)]
     exact para_subst x (mem x q1) para
 
+-- TODO: the Takahashi translation would be a much nicer and shorter proof, but I had difficultly
+-- writing it for locally nameless terms.
+
 /-- Parallel reduction has the diamond property. -/
 theorem para_diamond : Diamond (@Parallel Var) := by
   intros t t1 t2 tpt1

From 425566242ee628e8e1b0e0401f78c9ab7516f9dc Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Thu, 17 Jul 2025 17:31:38 -0400
Subject: [PATCH 05/21] non-terminal simp

---
 .../LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index 82fd7113..1969baed 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -71,7 +71,7 @@ private def Parallel.lc_refl' (M : Term Var) : LC M → Parallel M M := by
 omit [HasFresh Var] [DecidableEq Var] in
 /-- A single β-reduction implies a single parallel reduction. -/
 lemma step_to_para (step : M ⭢β N) : (M ⭢ₚ N) := by
-  induction step <;> simp [para_rs_Red_eq]
+  induction step <;> simp only [para_rs_Red_eq]
   case «β» _ abs_lc _ => cases abs_lc with | abs xs _ => 
     apply Parallel.beta xs <;> intros <;> apply Parallel.lc_refl <;> aesop
   all_goals aesop (config := {enableSimp := false})

From b3e129623ec95d84f18da2a19a69e4bffc9cca83 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Thu, 17 Jul 2025 17:39:05 -0400
Subject: [PATCH 06/21] remove redundant lemma

---
 .../LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean   | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index 1969baed..b7f2e9d1 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -34,7 +34,6 @@ inductive Parallel : Term Var → Term Var → Prop
 
 -- TODO: API for these???
 lemma para_rs_Red_eq {α}: (@para_rs α).Red = Parallel := by rfl
-lemma para_rs_MRed_eq {α}: (@para_rs α).MRed = Relation.ReflTransGen Parallel := by rfl
 
 variable {M M' N N' : Term Var}
 

From 006c43b84dbfdf0695a7fea44a9904118e667643 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Thu, 17 Jul 2025 17:43:18 -0400
Subject: [PATCH 07/21] update TODO

---
 .../Untyped/LocallyNameless/ConfluenceBeta.lean               | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index b7f2e9d1..4dc10782 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -32,8 +32,8 @@ inductive Parallel : Term Var → Term Var → Prop
     Parallel n n' → 
     Parallel (app (abs m) n) (m' ^ n')
 
--- TODO: API for these???
-lemma para_rs_Red_eq {α}: (@para_rs α).Red = Parallel := by rfl
+-- TODO: I think this could be generated along with `para_rs`
+lemma para_rs_Red_eq {α} : (@para_rs α).Red = Parallel := by rfl
 
 variable {M M' N N' : Term Var}
 

From de6298ebd9b7d34310325c71fd6c5bacba15674e Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Thu, 17 Jul 2025 18:19:07 -0400
Subject: [PATCH 08/21] style

---
 .../LocallyNameless/ConfluenceBeta.lean       | 20 ++++++++-----------
 1 file changed, 8 insertions(+), 12 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index 4dc10782..5edc6816 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -187,17 +187,12 @@ theorem para_diamond : Diamond (@Parallel Var) := by
       have ⟨q1, q2, q3, q4⟩ := qx
       have ⟨t', qt'_l, qt'_r⟩ := ih x q1 (mem' _ q2)
       exists abs (t' ^* x)
-      constructor
-      · apply Parallel.abs ((s2' ^ fvar x).fv ∪ t'.fv ∪ {x})
-        intros y qy
-        simp only [open', close]
-        rw [←open_close x s2' 0 q4]
-        exact para_open_close x y 0 qt'_l qy
-      · apply Parallel.abs ((t2' ^ fvar x).fv ∪ t'.fv ∪ {x})
-        intros y qy
-        simp only [open', close]
-        rw [←open_close x t2' 0 q3]
-        exact para_open_close x y 0 qt'_r qy 
+      constructor 
+      <;> [let z := s2'; let z := t2']
+      <;> apply Parallel.abs ((z ^ fvar x).fv ∪ t'.fv ∪ {x})
+      <;> intros y qy <;> simp only [open', close]
+      <;> [rw [←open_close x _ 0 q4]; rw [←open_close x _ 0 q3]] 
+      <;> refine para_open_close x y 0 ?_ qy <;> [exact qt'_l; exact qt'_r]
   case beta s1 s1' s2 s2' xs mem ps ih1 ih2 => 
     cases tpt2
     case app u2 u2' s1pu2 s2pu2' => 
@@ -210,7 +205,8 @@ theorem para_diamond : Diamond (@Parallel Var) := by
         have ⟨t'', qt''_l, qt''_r⟩ := @ih1 x q1 _ (mem' _ q2)
         exists (t'' ^* x) ^ t'
         constructor
-        · rw [subst_intro x s2' _ q4 (para_lc_l qt'_l), subst_intro x t' _ (close_var_not_fvar x t'') (para_lc_r qt'_l)]
+        · rw [subst_intro x s2' _ q4 (para_lc_l qt'_l), 
+              subst_intro x t' _ (close_var_not_fvar x t'') (para_lc_r qt'_l)]
           simp only [instHasSubstitutionTerm, open', close]
           rw [close_open _ _ _ (para_lc_r qt''_l)]
           exact para_subst x qt''_l qt'_l

From b66806739f702d4e6cb28caf0d0913c29aff3399 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Thu, 17 Jul 2025 19:14:20 -0400
Subject: [PATCH 09/21] fix Trans instances

---
 .../Untyped/LocallyNameless/ConfluenceBeta.lean   | 15 ++++-----------
 Cslib/Semantics/ReductionSystem/Basic.lean        |  6 +-----
 CslibTests/ReductionSystem.lean                   |  2 +-
 3 files changed, 6 insertions(+), 17 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index 5edc6816..09e3509f 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -92,17 +92,10 @@ lemma para_to_redex (para : M ⭢ₚ N) : (M ↠β N) := by
       apply LC.abs xs
       intros _ mem
       exact para_lc_r (para_ih _ mem)
-    trans
-    exact redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
-    exact Relation.ReflTransGen.tail 
-      (redex_app_r_cong redex_n m'_abs_lc) 
-      (Step.β m'_abs_lc (para_lc_r para_n))
-    -- TODO: the `Trans` instances in Cslib/Semantics/ReductionSystem/Basic.lean cause problems here
-    -- it ends up trying to take the transitive closure of the transitve closure
-    --calc
-    --  m.abs.app n ↠β m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
-    --  _           ↠β m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
-    --  _           ↠β m' ^ n'       := Relation.ReflTransGen.single (Step.β m'_abs_lc (para_lc_r para_n))
+    calc
+      m.abs.app n ↠β m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
+      _           ↠β m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
+      _           ↠β m' ^ n'       := Relation.ReflTransGen.single (Step.β m'_abs_lc (para_lc_r para_n))
 
 /-- Multiple parallel reduction is equivalent to multiple β-reduction. -/
 theorem parachain_iff_redex : (M ↠ₚ N) ↔ (M ↠β N) := by
diff --git a/Cslib/Semantics/ReductionSystem/Basic.lean b/Cslib/Semantics/ReductionSystem/Basic.lean
index f5c277d1..0df9f59b 100644
--- a/Cslib/Semantics/ReductionSystem/Basic.lean
+++ b/Cslib/Semantics/ReductionSystem/Basic.lean
@@ -42,17 +42,13 @@ theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b)
 
 open Relation Relation.ReflTransGen
 
--- these instance allow us to switch between single and multistep reductions in a `calc` block
-instance {α} (R : α → α → Prop) : Trans R R (ReflTransGen R) where
-  trans hab hbc := head hab (single hbc)
-
+-- these instances allow us to switch between single and multistep reductions in a `calc` block
 instance {α} (R : α → α → Prop) : Trans R (ReflTransGen R) (ReflTransGen R) where
   trans := head
 
 instance {α} (R : α → α → Prop) : Trans (ReflTransGen R) R (ReflTransGen R) where
   trans := tail
 
-instance (rs : ReductionSystem Term) : Trans rs.Red rs.Red rs.MRed  := by infer_instance
 instance (rs : ReductionSystem Term) : Trans rs.Red rs.MRed rs.MRed := by infer_instance
 instance (rs : ReductionSystem Term) : Trans rs.MRed rs.Red rs.MRed := by infer_instance
 
diff --git a/CslibTests/ReductionSystem.lean b/CslibTests/ReductionSystem.lean
index 727bcbc3..f31e6342 100644
--- a/CslibTests/ReductionSystem.lean
+++ b/CslibTests/ReductionSystem.lean
@@ -15,7 +15,7 @@ lemma multiple_step : 5 ↠ₙ 1 := by
     5 ⭢ₙ 4 := by simp [h]
     _ ↠ₙ 2 := by
       calc
-        4 ⭢ₙ 3 := by simp [h]
+        4 ↠ₙ 3 := by apply ReductionSystem.MRed.single; simp [h]
         _ ⭢ₙ 2 := by simp [h]
     _ ⭢ₙ 1 := by simp [h]
 

From adca73fd9396ddd9b112b709679381f6b6c3c879 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 18 Jul 2025 14:55:31 -0400
Subject: [PATCH 10/21] use Trans instance for brevity

---
 .../LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index 09e3509f..0829b0d6 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -95,7 +95,7 @@ lemma para_to_redex (para : M ⭢ₚ N) : (M ↠β N) := by
     calc
       m.abs.app n ↠β m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
       _           ↠β m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
-      _           ↠β m' ^ n'       := Relation.ReflTransGen.single (Step.β m'_abs_lc (para_lc_r para_n))
+      _           ⭢β m' ^ n'       := Step.β m'_abs_lc (para_lc_r para_n)
 
 /-- Multiple parallel reduction is equivalent to multiple β-reduction. -/
 theorem parachain_iff_redex : (M ↠ₚ N) ↔ (M ↠β N) := by

From d146a5156c44d0b1d47c91a5f217bb6bade167d7 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 18 Jul 2025 14:58:22 -0400
Subject: [PATCH 11/21] add a reference

---
 .../LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean   | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index 0829b0d6..ab55decb 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -161,6 +161,7 @@ lemma para_open_out (L : Finset Var) :
 -- TODO: the Takahashi translation would be a much nicer and shorter proof, but I had difficultly
 -- writing it for locally nameless terms.
 
+-- adapted from https://github.com/ElifUskuplu/Stlc_deBruijn/blob/main/Stlc/confluence.lean
 /-- Parallel reduction has the diamond property. -/
 theorem para_diamond : Diamond (@Parallel Var) := by
   intros t t1 t2 tpt1

From abfa7a8f57ca4766f5e0c6de1594ff6aabd2f934 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 18 Jul 2025 15:19:18 -0400
Subject: [PATCH 12/21] para_lc_l and para_lc_r as

---
 .../LocallyNameless/ConfluenceBeta.lean       | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
index ab55decb..208064b1 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
@@ -38,6 +38,7 @@ lemma para_rs_Red_eq {α} : (@para_rs α).Red = Parallel := by rfl
 variable {M M' N N' : Term Var}
 
 /-- The left side of a parallel reduction is locally closed. -/
+@[aesop unsafe]
 lemma para_lc_l (step : M ⭢ₚ N) : LC M  := by
   induction step
   case abs _ _ xs _ ih => exact LC.abs xs _ ih
@@ -47,6 +48,7 @@ lemma para_lc_l (step : M ⭢ₚ N) : LC M  := by
 variable [HasFresh Var] [DecidableEq Var]
 
 /-- The right side of a parallel reduction is locally closed. -/
+@[aesop unsafe]
 lemma para_lc_r (step : M ⭢ₚ N) : LC N := by
   induction step
   case abs _ _ xs _ ih => exact LC.abs xs _ ih
@@ -64,8 +66,7 @@ def Parallel.lc_refl (M : Term Var) : LC M → M ⭢ₚ M := by
 -- The problem is that sometimes when we apply a theorem we get out of our notation, so aesop can't
 -- see they are the same, including constructors.
 @[aesop safe]
-private def Parallel.lc_refl' (M : Term Var) : LC M → Parallel M M := by 
-  apply Parallel.lc_refl
+def Parallel.lc_refl' (M : Term Var) : LC M → Parallel M M := Parallel.lc_refl M
 
 omit [HasFresh Var] [DecidableEq Var] in
 /-- A single β-reduction implies a single parallel reduction. -/
@@ -167,12 +168,7 @@ theorem para_diamond : Diamond (@Parallel Var) := by
   intros t t1 t2 tpt1
   revert t2
   induction tpt1 <;> intros t2 tpt2
-  case fvar x =>
-    exists t2
-    and_intros
-    · assumption
-    · apply Parallel.lc_refl
-      exact para_lc_r tpt2
+  case fvar x => exact ⟨t2, by aesop⟩
   case abs s1 s2' xs mem ih => 
     cases tpt2
     case abs t2' xs' mem' =>
@@ -224,8 +220,7 @@ theorem para_diamond : Diamond (@Parallel Var) := by
     case app u1 u2' s1 s2 =>
       have ⟨l, _, _⟩ := ih1 s1
       have ⟨r, _, _⟩ := ih2 s2
-      exists app l r
-      and_intros <;> constructor <;> assumption
+      exact ⟨app l r, by aesop⟩
     case beta t1' u1' u2' xs mem s2pu2' => 
       cases s1ps1'
       case abs s1'' xs' mem' =>
@@ -240,9 +235,7 @@ theorem para_diamond : Diamond (@Parallel Var) := by
         case abs xs''' mem''' =>
           exists w1 ^ t'
           constructor
-          · apply Parallel.beta xs''
-            exact fun x a ↦ mem'' x a
-            exact qt'_l
+          · aesop (config := {enableSimp := false})
           · exact para_open_out xs''' mem''' qt'_r
 
 /-- Parallel reduction is confluent. -/

From 7903fec33428beb4fd9131b89e4dc861520a0c81 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 19 Jul 2025 13:10:49 -0400
Subject: [PATCH 13/21] naming conventions

---
 .../{BetaReduction.lean => FullBeta.lean}     | 30 +++++++++----------
 ...uenceBeta.lean => FullBetaConfluence.lean} | 21 ++++++-------
 2 files changed, 26 insertions(+), 25 deletions(-)
 rename Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/{BetaReduction.lean => FullBeta.lean} (76%)
 rename Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/{ConfluenceBeta.lean => FullBetaConfluence.lean} (93%)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
similarity index 76%
rename from Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean
rename to Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
index c6c61a61..3914482b 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/BetaReduction.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
@@ -25,35 +25,35 @@ variable {Var : Type u}
 namespace LambdaCalculus.LocallyNameless.Term
 
 /-- A single β-reduction step. -/
-@[reduction_sys beta_rs "β"]
-inductive Step : Term Var → Term Var → Prop
+@[reduction_sys fullBetaRs "βᶠ"]
+inductive FullBeta : Term Var → Term Var → Prop
 /-- Reduce an application to a lambda term. -/
-| β : LC (abs M)→ LC N → Step (app (abs M) N) (M ^ N)
+| β : LC (abs M)→ LC N → FullBeta (app (abs M) N) (M ^ N)
 /-- Left congruence rule for application. -/
-| ξₗ: LC Z → Step M N → Step (app Z M) (app Z N)
+| ξₗ: LC Z → FullBeta M N → FullBeta (app Z M) (app Z N)
 /-- Right congruence rule for application. -/
-| ξᵣ : LC Z → Step M N → Step (app M Z) (app N Z)
+| ξᵣ : LC Z → FullBeta M N → FullBeta (app M Z) (app N Z)
 /-- Congruence rule for lambda terms. -/
-| ξ (xs : Finset Var) : (∀ x ∉ xs, Step (M ^ fvar x) (N ^ fvar x)) → Step (abs M) (abs N) 
+| ξ (xs : Finset Var) : (∀ x ∉ xs, FullBeta (M ^ fvar x) (N ^ fvar x)) → FullBeta (abs M) (abs N) 
 
-open Step
+namespace FullBeta
 
 variable {M M' N N' : Term Var}
 
 /-- The left side of a reduction is locally closed. -/
-lemma step_lc_l (step : M ⭢β M') : LC M := by
+lemma step_lc_l (step : M ⭢βᶠ M') : LC M := by
   induction step <;> constructor
   all_goals assumption
 
 /-- Left congruence rule for application in multiple reduction.-/
-theorem redex_app_l_cong : (M ↠β M') → LC N → (app M N ↠β app M' N) := by
+theorem redex_app_l_cong : (M ↠βᶠ M') → LC N → (app M N ↠βᶠ app M' N) := by
   intros redex lc_N 
   induction' redex
   case refl => rfl
   case tail ih r => exact Relation.ReflTransGen.tail r (ξᵣ lc_N ih)
 
 /-- Right congruence rule for application in multiple reduction.-/
-theorem redex_app_r_cong : (M ↠β M') → LC N → (app N M ↠β app N M') := by
+theorem redex_app_r_cong : (M ↠βᶠ M') → LC N → (app N M ↠βᶠ app N M') := by
   intros redex lc_N 
   induction' redex
   case refl => rfl
@@ -62,13 +62,13 @@ theorem redex_app_r_cong : (M ↠β M') → LC N → (app N M ↠β app N M') :=
 variable [HasFresh Var] [DecidableEq Var]
 
 /-- The right side of a reduction is locally closed. -/
-lemma step_lc_r (step : M ⭢β M') : LC M' := by
+lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   induction step
   case «β» => apply beta_lc <;> assumption
   all_goals try constructor <;> assumption 
 
 /-- Substitution respects a single reduction step. -/
-lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢β s') -> (s [ x := fvar y ]) ⭢β (s' [ x := fvar y ]) := by
+lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢βᶠ s') -> (s [ x := fvar y ]) ⭢βᶠ (s' [ x := fvar y ]) := by
   intros step
   induction step
   case ξₗ ih => exact ξₗ (subst_lc (by assumption) (by constructor)) ih 
@@ -93,7 +93,7 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢β s') -> (s [ x :=
     all_goals aesop
 
 /-- Abstracting then closing preserves a single reduction. -/
-lemma step_abs_close {x : Var} : (M ⭢β M') → (abs (M⟦0 ↜ x⟧) ⭢β abs (M'⟦0 ↜ x⟧)) := by
+lemma step_abs_close {x : Var} : (M ⭢βᶠ M') → (abs (M⟦0 ↜ x⟧) ⭢βᶠ abs (M'⟦0 ↜ x⟧)) := by
   intros step
   apply ξ ∅
   intros y _
@@ -104,7 +104,7 @@ lemma step_abs_close {x : Var} : (M ⭢β M') → (abs (M⟦0 ↜ x⟧) ⭢β ab
   exact step_lc_l step
 
 /-- Abstracting then closing preserves multiple reductions. -/
-lemma redex_abs_close {x : Var} : (M ↠β M') → (abs (M⟦0 ↜ x⟧) ↠β abs (M'⟦0 ↜ x⟧)) :=  by
+lemma redex_abs_close {x : Var} : (M ↠βᶠ M') → (abs (M⟦0 ↜ x⟧) ↠βᶠ abs (M'⟦0 ↜ x⟧)) :=  by
   intros step
   induction step using Relation.ReflTransGen.trans_induction_on
   case ih₁ => rfl
@@ -112,7 +112,7 @@ lemma redex_abs_close {x : Var} : (M ↠β M') → (abs (M⟦0 ↜ x⟧) ↠β a
   case ih₃ l r => trans; exact l; exact r
 
 /-- Multiple reduction of opening implies multiple reduction of abstraction. -/
-theorem redex_abs_cong (xs : Finset Var) : (∀ x ∉ xs, (M ^ fvar x) ↠β (M' ^ fvar x)) → abs M ↠β abs M' := by
+theorem redex_abs_cong (xs : Finset Var) : (∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) → abs M ↠βᶠ abs M' := by
   intros mem
   have ⟨fresh, union⟩ := fresh_exists (xs ∪ M.fv ∪ M'.fv)
   simp only [Finset.union_assoc, Finset.mem_union, not_or] at union
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
similarity index 93%
rename from Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
rename to Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
index 208064b1..c773950d 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/ConfluenceBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
@@ -6,7 +6,7 @@ Authors: Chris Henson
 
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
 import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.BetaReduction
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBeta
 import Cslib.Utils.Relation
 
 /-! # β-confluence for the λ-calculus -/
@@ -18,7 +18,7 @@ variable {Var : Type u}
 namespace LambdaCalculus.LocallyNameless.Term
 
 /-- A parallel β-reduction step. -/
-@[aesop safe [constructors], reduction_sys para_rs "ₚ"]
+@[aesop safe [constructors], reduction_sys paraRs "ₚ"]
 inductive Parallel : Term Var → Term Var → Prop
 /-- Free variables parallel step to themselves. -/
 | fvar (x : Var) : Parallel (fvar x) (fvar x)
@@ -33,7 +33,7 @@ inductive Parallel : Term Var → Term Var → Prop
     Parallel (app (abs m) n) (m' ^ n')
 
 -- TODO: I think this could be generated along with `para_rs`
-lemma para_rs_Red_eq {α} : (@para_rs α).Red = Parallel := by rfl
+lemma para_rs_Red_eq {α} : (@paraRs α).Red = Parallel := by rfl
 
 variable {M M' N N' : Term Var}
 
@@ -70,14 +70,15 @@ def Parallel.lc_refl' (M : Term Var) : LC M → Parallel M M := Parallel.lc_refl
 
 omit [HasFresh Var] [DecidableEq Var] in
 /-- A single β-reduction implies a single parallel reduction. -/
-lemma step_to_para (step : M ⭢β N) : (M ⭢ₚ N) := by
+lemma step_to_para (step : M ⭢βᶠ N) : (M ⭢ₚ N) := by
   induction step <;> simp only [para_rs_Red_eq]
   case «β» _ abs_lc _ => cases abs_lc with | abs xs _ => 
     apply Parallel.beta xs <;> intros <;> apply Parallel.lc_refl <;> aesop
   all_goals aesop (config := {enableSimp := false})
 
+open FullBeta in
 /-- A single parallel reduction implies a multiple β-reduction. -/
-lemma para_to_redex (para : M ⭢ₚ N) : (M ↠β N) := by
+lemma para_to_redex (para : M ⭢ₚ N) : (M ↠βᶠ N) := by
   induction para
   case fvar => constructor
   case app _ _ _ _ l_para m_para redex_l redex_m =>
@@ -94,12 +95,12 @@ lemma para_to_redex (para : M ⭢ₚ N) : (M ↠β N) := by
       intros _ mem
       exact para_lc_r (para_ih _ mem)
     calc
-      m.abs.app n ↠β m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
-      _           ↠β m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
-      _           ⭢β m' ^ n'       := Step.β m'_abs_lc (para_lc_r para_n)
+      m.abs.app n ↠βᶠ m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
+      _           ↠βᶠ m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
+      _           ⭢βᶠ m' ^ n'       := β m'_abs_lc (para_lc_r para_n)
 
 /-- Multiple parallel reduction is equivalent to multiple β-reduction. -/
-theorem parachain_iff_redex : (M ↠ₚ N) ↔ (M ↠β N) := by
+theorem parachain_iff_redex : (M ↠ₚ N) ↔ (M ↠βᶠ N) := by
   refine Iff.intro ?chain_to_redex ?redex_to_chain <;> intros h <;> induction' h <;> try rfl
   case redex_to_chain.tail redex chain => exact Relation.ReflTransGen.tail chain (step_to_para redex)
   case chain_to_redex.tail para  redex => exact Relation.ReflTransGen.trans redex (para_to_redex para)
@@ -243,5 +244,5 @@ theorem para_confluence : Confluence (@Parallel Var) :=
   Relation.ReflTransGen.diamond_confluence para_diamond
 
 /-- β-reduction is confluent. -/
-theorem confluence_beta : Confluence (@Step Var) := 
+theorem confluence_beta : Confluence (@FullBeta Var) := 
   diamond_bisim parachain_iff_redex (@para_confluence Var _ _)

From 8f8ec13ea1b5bde8d2eda22aeafc69bfe039b803 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 19 Jul 2025 16:02:46 -0400
Subject: [PATCH 14/21] change confusing names

---
 .../Untyped/LocallyNameless/FullBeta.lean     | 34 +++++++++----------
 .../LocallyNameless/FullBetaConfluence.lean   |  4 +--
 2 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
index 3914482b..50a4d21b 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
@@ -28,13 +28,13 @@ namespace LambdaCalculus.LocallyNameless.Term
 @[reduction_sys fullBetaRs "βᶠ"]
 inductive FullBeta : Term Var → Term Var → Prop
 /-- Reduce an application to a lambda term. -/
-| β : LC (abs M)→ LC N → FullBeta (app (abs M) N) (M ^ N)
+| beta : LC (abs M)→ LC N → FullBeta (app (abs M) N) (M ^ N)
 /-- Left congruence rule for application. -/
-| ξₗ: LC Z → FullBeta M N → FullBeta (app Z M) (app Z N)
+| appL: LC Z → FullBeta M N → FullBeta (app Z M) (app Z N)
 /-- Right congruence rule for application. -/
-| ξᵣ : LC Z → FullBeta M N → FullBeta (app M Z) (app N Z)
+| appR : LC Z → FullBeta M N → FullBeta (app M Z) (app N Z)
 /-- Congruence rule for lambda terms. -/
-| ξ (xs : Finset Var) : (∀ x ∉ xs, FullBeta (M ^ fvar x) (N ^ fvar x)) → FullBeta (abs M) (abs N) 
+| abs (xs : Finset Var) : (∀ x ∉ xs, FullBeta (M ^ fvar x) (N ^ fvar x)) → FullBeta (abs M) (abs N) 
 
 namespace FullBeta
 
@@ -50,37 +50,37 @@ theorem redex_app_l_cong : (M ↠βᶠ M') → LC N → (app M N ↠βᶠ app M'
   intros redex lc_N 
   induction' redex
   case refl => rfl
-  case tail ih r => exact Relation.ReflTransGen.tail r (ξᵣ lc_N ih)
+  case tail ih r => exact Relation.ReflTransGen.tail r (appR lc_N ih)
 
 /-- Right congruence rule for application in multiple reduction.-/
 theorem redex_app_r_cong : (M ↠βᶠ M') → LC N → (app N M ↠βᶠ app N M') := by
   intros redex lc_N 
   induction' redex
   case refl => rfl
-  case tail ih r => exact Relation.ReflTransGen.tail r (ξₗ lc_N ih)
+  case tail ih r => exact Relation.ReflTransGen.tail r (appL lc_N ih)
 
 variable [HasFresh Var] [DecidableEq Var]
 
 /-- The right side of a reduction is locally closed. -/
 lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   induction step
-  case «β» => apply beta_lc <;> assumption
+  case beta => apply beta_lc <;> assumption
   all_goals try constructor <;> assumption 
 
 /-- Substitution respects a single reduction step. -/
 lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢βᶠ s') -> (s [ x := fvar y ]) ⭢βᶠ (s' [ x := fvar y ]) := by
   intros step
   induction step
-  case ξₗ ih => exact ξₗ (subst_lc (by assumption) (by constructor)) ih 
-  case ξᵣ ih => exact ξᵣ (subst_lc (by assumption) (by constructor)) ih  
-  case «β» m n abs_lc n_lc => 
+  case appL ih => exact appL (subst_lc (by assumption) (by constructor)) ih 
+  case appR ih => exact appR (subst_lc (by assumption) (by constructor)) ih  
+  case beta m n abs_lc n_lc => 
     cases abs_lc with | abs xs _ mem =>
       simp only [open']
       rw [subst_open x (fvar y) 0 n m (by constructor)]
-      refine «β» ?_ (subst_lc n_lc (by constructor))
+      refine beta ?_ (subst_lc n_lc (by constructor))
       exact subst_lc (LC.abs xs m mem) (LC.fvar y)
-  case ξ m' m xs mem ih => 
-    apply ξ ({x} ∪ xs)
+  case abs m' m xs mem ih => 
+    apply abs ({x} ∪ xs)
     intros z z_mem
     simp only [open']
     rw [
@@ -93,9 +93,9 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢βᶠ s') -> (s [ x
     all_goals aesop
 
 /-- Abstracting then closing preserves a single reduction. -/
-lemma step_abs_close {x : Var} : (M ⭢βᶠ M') → (abs (M⟦0 ↜ x⟧) ⭢βᶠ abs (M'⟦0 ↜ x⟧)) := by
+lemma step_abs_close {x : Var} : (M ⭢βᶠ M') → (M⟦0 ↜ x⟧.abs ⭢βᶠ M'⟦0 ↜ x⟧.abs) := by
   intros step
-  apply ξ ∅
+  apply abs ∅
   intros y _
   simp only [open']
   repeat rw [open_close_to_subst]
@@ -104,7 +104,7 @@ lemma step_abs_close {x : Var} : (M ⭢βᶠ M') → (abs (M⟦0 ↜ x⟧) ⭢β
   exact step_lc_l step
 
 /-- Abstracting then closing preserves multiple reductions. -/
-lemma redex_abs_close {x : Var} : (M ↠βᶠ M') → (abs (M⟦0 ↜ x⟧) ↠βᶠ abs (M'⟦0 ↜ x⟧)) :=  by
+lemma redex_abs_close {x : Var} : (M ↠βᶠ M') → (M⟦0 ↜ x⟧.abs ↠βᶠ M'⟦0 ↜ x⟧.abs) :=  by
   intros step
   induction step using Relation.ReflTransGen.trans_induction_on
   case ih₁ => rfl
@@ -112,7 +112,7 @@ lemma redex_abs_close {x : Var} : (M ↠βᶠ M') → (abs (M⟦0 ↜ x⟧) ↠
   case ih₃ l r => trans; exact l; exact r
 
 /-- Multiple reduction of opening implies multiple reduction of abstraction. -/
-theorem redex_abs_cong (xs : Finset Var) : (∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) → abs M ↠βᶠ abs M' := by
+theorem redex_abs_cong (xs : Finset Var) : (∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) → M.abs ↠βᶠ M'.abs := by
   intros mem
   have ⟨fresh, union⟩ := fresh_exists (xs ∪ M.fv ∪ M'.fv)
   simp only [Finset.union_assoc, Finset.mem_union, not_or] at union
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
index c773950d..97b871a4 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
@@ -72,7 +72,7 @@ omit [HasFresh Var] [DecidableEq Var] in
 /-- A single β-reduction implies a single parallel reduction. -/
 lemma step_to_para (step : M ⭢βᶠ N) : (M ⭢ₚ N) := by
   induction step <;> simp only [para_rs_Red_eq]
-  case «β» _ abs_lc _ => cases abs_lc with | abs xs _ => 
+  case beta _ abs_lc _ => cases abs_lc with | abs xs _ => 
     apply Parallel.beta xs <;> intros <;> apply Parallel.lc_refl <;> aesop
   all_goals aesop (config := {enableSimp := false})
 
@@ -97,7 +97,7 @@ lemma para_to_redex (para : M ⭢ₚ N) : (M ↠βᶠ N) := by
     calc
       m.abs.app n ↠βᶠ m'.abs.app n  := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
       _           ↠βᶠ m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc
-      _           ⭢βᶠ m' ^ n'       := β m'_abs_lc (para_lc_r para_n)
+      _           ⭢βᶠ m' ^ n'       := beta m'_abs_lc (para_lc_r para_n)
 
 /-- Multiple parallel reduction is equivalent to multiple β-reduction. -/
 theorem parachain_iff_redex : (M ↠ₚ N) ↔ (M ↠βᶠ N) := by

From 5498870513b146175c4db2196331396d9c767344 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 20 Jul 2025 15:06:01 -0400
Subject: [PATCH 15/21] aesop ruleset

---
 .../Untyped/LocallyNameless/AesopRuleset.lean |   3 +
 .../Untyped/LocallyNameless/Basic.lean        |  77 +++++++++--
 .../LocallyNameless/FullBetaConfluence.lean   |  19 +--
 .../Untyped/LocallyNameless/Properties.lean   | 122 +++++++-----------
 4 files changed, 121 insertions(+), 100 deletions(-)
 create mode 100644 Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean
new file mode 100644
index 00000000..3d5cff83
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean
@@ -0,0 +1,3 @@
+import Aesop
+
+declare_aesop_rule_sets [ln] (default := true)
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
index 8457db72..35a43618 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
@@ -6,6 +6,7 @@ Authors: Chris Henson
 
 import Cslib.Data.HasFresh
 import Cslib.Syntax.HasSubstitution
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.AesopRuleset
 
 /-! # λ-calculus
 
@@ -36,9 +37,10 @@ inductive Term (Var : Type u)
 /-- Function application. -/
 | app  : Term Var → Term Var → Term Var
 
+namespace Term
+
 /-- Variable opening of the ith bound variable. -/
-@[simp]
-def Term.openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var
+def openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var
 | bvar i' => if i = i' then sub else bvar i'
 | fvar x  => fvar x
 | app l r => app (openRec i sub l) (openRec i sub r)
@@ -46,15 +48,25 @@ def Term.openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var
 
 scoped notation:68 e "⟦" i " ↝ " sub "⟧"=> Term.openRec i sub e 
 
+@[aesop norm (rule_sets := [ln])]
+lemma openRec_bvar : (bvar i')⟦i ↝ s⟧ = if i = i' then s else bvar i' := by rfl
+
+@[aesop norm (rule_sets := [ln])]
+lemma openRec_fvar : (fvar x)⟦i ↝ s⟧ = fvar x := by rfl
+
+@[aesop norm (rule_sets := [ln])]
+lemma openRec_app : (app l r)⟦i ↝ s⟧ = app (l⟦i ↝ s⟧) (r⟦i ↝ s⟧) := by rfl
+
+@[aesop norm (rule_sets := [ln])]
+lemma openRec_abs : M.abs⟦i ↝ s⟧ = M⟦i + 1 ↝ s⟧.abs := by rfl
+
 /-- Variable opening of the closest binding. -/
-@[simp]
-def Term.open' {X} (e u):= @Term.openRec X 0 u e
+def open' {X} (e u):= @Term.openRec X 0 u e
 
 infixr:80 " ^ " => Term.open'
 
 /-- Variable closing, replacing a free `fvar x` with `bvar k` -/
-@[simp]
-def Term.closeRec (k : ℕ) (x : Var) : Term Var → Term Var
+def closeRec (k : ℕ) (x : Var) : Term Var → Term Var
 | fvar x' => if x = x' then bvar k else fvar x'
 | bvar i  => bvar i
 | app l r => app (closeRec k x l) (closeRec k x r)
@@ -62,15 +74,31 @@ def Term.closeRec (k : ℕ) (x : Var) : Term Var → Term Var
 
 scoped notation:68 e "⟦" k " ↜ " x "⟧"=> Term.closeRec k x e 
 
+variable {x : Var}
+
+omit [HasFresh Var] in
+@[aesop norm (rule_sets := [ln])]
+lemma closeRec_bvar : (bvar i)⟦k ↜ x⟧ = bvar i := by rfl
+
+omit [HasFresh Var] in
+@[aesop norm (rule_sets := [ln])]
+lemma closeRec_fvar : (fvar x')⟦k ↜ x⟧ = if x = x' then bvar k else fvar x' := by rfl
+
+omit [HasFresh Var] in
+@[aesop norm (rule_sets := [ln])]
+lemma closeRec_app : (app l r)⟦k ↜ x⟧ = app (l⟦k ↜ x⟧) (r⟦k ↜ x⟧) := by rfl
+
+omit [HasFresh Var] in
+@[aesop norm (rule_sets := [ln])]
+lemma closeRec_abs : t.abs⟦k ↜ x⟧ = t⟦k + 1 ↜ x⟧.abs := by rfl
+
 /-- Variable closing of the closest binding. -/
-@[simp]
-def Term.close {Var} [DecidableEq Var] (e u):= @Term.closeRec Var _ 0 u e
+def close {Var} [DecidableEq Var] (e u):= @Term.closeRec Var _ 0 u e
 
 infixr:80 " ^* " => Term.close
 
 /- Substitution of a free variable to a term. -/
-@[simp]
-def Term.subst (m : Term Var) (x : Var) (sub : Term Var) : Term Var :=
+def subst (m : Term Var) (x : Var) (sub : Term Var) : Term Var :=
   match m with
   | bvar i  => bvar i
   | fvar x' => if x = x' then sub else fvar x'
@@ -78,23 +106,44 @@ def Term.subst (m : Term Var) (x : Var) (sub : Term Var) : Term Var :=
   | abs M   => abs $ M.subst x sub
 
 /-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
-@[simp]
 instance instHasSubstitutionTerm : HasSubstitution (Term Var) Var where
   subst := Term.subst
 
 omit [HasFresh Var] in
-lemma Term.subst_def (m : Term Var) (x : Var) (n : Term Var) : m.subst x n = m[x := n] := by rfl
+@[aesop norm (rule_sets := [ln])]
+lemma subst_bvar {n : Term Var} : (bvar i)[x := n] = bvar i := by rfl
+
+omit [HasFresh Var] in
+@[aesop norm (rule_sets := [ln])]
+lemma subst_fvar : (fvar x')[x := n] = if x = x' then n else fvar x' := by rfl
+
+omit [HasFresh Var] in
+@[aesop norm (rule_sets := [ln])]
+lemma subst_app {l r : Term Var} : (app l r)[x := n] = app (l[x := n]) (r[x := n]) := by rfl
+
+omit [HasFresh Var] in
+@[aesop norm (rule_sets := [ln])]
+lemma subst_abs {M : Term Var} : M.abs[x := n] = M[x := n].abs := by rfl
+
+omit [HasFresh Var] in
+@[aesop norm (rule_sets := [ln])]
+lemma subst_def (m : Term Var) (x : Var) (n : Term Var) : m.subst x n = m[x := n] := by rfl
 
 /-- Free variables of a term. -/
 @[simp]
-def Term.fv : Term Var → Finset Var
+def fv : Term Var → Finset Var
 | bvar _ => {}
 | fvar x => {x}
 | abs e1 => e1.fv
 | app l r => l.fv ∪ r.fv
 
+omit [HasFresh Var] in
+@[simp]
+lemma fv_bvar : x ∉ (bvar i).fv := by simp
+
 /-- Locally closed terms. -/
-inductive Term.LC : Term Var → Prop
+@[aesop safe (rule_sets := [ln]) [constructors]]
+inductive LC : Term Var → Prop
 | fvar (x)  : LC (fvar x)
 | abs (L : Finset Var) (e : Term Var) : (∀ x : Var, x ∉ L → LC (e ^ fvar x)) → LC (abs e)
 | app {l r} : l.LC → r.LC → LC (app l r)
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
index 97b871a4..db52b71e 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
@@ -18,7 +18,7 @@ variable {Var : Type u}
 namespace LambdaCalculus.LocallyNameless.Term
 
 /-- A parallel β-reduction step. -/
-@[aesop safe [constructors], reduction_sys paraRs "ₚ"]
+@[aesop safe (rule_sets := [ln]) [constructors], reduction_sys paraRs "ₚ"]
 inductive Parallel : Term Var → Term Var → Prop
 /-- Free variables parallel step to themselves. -/
 | fvar (x : Var) : Parallel (fvar x) (fvar x)
@@ -108,19 +108,20 @@ theorem parachain_iff_redex : (M ↠ₚ N) ↔ (M ↠βᶠ N) := by
 /-- Parallel reduction respects substitution. -/
 lemma para_subst (x : Var) : (M ⭢ₚ M') → (N ⭢ₚ N') → (M[x := N] ⭢ₚ M'[x := N']) := by
   intros pm pn
-  induction pm <;> simp only [instHasSubstitutionTerm, subst, open']
-  case fvar x' =>
-    split
-    assumption
-    constructor
+  induction pm
+  case fvar => aesop
   case beta _ _ _ _ xs _ _ ih _ => 
-    repeat rw [subst_def]
+    simp only [open']
     rw [subst_open _ _ _ _ _ (para_lc_r pn)]
     apply Parallel.beta (xs ∪ {x})
     intros y ymem
     simp only [Finset.mem_union, Finset.mem_singleton, not_or] at ymem
     push_neg at ymem
-    rw [subst_open_var _ _ _ _ _ (para_lc_r pn), subst_open_var _ _ _ _ _ (para_lc_l pn)]
+    rw [
+      subst_def, 
+      subst_open_var _ _ _ _ _ (para_lc_r pn), 
+      subst_open_var _ _ _ _ _ (para_lc_l pn)
+    ]
     apply ih
     all_goals aesop
   case app => constructor <;> assumption
@@ -198,7 +199,7 @@ theorem para_diamond : Diamond (@Parallel Var) := by
         constructor
         · rw [subst_intro x s2' _ q4 (para_lc_l qt'_l), 
               subst_intro x t' _ (close_var_not_fvar x t'') (para_lc_r qt'_l)]
-          simp only [instHasSubstitutionTerm, open', close]
+          simp only [open', close]
           rw [close_open _ _ _ (para_lc_r qt''_l)]
           exact para_subst x qt''_l qt'_l
         · apply Parallel.beta ((s1'' ^ fvar x).fv ∪ t''.fv ∪ {x})
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
index 2ca6e005..7fa9ca92 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
@@ -12,44 +12,43 @@ variable {Var : Type u}
 
 namespace LambdaCalculus.LocallyNameless.Term
 
+lemma open_app_inj : app l r = (app l r)⟦i ↝ s⟧ ↔ l = l⟦i ↝ s⟧ ∧ r = r⟦i ↝ s⟧ := by
+  simp [openRec]
+
+lemma open_abs_inj : M.abs = M⟦i + 1 ↝ s⟧.abs ↔ M = M⟦i + 1 ↝ s⟧ := by
+  simp
+
 /-- An opening appearing in both sides of an equality of terms can be removed. -/
 lemma open_lc_aux (e : Term Var) : ∀ (j v i u),
   i ≠ j ->
   e ⟦j ↝ v⟧ = (e ⟦j ↝ v⟧) ⟦i ↝ u⟧ ->
   e = e ⟦i ↝ u⟧ := by
-  induction' e 
-  <;> intros j v i u neq h 
-  <;> simp only [openRec, app.injEq, abs.injEq] at *
-  case bvar => aesop
-  case app ih_l ih_r => 
-    obtain ⟨hl, hr⟩ := h
+  induction' e <;> intros j v i u neq h 
+  case app l r ih_l ih_r => 
+    obtain ⟨hl, hr⟩ := open_app_inj.mp h
+    simp only [open_app_inj]
     exact ⟨ih_l j v i u neq hl, ih_r j v i u neq hr⟩
-  case abs ih => exact ih (j+1) v (i+1) u (by aesop) h
+  case abs ih =>
+    simp only [openRec_abs, open_abs_inj] at *
+    exact ih (j+1) v (i+1) u (by aesop) h
+  all_goals aesop
 
 /-- Opening is associative for nonclashing free variables. -/
 lemma swap_open_fvars (k n : ℕ) (x y : Var) (m : Term Var) : 
     k ≠ n → x ≠ y → m⟦n ↝ fvar y⟧⟦k ↝ fvar x⟧ = m⟦k ↝ fvar x⟧⟦n ↝ fvar y⟧ := by
   revert k n
-  induction' m <;> intros k n ne_kn ne_xy <;> simp only [openRec, app.injEq, abs.injEq]
-  case bvar n' => aesop
-  case abs ih => apply ih <;> aesop
-  case app => aesop
+  induction' m <;> aesop
 
 variable [DecidableEq Var]
 
 /-- Substitution of a free variable not present in a term leaves it unchanged. -/
 theorem subst_fresh (x : Var) (t sub : Term Var) : x ∉ t.fv → (t [x := sub]) = t := by
-  induction t <;> intros <;> aesop
+  induction t <;> aesop
 
 /- Opening and closing are inverses. -/
 lemma open_close (x : Var) (t : Term Var) (k : ℕ) : x ∉ t.fv → t⟦k ↝ fvar x⟧⟦k ↜ x⟧ = t := by
-  intros mem
   revert k
-  induction t <;> intros k <;> simp only [openRec, closeRec, app.injEq, abs.injEq]
-  case bvar n => split <;> simp_all
-  case abs t ih => exact ih mem (k + 1)
-  case app l r ih_l ih_r => refine ⟨ih_l ?_ k, ih_r ?_ k⟩ <;> aesop
-  all_goals aesop
+  induction t <;> aesop
 
 /-- Opening is injective. -/
 lemma open_injective (x : Var) (M M' : Term Var) : x ∉ M.fv → x ∉ M'.fv → M ^ fvar x = M' ^ fvar x → M = M' := by
@@ -61,49 +60,27 @@ lemma open_injective (x : Var) (M M' : Term Var) : x ∉ M.fv → x ∉ M'.fv 
 lemma swap_open_fvar_close (k n: ℕ) (x y : Var) (m : Term Var) : 
     k ≠ n → x ≠ y → m⟦n ↝ fvar y⟧⟦k ↜ x⟧ = m⟦k ↜ x⟧⟦n ↝ fvar y⟧ := by
   revert k n
-  induction' m 
-  <;> intros k n ne_kn ne_xy 
-  <;> simp only [openRec, closeRec, app.injEq, abs.injEq]
-  case bvar n'  => split <;> aesop
-  case fvar x'  => split <;> aesop
-  case abs ih => apply ih <;> aesop
-  case app => aesop
+  induction' m <;> aesop
 
 /-- Closing preserves free variables. -/
 lemma close_preserve_not_fvar {k x y} (m : Term Var) : x ∉ m.fv → x ∉ (m⟦k ↜ y⟧).fv := by
-  intros mem
   revert k
-  induction m <;> intros k <;> simp only [closeRec]
-  case fvar y' => split <;> aesop
-  case abs ih => exact ih mem
-  all_goals aesop
+  induction m <;> aesop
 
 /-- Opening to a fresh free variable preserves free variables. -/
 lemma open_fresh_preserve_not_fvar {k x y} (m : Term Var) : x ∉ m.fv → x ≠ y → x ∉ (m⟦k ↝ fvar y⟧).fv := by
-  intros mem neq
   revert k
-  induction m <;> intros k <;> simp only [openRec]
-  case bvar n'  => split <;> aesop
-  case fvar => aesop
-  case abs ih => exact ih mem
-  all_goals aesop
+  induction m <;> aesop
 
 /-- Substitution preserves free variables. -/
 lemma subst_preserve_not_fvar {x y : Var} (m n : Term Var) : x ∉ m.fv ∪ n.fv → x ∉ (m [y := n]).fv := by
-  intros mem
-  simp only [Finset.mem_union, not_or] at mem
-  induction m <;> simp only [instHasSubstitutionTerm, subst]
-  case fvar y' => split <;> simp only [fv, Finset.mem_singleton, mem] <;> aesop
-  case abs ih => exact ih mem
+  induction m
   all_goals aesop
 
 /-- Closing removes a free variable. -/
 lemma close_var_not_fvar_rec (x) (k) (t : Term Var) : x ∉ (t⟦k ↜ x⟧).fv := by
   revert k
-  induction t <;> intros k <;> simp only [closeRec]
-  case fvar x' => split <;> simp_all
-  case abs ih => exact ih (k + 1)
-  all_goals aesop
+  induction t <;> aesop
 
 /-- Specializes `close_var_not_fvar_rec` to first closing. -/
 lemma close_var_not_fvar (x) (t : Term Var) : x ∉ (t ^* x).fv := close_var_not_fvar_rec x 0 t
@@ -112,55 +89,47 @@ variable [HasFresh Var]
 
 omit [DecidableEq Var] in
 /-- A locally closed term is unchanged by opening. -/
+@[aesop safe (rule_sets := [ln])]
 lemma open_lc (k t) (e : Term Var) : e.LC → e = e⟦k ↝ t⟧ := by
   intros e_lc
   revert k
-  induction e_lc <;> intros k <;> simp only [openRec, app.injEq, abs.injEq]
-  case app => aesop
-  case abs xs e _ ih => refine open_lc_aux e 0 (fvar (fresh xs)) (k+1) t ?_ ?_ <;> aesop
+  induction e_lc
+  case abs xs e _ ih => 
+    intros k
+    simp only [openRec, abs.injEq]
+    refine open_lc_aux e 0 (fvar (fresh xs)) (k+1) t ?_ ?_ <;> aesop
+  all_goals aesop
 
 /-- Substitution of a locally closed term distributes with opening. -/
 lemma subst_open (x : Var) (t : Term Var) (k : ℕ) (u e) :
   LC t → 
   (e ⟦ k ↝ u ⟧) [ x := t ] = (e [ x := t ]) ⟦k ↝  u [ x := t ]⟧ := by
   revert k
-  induction' e 
-  <;> intros k t_lv 
-  <;> simp only [openRec, instHasSubstitutionTerm, subst, app.injEq, abs.injEq]
-  case bvar k' => aesop
-  case fvar x' => 
-    split <;> simp_all
-    exact open_lc k (u[x':=t]) t t_lv
-  case abs ih => exact ih (k + 1) t_lv
-  case app ih_l ih_r => exact ⟨ih_l k t_lv, ih_r k t_lv⟩
+  induction' e <;> aesop
 
 /-- Specialize `subst_open` to the first opening. -/
 theorem subst_open_var (x y : Var) (u e : Term Var) : y ≠ x → LC u → (e [y := u]) ^ fvar x = (e ^ fvar x) [y := u] := by
   intros neq u_lc
-  have := subst_open y u 0 (fvar x) e u_lc
+  have h : (e ^ fvar x)[y:=u] = e[y:=u] ^ (fvar x)[y:=u] := subst_open y u 0 (fvar x) e u_lc
   aesop
 
 /-- Substitution of locally closed terms is locally closed. -/
 theorem subst_lc {x : Var} {e u : Term Var} : LC e → LC u → LC (e [x := u]) := by
   intros lc_e lc_u
-  induction lc_e <;> simp only [instHasSubstitutionTerm, subst]
-  case fvar => split <;> [assumption; constructor] 
-  case app ih_l ih_r => exact LC.app ih_l ih_r
+  induction lc_e 
   case abs xs e _ ih =>
     refine LC.abs ({x} ∪ xs) _ (?_ : ∀ y ∉ {x} ∪ xs, (e[x := u] ^ fvar y).LC)
     intros y mem
     rw [subst_open_var y x u e ?_ lc_u]
-    apply ih
     all_goals aesop
+  all_goals aesop
 
 /-- Opening to a term `t` is equivalent to opening to a free variable and substituting it for `t`. -/
 lemma subst_intro (x : Var) (t e : Term Var) : x ∉ e.fv → LC t → e ^ t = (e ^ fvar x) [ x := t ] := by
   intros mem t_lc
   simp only [open']
-  rw [subst_open x t 0 (fvar x) e t_lc]
-  have s := subst_fresh _ _ t mem
-  simp only [instHasSubstitutionTerm, subst, ↓reduceIte] at *
-  rw [s]
+  rw [subst_open x t 0 (fvar x) e t_lc, subst_fresh _ _ t mem]
+  aesop
 
 /-- Opening of locally closed terms is locally closed. -/
 theorem beta_lc {M N : Term Var} : LC (abs M) → LC N → LC (M ^ N) := by
@@ -174,23 +143,20 @@ theorem beta_lc {M N : Term Var} : LC (abs M) → LC N → LC (M ^ N) := by
     rw [subst_intro y N M]
     apply subst_lc
     apply mem
-    all_goals aesop        
+    all_goals aesop
 
 /-- Opening then closing is equivalent to substitution. -/
 lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) : LC m → m ⟦k ↜ x⟧⟦k ↝ fvar y⟧ = m [x := fvar y] := by
   intros m_lc
   revert k
   induction' m_lc 
-  <;> intros k 
-  <;> simp only [closeRec, openRec, instHasSubstitutionTerm, subst, abs.injEq, app.injEq]
-  case fvar x' => split <;> simp
-  case app ih_l ih_r => exact ⟨ih_l _, ih_r _⟩
   case abs xs t x_mem ih =>
+    intros k
     have ⟨x', x'_mem⟩ := fresh_exists ({x} ∪ {y} ∪ t.fv ∪ xs)
     have s := subst_open_var x' x (fvar y) t ?_ (by constructor)
-    simp only [open', Finset.union_assoc, Finset.mem_union, Finset.mem_singleton, not_or] at *
-    rw [←open_close x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ fvar y⟧) 0 ?f₁, ←open_close x' (t.subst x (fvar y)) 0 ?f₂]
-    simp [instHasSubstitutionTerm] at s
+    simp only [closeRec_abs, openRec_abs, subst_abs]
+    rw [←open_close x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ fvar y⟧) 0 ?f₁, ←open_close x' (t[x := fvar y]) 0 ?f₂]
+    simp only [open'] at *
     rw [swap_open_fvars, ←swap_open_fvar_close, s, ih]
     case f₁ =>
       apply open_fresh_preserve_not_fvar
@@ -200,14 +166,16 @@ lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) : LC m → m ⟦k
       apply subst_preserve_not_fvar
       aesop
     all_goals aesop
+  all_goals aesop
 
 /-- Closing and opening are inverses. -/
 lemma close_open (x : Var) (t : Term Var) (k : ℕ) : LC t → t⟦k ↜ x⟧⟦k ↝ fvar x⟧ = t := by
   intros lc_t
   revert k
-  induction lc_t <;> intros k <;> simp only [closeRec, openRec, abs.injEq, app.injEq]
-  case fvar x' => split <;> simp_all
+  induction lc_t
   case abs xs t t_open_lc ih => 
+    intros k
+    simp only [closeRec_abs, openRec_abs, abs.injEq]
     have ⟨y, hy⟩ := fresh_exists (xs ∪ t.fv ∪ (t⟦k + 1 ↜ x⟧⟦k + 1 ↝ fvar x⟧).fv ∪ {x})
     simp only [Finset.union_assoc, Finset.mem_union, Finset.mem_singleton, not_or] at hy
     obtain ⟨q1, q2, q3, q4⟩ := hy
@@ -216,4 +184,4 @@ lemma close_open (x : Var) (t : Term Var) (k : ℕ) : LC t → t⟦k ↜ x⟧⟦
     simp only [open']
     rw [swap_open_fvar_close, swap_open_fvars]
     all_goals aesop
-  case app => aesop
+  all_goals aesop

From d6ad80d96c2585b7953653dc7a705807c83350f5 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 20 Jul 2025 15:15:28 -0400
Subject: [PATCH 16/21] rm unused lemma

---
 .../LambdaCalculus/Untyped/LocallyNameless/Basic.lean         | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
index 35a43618..1c7fc5a3 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
@@ -137,10 +137,6 @@ def fv : Term Var → Finset Var
 | abs e1 => e1.fv
 | app l r => l.fv ∪ r.fv
 
-omit [HasFresh Var] in
-@[simp]
-lemma fv_bvar : x ∉ (bvar i).fv := by simp
-
 /-- Locally closed terms. -/
 @[aesop safe (rule_sets := [ln]) [constructors]]
 inductive LC : Term Var → Prop

From f9c6b1217c21e2e11c18c408e5a9828532bd4ac3 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 20 Jul 2025 16:52:06 -0400
Subject: [PATCH 17/21] ASCII arrows

---
 .../LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean      | 2 +-
 .../LambdaCalculus/Untyped/LocallyNameless/Properties.lean    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
index 50a4d21b..35bc61bc 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
@@ -68,7 +68,7 @@ lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   all_goals try constructor <;> assumption 
 
 /-- Substitution respects a single reduction step. -/
-lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢βᶠ s') -> (s [ x := fvar y ]) ⭢βᶠ (s' [ x := fvar y ]) := by
+lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢βᶠ s') → (s [ x := fvar y ]) ⭢βᶠ (s' [ x := fvar y ]) := by
   intros step
   induction step
   case appL ih => exact appL (subst_lc (by assumption) (by constructor)) ih 
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
index 7fa9ca92..18abd493 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
@@ -20,8 +20,8 @@ lemma open_abs_inj : M.abs = M⟦i + 1 ↝ s⟧.abs ↔ M = M⟦i + 1 ↝ s⟧ :
 
 /-- An opening appearing in both sides of an equality of terms can be removed. -/
 lemma open_lc_aux (e : Term Var) : ∀ (j v i u),
-  i ≠ j ->
-  e ⟦j ↝ v⟧ = (e ⟦j ↝ v⟧) ⟦i ↝ u⟧ ->
+  i ≠ j →
+  e ⟦j ↝ v⟧ = (e ⟦j ↝ v⟧) ⟦i ↝ u⟧ →
   e = e ⟦i ↝ u⟧ := by
   induction' e <;> intros j v i u neq h 
   case app l r ih_l ih_r => 

From 64c57d95fc5eb60021d2345a72a25d2978141f63 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 20 Jul 2025 16:53:52 -0400
Subject: [PATCH 18/21] missed rule_sets

---
 .../Untyped/LocallyNameless/FullBetaConfluence.lean       | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
index db52b71e..31d68519 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
@@ -38,7 +38,7 @@ lemma para_rs_Red_eq {α} : (@paraRs α).Red = Parallel := by rfl
 variable {M M' N N' : Term Var}
 
 /-- The left side of a parallel reduction is locally closed. -/
-@[aesop unsafe]
+@[aesop unsafe (rule_sets := [ln])]
 lemma para_lc_l (step : M ⭢ₚ N) : LC M  := by
   induction step
   case abs _ _ xs _ ih => exact LC.abs xs _ ih
@@ -48,7 +48,7 @@ lemma para_lc_l (step : M ⭢ₚ N) : LC M  := by
 variable [HasFresh Var] [DecidableEq Var]
 
 /-- The right side of a parallel reduction is locally closed. -/
-@[aesop unsafe]
+@[aesop unsafe (rule_sets := [ln])]
 lemma para_lc_r (step : M ⭢ₚ N) : LC N := by
   induction step
   case abs _ _ xs _ ih => exact LC.abs xs _ ih
@@ -56,7 +56,7 @@ lemma para_lc_r (step : M ⭢ₚ N) : LC N := by
   all_goals constructor <;> assumption
 
 /-- Parallel reduction is reflexive for locally closed terms. -/
-@[aesop safe]
+@[aesop safe (rule_sets := [ln])]
 def Parallel.lc_refl (M : Term Var) : LC M → M ⭢ₚ M := by
   intros lc
   induction lc
@@ -65,7 +65,7 @@ def Parallel.lc_refl (M : Term Var) : LC M → M ⭢ₚ M := by
 -- TODO: better ways to handle this?
 -- The problem is that sometimes when we apply a theorem we get out of our notation, so aesop can't
 -- see they are the same, including constructors.
-@[aesop safe]
+@[aesop safe (rule_sets := [ln])]
 def Parallel.lc_refl' (M : Term Var) : LC M → Parallel M M := Parallel.lc_refl M
 
 omit [HasFresh Var] [DecidableEq Var] in

From 78e251f85de21b9ac619ea888802082996825948 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 20 Jul 2025 17:21:00 -0400
Subject: [PATCH 19/21] use proof irrelevance

---
 .../Untyped/LocallyNameless/FullBetaConfluence.lean      | 9 +++++++--
 Cslib/Utils/Relation.lean                                | 8 +-------
 2 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
index 31d68519..3d0ca3dd 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
@@ -245,5 +245,10 @@ theorem para_confluence : Confluence (@Parallel Var) :=
   Relation.ReflTransGen.diamond_confluence para_diamond
 
 /-- β-reduction is confluent. -/
-theorem confluence_beta : Confluence (@FullBeta Var) := 
-  diamond_bisim parachain_iff_redex (@para_confluence Var _ _)
+theorem confluence_beta : Confluence (@FullBeta Var) := by
+  simp only [Confluence]
+  have eq : Relation.ReflTransGen (@Parallel Var) = Relation.ReflTransGen (@FullBeta Var) := by
+    ext
+    exact parachain_iff_redex
+  rw [←eq]
+  exact @para_confluence Var _ _
diff --git a/Cslib/Utils/Relation.lean b/Cslib/Utils/Relation.lean
index d35bf3fa..ceaf7382 100644
--- a/Cslib/Utils/Relation.lean
+++ b/Cslib/Utils/Relation.lean
@@ -29,7 +29,7 @@ lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) :
     obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D
     exact ⟨D', ⟨B_D', head CD D_D'⟩⟩
 
-/-- The dismond property implies confluence. -/
+/-- The diamond property implies confluence. -/
 theorem Relation.ReflTransGen.diamond_confluence (h : Diamond R) : Confluence R := by
   intros A B C AB BC
   revert C
@@ -40,12 +40,6 @@ theorem Relation.ReflTransGen.diamond_confluence (h : Diamond R) : Confluence R
     obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D
     exact ⟨D', ⟨B_D', trans CD D_D'⟩⟩
 
-/-- Equivalence of relations preserves the diamond property. -/
-theorem diamond_bisim (sim : ∀ {M N : α}, R M N ↔ R' M N) (h : Diamond R) : Diamond R' := by
-  intros L M₁ M₂ L_M₁ L_M₂
-  have ⟨N, ⟨M₁_chain_N, M₂_chain_N⟩⟩ := h (sim.mpr L_M₁) (sim.mpr L_M₂)
-  exact ⟨N, ⟨sim.mp M₁_chain_N, sim.mp M₂_chain_N⟩⟩
-
 -- not sure why this doesn't compile as an "instance" but oh well
 def trans_of_subrelation {α : Type _} (s s' r : α → α → Prop) (hr : Transitive r)
     (h : ∀ a b : α, s a b → r a b) (h' : ∀ a b : α, s' a b → r a b) : Trans s s' r where

From eee9754f4b4c297316ac46bc4e2ac03e3eed0cf3 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 20 Jul 2025 23:46:28 -0400
Subject: [PATCH 20/21] style

---
 .../LambdaCalculus/Untyped/LocallyNameless/Properties.lean      | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
index 18abd493..57474404 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
@@ -96,7 +96,7 @@ lemma open_lc (k t) (e : Term Var) : e.LC → e = e⟦k ↝ t⟧ := by
   induction e_lc
   case abs xs e _ ih => 
     intros k
-    simp only [openRec, abs.injEq]
+    simp only [openRec_abs, abs.injEq]
     refine open_lc_aux e 0 (fvar (fresh xs)) (k+1) t ?_ ?_ <;> aesop
   all_goals aesop
 

From de77456cd712cca16aab369646a474e8a290e19c Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 21 Jul 2025 13:36:15 -0400
Subject: [PATCH 21/21] namespace rule set

---
 .../Untyped/LocallyNameless/AesopRuleset.lean |  2 +-
 .../Untyped/LocallyNameless/Basic.lean        | 28 +++++++++----------
 .../LocallyNameless/FullBetaConfluence.lean   | 10 +++----
 .../Untyped/LocallyNameless/Properties.lean   |  2 +-
 4 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean
index 3d5cff83..1e43b5ba 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean
@@ -1,3 +1,3 @@
 import Aesop
 
-declare_aesop_rule_sets [ln] (default := true)
+declare_aesop_rule_sets [LambdaCalculus.LocallyNameless.ruleSet] (default := true)
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
index 1c7fc5a3..646cae50 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
@@ -48,16 +48,16 @@ def openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var
 
 scoped notation:68 e "⟦" i " ↝ " sub "⟧"=> Term.openRec i sub e 
 
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma openRec_bvar : (bvar i')⟦i ↝ s⟧ = if i = i' then s else bvar i' := by rfl
 
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma openRec_fvar : (fvar x)⟦i ↝ s⟧ = fvar x := by rfl
 
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma openRec_app : (app l r)⟦i ↝ s⟧ = app (l⟦i ↝ s⟧) (r⟦i ↝ s⟧) := by rfl
 
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma openRec_abs : M.abs⟦i ↝ s⟧ = M⟦i + 1 ↝ s⟧.abs := by rfl
 
 /-- Variable opening of the closest binding. -/
@@ -77,19 +77,19 @@ scoped notation:68 e "⟦" k " ↜ " x "⟧"=> Term.closeRec k x e
 variable {x : Var}
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma closeRec_bvar : (bvar i)⟦k ↜ x⟧ = bvar i := by rfl
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma closeRec_fvar : (fvar x')⟦k ↜ x⟧ = if x = x' then bvar k else fvar x' := by rfl
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma closeRec_app : (app l r)⟦k ↜ x⟧ = app (l⟦k ↜ x⟧) (r⟦k ↜ x⟧) := by rfl
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma closeRec_abs : t.abs⟦k ↜ x⟧ = t⟦k + 1 ↜ x⟧.abs := by rfl
 
 /-- Variable closing of the closest binding. -/
@@ -110,23 +110,23 @@ instance instHasSubstitutionTerm : HasSubstitution (Term Var) Var where
   subst := Term.subst
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma subst_bvar {n : Term Var} : (bvar i)[x := n] = bvar i := by rfl
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma subst_fvar : (fvar x')[x := n] = if x = x' then n else fvar x' := by rfl
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma subst_app {l r : Term Var} : (app l r)[x := n] = app (l[x := n]) (r[x := n]) := by rfl
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma subst_abs {M : Term Var} : M.abs[x := n] = M[x := n].abs := by rfl
 
 omit [HasFresh Var] in
-@[aesop norm (rule_sets := [ln])]
+@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma subst_def (m : Term Var) (x : Var) (n : Term Var) : m.subst x n = m[x := n] := by rfl
 
 /-- Free variables of a term. -/
@@ -138,7 +138,7 @@ def fv : Term Var → Finset Var
 | app l r => l.fv ∪ r.fv
 
 /-- Locally closed terms. -/
-@[aesop safe (rule_sets := [ln]) [constructors]]
+@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet]) [constructors]]
 inductive LC : Term Var → Prop
 | fvar (x)  : LC (fvar x)
 | abs (L : Finset Var) (e : Term Var) : (∀ x : Var, x ∉ L → LC (e ^ fvar x)) → LC (abs e)
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
index 3d0ca3dd..5dfc85ba 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
@@ -18,7 +18,7 @@ variable {Var : Type u}
 namespace LambdaCalculus.LocallyNameless.Term
 
 /-- A parallel β-reduction step. -/
-@[aesop safe (rule_sets := [ln]) [constructors], reduction_sys paraRs "ₚ"]
+@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet]) [constructors], reduction_sys paraRs "ₚ"]
 inductive Parallel : Term Var → Term Var → Prop
 /-- Free variables parallel step to themselves. -/
 | fvar (x : Var) : Parallel (fvar x) (fvar x)
@@ -38,7 +38,7 @@ lemma para_rs_Red_eq {α} : (@paraRs α).Red = Parallel := by rfl
 variable {M M' N N' : Term Var}
 
 /-- The left side of a parallel reduction is locally closed. -/
-@[aesop unsafe (rule_sets := [ln])]
+@[aesop unsafe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma para_lc_l (step : M ⭢ₚ N) : LC M  := by
   induction step
   case abs _ _ xs _ ih => exact LC.abs xs _ ih
@@ -48,7 +48,7 @@ lemma para_lc_l (step : M ⭢ₚ N) : LC M  := by
 variable [HasFresh Var] [DecidableEq Var]
 
 /-- The right side of a parallel reduction is locally closed. -/
-@[aesop unsafe (rule_sets := [ln])]
+@[aesop unsafe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma para_lc_r (step : M ⭢ₚ N) : LC N := by
   induction step
   case abs _ _ xs _ ih => exact LC.abs xs _ ih
@@ -56,7 +56,7 @@ lemma para_lc_r (step : M ⭢ₚ N) : LC N := by
   all_goals constructor <;> assumption
 
 /-- Parallel reduction is reflexive for locally closed terms. -/
-@[aesop safe (rule_sets := [ln])]
+@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 def Parallel.lc_refl (M : Term Var) : LC M → M ⭢ₚ M := by
   intros lc
   induction lc
@@ -65,7 +65,7 @@ def Parallel.lc_refl (M : Term Var) : LC M → M ⭢ₚ M := by
 -- TODO: better ways to handle this?
 -- The problem is that sometimes when we apply a theorem we get out of our notation, so aesop can't
 -- see they are the same, including constructors.
-@[aesop safe (rule_sets := [ln])]
+@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 def Parallel.lc_refl' (M : Term Var) : LC M → Parallel M M := Parallel.lc_refl M
 
 omit [HasFresh Var] [DecidableEq Var] in
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
index 57474404..69fbb9b2 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
@@ -89,7 +89,7 @@ variable [HasFresh Var]
 
 omit [DecidableEq Var] in
 /-- A locally closed term is unchanged by opening. -/
-@[aesop safe (rule_sets := [ln])]
+@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 lemma open_lc (k t) (e : Term Var) : e.LC → e = e⟦k ↝ t⟧ := by
   intros e_lc
   revert k