feat(LambdaCalculus): basics of named representation (alpha equivalence and capture-avoiding substitution)

Cslib.lean

@@ -93,6 +93,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaCon
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
 public import Cslib.Logics.HML.Basic
 public import Cslib.Logics.LinearLogic.CLL.Basic
 public import Cslib.Logics.LinearLogic.CLL.CutElimination

Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
+Authors: Fabrizio Montesi, Haoxuan Yin
 -/
 
 module
@@ -14,21 +14,23 @@ public import Cslib.Foundations.Syntax.HasSubstitution
 
 /-! # λ-calculus
 
-The untyped λ-calculus.
+The untyped λ-calculus, with a named representation of variables.
 
 ## References
 
 * [H. Barendregt, *Introduction to Lambda Calculus*][Barendregt1984]
+* Definition of α-equivalence [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with
+Variable Binding*][Gabbay2002]
 
 -/
 
 namespace Cslib
 
 universe u
 
-variable {Var : Type u}
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
 
-namespace LambdaCalculus.Named
+namespace LambdaCalculus.Named.Untyped
 
 /-- Syntax of terms. -/
 inductive Term (Var : Type u) : Type u where
@@ -37,52 +39,71 @@ inductive Term (Var : Type u) : Type u where
   | app (m n : Term Var)
 deriving DecidableEq
 
+namespace Term
+
 /-- Free variables. -/
-def Term.fv [DecidableEq Var] : Term Var → Finset Var
+def fv : Term Var → Finset Var
   | var x => {x}
-  | abs x m => m.fv.erase x
+  | abs x m => m.fv \ {x}
   | app m n => m.fv ∪ n.fv
 
 /-- Bound variables. -/
-def Term.bv [DecidableEq Var] : Term Var → Finset Var
+def bv : Term Var → Finset Var
   | var _ => ∅
-  | abs x m => m.bv ∪ {x} -- Could also be `insert x m.bv`
+  | abs x m => m.bv ∪ {x}
   | app m n => m.bv ∪ n.bv
 
 /-- Variable names (free and bound) in a term. -/
-def Term.vars [DecidableEq Var] (m : Term Var) : Finset Var :=
-  m.fv ∪ m.bv
+def vars : Term Var → Finset Var
+  | var x => {x}
+  | abs x m => m.vars ∪ {x}
+  | app m n => m.vars ∪ n.vars
 
-/-- Capture-avoiding substitution, as an inference system. -/
-inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop where
-  | varHit : (var x).Subst x r r
-  | varMiss : x ≠ y → (var y).Subst x r (var y)
-  | absShadow : (abs x m).Subst x r (abs x m)
-  | absIn : x ≠ y → y ∉ r.fv → m.Subst x r m' → (abs y m).Subst x r (abs y m')
-  | app : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n')
-
-/-- Renaming, or variable substitution. `m.rename x y` renames `x` into `y` in `m`. -/
-def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var :=
+/-- Variable renaming, applying to both free and bound variables.
+    `m.rename x y` changes all occurrences of `x` into `y` in `m`. -/
+def rename (m : Term Var) (x y : Var) : Term Var :=
   match m with
-  | var z => if z = x then (var y) else (var z)
-  | abs z m' =>
-    if z = x then
-      -- Shadowing
-      abs z m'
-    else
-      abs z (m'.rename x y)
+  | var z => var (if z = x then y else z)
+  | abs z m' => abs (if z = x then y else z) (m'.rename x y)
   | app n1 n2 => app (n1.rename x y) (n2.rename x y)
 
+omit [HasFresh Var] in
 /-- Renaming preserves size. -/
 @[simp]
-theorem Term.rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] :
-  sizeOf (m.rename x y) = sizeOf m := by
+theorem rename_eq_sizeOf {m : Term Var} {x y : Var} : sizeOf (m.rename x y) = sizeOf m := by
   induction m <;> aesop (add simp [Term.rename])
 
