Locally Nameless Beta Confluence

Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean

@@ -0,0 +1,3 @@
+import Aesop
+
+declare_aesop_rule_sets [LambdaCalculus.LocallyNameless.ruleSet] (default := true)

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,62 +37,109 @@ 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)
 | abs M   => abs $ openRec (i+1) sub M
 
 scoped notation:68 e "⟦" i " ↝ " sub "⟧"=> Term.openRec i sub e 
 
+@[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 := [LambdaCalculus.LocallyNameless.ruleSet])]
+lemma openRec_fvar : (fvar x)⟦i ↝ s⟧ = fvar x := by rfl
+
+@[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 := [LambdaCalculus.LocallyNameless.ruleSet])]
+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)
 | abs t   => abs $ closeRec (k+1) x t
 
 scoped notation:68 e "⟦" k " ↜ " x "⟧"=> Term.closeRec k x e 
 
+variable {x : Var}
+
+omit [HasFresh Var] in
+@[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 := [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 := [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 := [LambdaCalculus.LocallyNameless.ruleSet])]
+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'
   | app l r => app (l.subst x sub) (r.subst x sub)
   | 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
+@[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 := [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 := [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 := [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 := [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. -/
 @[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
 
 /-- Locally closed terms. -/
-inductive Term.LC : Term Var → Prop
+@[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)
 | app {l r} : l.LC → r.LC → LC (app l r)

Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean

@@ -0,0 +1,122 @@
+/-
+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.Semantics.ReductionSystem.Basic
+
+/-! # β-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. -/
+@[reduction_sys fullBetaRs "βᶠ"]
+inductive FullBeta : Term Var → Term Var → Prop
+/-- Reduce an application to a lambda term. -/
+| beta : LC (abs M)→ LC N → FullBeta (app (abs M) N) (M ^ N)
+/-- Left congruence rule for application. -/
+| appL: LC Z → FullBeta M N → FullBeta (app Z M) (app Z N)
+/-- Right congruence rule for application. -/
+| appR : LC Z → FullBeta M N → FullBeta (app M Z) (app N Z)
+/-- Congruence rule for lambda terms. -/
+| abs (xs : Finset Var) : (∀ x ∉ xs, FullBeta (M ^ fvar x) (N ^ fvar x)) → FullBeta (abs M) (abs N) 
+
+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
+  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 (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 (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 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 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 beta ?_ (subst_lc n_lc (by constructor))
+      exact subst_lc (LC.abs xs m mem) (LC.fvar y)
+  case abs m' m xs mem ih => 
+    apply abs ({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') → (M⟦0 ↜ x⟧.abs ⭢βᶠ M'⟦0 ↜ x⟧.abs) := by
+  intros step
+  apply abs ∅
+  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') → (M⟦0 ↜ x⟧.abs ↠βᶠ M'⟦0 ↜ x⟧.abs) :=  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)) → 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
+  obtain ⟨_, _, _⟩ := union
+  rw [←open_close fresh M 0 ?_, ←open_close fresh M' 0 ?_]
+  refine redex_abs_close (mem fresh ?_)
+  all_goals assumption