+/-- α-equivalence. -/
+inductive AlphaEquiv : Term Var → Term Var → Prop where
+  | var {x} : AlphaEquiv (var x) (var x)
+  | abs {y x1 x2 m1 m2} : y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} →
+    AlphaEquiv (m1.rename x1 y) (m2.rename x2 y) → AlphaEquiv (abs x1 m1) (abs x2 m2)
+  | app {m1 n1 m2 n2} : AlphaEquiv m1 n1 → AlphaEquiv m2 n2 → AlphaEquiv (app m1 m2) (app n1 n2)
+
+/-- Instance for the notation `m =α n`. -/
+instance instHasAlphaEquivTerm : HasAlphaEquiv (Term Var) where
+  AlphaEquiv := AlphaEquiv
+
+omit [HasFresh Var] in
+/-- Allow grind to recognise the notation of α-equivalence. -/
+@[grind ←]
+theorem AlphaEquiv_def (m n : Term Var) : AlphaEquiv m n ↔ m =α n := by
+  rfl
+
+/-- Capture-avoiding substitution, as an inference system. -/
+inductive Subst : Term Var → Var → Term Var → Term Var → Prop where
+  | varHit {x r} : (var x).Subst x r r
+  | varMiss {x y r} : y ≠ x → (var y).Subst x r (var y)
+  | absShadow {x m r} : (abs x m).Subst x r (abs x m)
+  | absIn {x y m r m'} : y ∉ r.fv ∪ {x} → m.Subst x r m' → (abs y m).Subst x r (abs y m')
+  | app {m n x r m' n'} : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n')
+  | alpha {m m' r r' n n' x} : m =α m' → r =α r' → n =α n' → Subst m x r n → m'.Subst x r' n'
+
 /-- Capture-avoiding substitution. `m.subst x r` replaces the free occurrences of variable `x`
 in `m` with `r`. -/
-def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) :
-  Term Var :=
+@[grind, simp]
+def subst (m : Term Var) (x : Var) (r : Term Var) :
+    Term Var :=
   match m with
   | var y => if y = x then r else var y
   | abs y m' =>
@@ -91,25 +112,21 @@ def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Te
     else if y ∉ r.fv then
       abs y (m'.subst x r)
     else
-      let z := HasFresh.fresh (m'.vars ∪ r.vars ∪ {x})
+      let z := HasFresh.fresh (m'.vars ∪ r.vars ∪ {x, y})
       abs z ((m'.rename y z).subst x r)
   | app m1 m2 => app (m1.subst x r) (m2.subst x r)
 termination_by m
-decreasing_by all_goals grind [rename.eq_sizeOf, abs.sizeOf_spec, app.sizeOf_spec]
+decreasing_by all_goals grind [rename_eq_sizeOf, abs.sizeOf_spec, app.sizeOf_spec]
 
 /-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
-instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
+instance instHasSubstitutionTerm :
     HasSubstitution (Term Var) Var (Term Var) where
-  subst := Term.subst
+  subst := subst
 
--- TODO
--- theorem Term.subst_comm
---   [DecidableEq Var] [HasFresh Var]
---   {m : Term Var} {x : Var} {n1 : Term Var} {y : Var} {n2 : Term Var} :
---   (m[x := n1])[y := n2] = (m[y := n2])[x := n1] := by
---   induction m
---   -- case var z =>
---   sorry
+/-- Allow grind to recognise the notation of substitution. -/
+@[grind ←]
+theorem subst_def (m r : Term Var) (x : Var) : m.subst x r = m[x := r] := by
+  rfl
 
 /-- Contexts. -/
 inductive Context (Var : Type u) : Type u where
@@ -127,39 +144,12 @@ def Context.fill (c : Context Var) (m : Term Var) : Term Var :=
   | appL c n => Term.app (c.fill m) n
   | appR n c => Term.app n (c.fill m)
 
-/-- Any `Term` can be obtained by filling a `Context` with a variable. This proves that `Context`
-completely captures the syntax of terms. -/
-theorem Context.complete (m : Term Var) :
-    ∃ (c : Context Var) (x : Var), m = (c.fill (Term.var x)) := by
-  induction m with
-  | var x => exists hole, x
-  | abs x n ih =>
-    obtain ⟨c', y, ih⟩ := ih
-    exists Context.abs x c', y
-    rw [ih, fill]
-  | app n₁ n₂ ih₁ ih₂ =>
-    obtain ⟨c₁, x₁, ih₁⟩ := ih₁
-    exists Context.appL c₁ n₂, x₁
-    rw [ih₁, fill]
-
-open Term
-
-/-- α-equivalence. -/
-inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where
--- The α-axiom
-| ax {m : Term Var} {x y : Var} :
-  y ∉ m.fv → AlphaEquiv (abs x m) (abs y (m.rename x y))
--- Equivalence relation rules
-| refl : AlphaEquiv m m
-| symm : AlphaEquiv m n → AlphaEquiv n m
-| trans : AlphaEquiv m1 m2 → AlphaEquiv m2 m3 → AlphaEquiv m1 m3
--- Context closure
-| ctx {c : Context Var} {m n : Term Var} : AlphaEquiv m n → AlphaEquiv (c.fill m) (c.fill n)
-
-/-- Instance for the notation `m =α n`. -/
-instance instHasAlphaEquivTerm [DecidableEq Var] : HasAlphaEquiv (Term Var) where
-  AlphaEquiv := Term.AlphaEquiv
+def Context.vars : Context Var → Finset Var
+  | hole => ∅
+  | abs x c => c.vars ∪ {x}
+  | appL c m => c.vars ∪ m.vars
+  | appR m c => m.vars ∪ c.vars
 
-end LambdaCalculus.Named
+end LambdaCalculus.Named.Untyped.Term
 
 end Cslib