Locally nameless STLC

Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean

@@ -0,0 +1,164 @@
+/-
+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.LocallyNameless.Stlc.Context
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
+
+/-! # λ-calculus
+
+The simply typed λ-calculus, with a locally nameless representation of syntax.
+
+## 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 v
+
+variable {Var : Type u} {Base : Type v} [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Stlc
+
+/-- Types of the simply typed lambda calculus. -/
+inductive Ty (Base : Type v)
+  /-- A base type, from a typing context. -/
+  | base : Base → Ty Base
+  /-- A function type. -/
+  | arrow : Ty Base → Ty Base → Ty Base
+
+scoped infixr:70 " ⤳ " => Ty.arrow
+
+open Term Ty
+
+/-- An extrinsic typing derivation for locally nameless terms. -/
+@[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
+inductive Typing : Context Var (Ty Base) → Term Var → Ty Base → Prop
+  /-- Free variables, from a context judgement. -/
+  | var : Γ✓ → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
+  /-- Lambda abstraction. -/
+  | abs (L : Finset Var) : (∀ x ∉ L, Typing (⟨x,σ⟩ :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
+  /-- Function application. -/
+  | app : Typing Γ t (σ ⤳ τ) → Typing Γ t' σ → Typing Γ (app t t') τ
+
+scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ
+
+namespace Typing
+
+variable {Γ Δ Θ : Context Var (Ty Base)}
+
+omit [DecidableEq Var] in
+/-- Typing is preserved on permuting a context. -/
+theorem perm (ht : Γ ⊢ t ∶τ) (hperm : Γ.Perm Δ) : Δ ⊢ t ∶ τ := by 
+  revert Δ
+  induction ht <;> intros Δ p
+  case app => aesop
+  case var => 
+    have := @p.mem_iff
+    aesop
+  case abs ih => 
+    constructor
+    intros x mem
+    exact ih x mem (by aesop)
+
+/-- Weakening of a typing derivation with an appended context. -/
+lemma weaken_aux : 
+    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Θ ++ Δ)✓ → (Γ ++ Θ ++ Δ) ⊢ t ∶ τ := by
+  generalize eq : Γ ++ Δ = Γ_Δ
+  intros h
+  revert Γ Δ Θ
+  induction h <;> intros Γ Δ Θ eq ok_Γ_Θ_Δ
+  case var => aesop
+  case app => aesop
+  case abs σ Γ' τ t xs ext ih =>
+    apply Typing.abs (xs ∪ (Γ ++ Θ ++ Δ).dom)
+    intros x _
+    have h : ⟨x, σ⟩ :: Γ ++ Δ = ⟨x, σ⟩ :: Γ' := by aesop
+    refine @ih x (by aesop) _ _ Θ h ?_
+    simp only [HasWellFormed.wf]
+    aesop
+
+/-- Weakening of a typing derivation by an additional context. -/
+lemma weaken : Γ ⊢ t ∶ τ → (Γ ++ Δ)✓ → Γ ++ Δ ⊢ t ∶ τ := by
+  intros der ok
+  rw [←List.append_nil (Γ ++ Δ)] at *
+  exact weaken_aux (by simp_all) ok
+
+omit [DecidableEq Var] in
+/-- Typing derivations exist only for locally closed terms. -/
+lemma lc : Γ ⊢ t ∶ τ → t.LC := by
+  intros h
+  induction h <;> constructor
+  case abs ih => exact ih
+  all_goals aesop
+
+variable [HasFresh Var]
+
+open Term
+
+/-- Substitution for a context weakened by a single type between appended contexts. -/
+lemma subst_aux :
+    (Δ ++ ⟨x, σ⟩ :: Γ) ⊢ t ∶ τ →
+    Γ ⊢ s ∶ σ → 
+    (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
+  generalize  eq : Δ ++ ⟨x, σ⟩ :: Γ = Θ
+  intros h
+  revert Γ Δ
+  induction h <;> intros Γ Δ eq der
+  case app => aesop
+  case var x' τ ok mem => 
+    simp only [subst_fvar]
+    rw [←eq] at mem
+    rw [←eq] at ok
+    cases (Context.wf_perm (by aesop) ok : (⟨x, σ⟩ :: Δ ++ Γ)✓)
+    case cons ok_weak _ =>
+    observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
+    by_cases h : x = x' <;> simp only [h]
+    case neg => aesop
+    case pos nmem =>
+      subst h eq
+      have nmem_Γ : ∀ γ, ⟨x, γ⟩ ∉ Γ := by
+        intros γ _
+        exact nmem x (List.mem_keys.mpr ⟨γ, by aesop⟩) rfl
+      have nmem_Δ : ∀ γ, ⟨x, γ⟩ ∉ Δ := by
+        intros γ _
+        exact nmem x (List.mem_keys.mpr ⟨γ, by aesop⟩) rfl
+      have eq' : τ = σ := by
+        simp only [List.mem_append, List.mem_cons, Sigma.mk.injEq, heq_eq_eq] at mem
+        match mem with | _ => aesop
+      rw [eq']
+      refine (weaken der ?_).perm perm
+      exact Context.wf_perm (id (List.Perm.symm perm)) ok_weak
+  case abs σ Γ' t T2 xs ih' ih =>
+    apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
+    intros x _
+    rw [
+      subst_def, 
+      subst_open_var _ _ _ _ _ der.lc,
+      show ⟨x, σ⟩ :: (Δ ++ Γ) = (⟨x, σ⟩ :: Δ) ++ Γ by aesop
+      ]
+    apply ih 
+    all_goals aesop  
+
+/-- Substitution for a context weakened by a single type. -/
+lemma typing_subst_head : 
+    ⟨x, σ⟩ :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
+  intros weak der
+  rw [←List.nil_append Γ]
+  exact subst_aux weak der
+
+/-- Typing preservation for opening. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem preservation_open {xs : Finset Var} :
+  (∀ x ∉ xs, ⟨x, σ⟩ :: Γ ⊢ m ^ fvar x ∶ τ) → 
+  Γ ⊢ n ∶ σ → Γ ⊢ m ^ n ∶ τ
+  := by
+  intros mem der
+  have ⟨fresh, free⟩ := fresh_exists (xs ∪ m.fv)
+  rw [subst_intro fresh n m (by aesop) der.lc]
+  exact typing_subst_head (mem fresh (by aesop)) der

Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean

@@ -0,0 +1,57 @@
+/-
+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.LocallyNameless.Untyped.AesopRuleset
+import Cslib.Syntax.HasWellFormed
+import Mathlib.Data.Finset.Defs
+import Mathlib.Data.Finset.Dedup
+import Mathlib.Data.List.Sigma
+
+/-! # λ-calculus
+
+Contexts as pairs of free variables and types.
+
+-/
+
+universe u v
+
+variable {Var : Type u} {Ty : Type v} [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Stlc
+
+/-- A typing context is a list of free variables and corresponding types. -/
+abbrev Context (Var : Type u) (Ty : Type v) := List ((_ : Var) × Ty)
+
+namespace Context
+
+/-- The domain of a context is the finite set of free variables it uses. -/
+@[simp]
+def dom : Context Var Ty → Finset Var := List.toFinset ∘ List.keys
+
+/-- A well-formed context. -/
+abbrev Ok : Context Var Ty → Prop := List.NodupKeys
+
+instance : HasWellFormed (Context Var Ty) :=
+  ⟨Ok⟩
+
+variable {Γ Δ : Context Var Ty}
+
+/-- Context membership is preserved on permuting a context. -/
+theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} : 
+    x ∈ Γ.dom ↔ x ∈ Δ.dom := by
+  induction h <;> aesop
+
+omit [DecidableEq Var] in
+/-- Context well-formedness is preserved on permuting a context. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem wf_perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp
+
+omit [DecidableEq Var] in
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem wf_strengthen : (Δ ++ ⟨x, σ⟩ :: Γ)✓ → (Δ ++ Γ)✓ := by
+  intros ok
+  have sl : List.Sublist (Δ ++ Γ) (Δ ++ ⟨x, σ⟩ :: Γ) := by simp
+  exact List.NodupKeys.sublist sl ok

Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean

@@ -0,0 +1,92 @@
+/-
+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.LocallyNameless.Stlc.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
+
+/-! # λ-calculus
+
+Type safety of the simply typed λ-calculus, with a locally nameless representation of syntax.
+Theorems in this file are namespaced by their respective reductions.
+
+## 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 v
+
+namespace LambdaCalculus.LocallyNameless
+
+open Stlc Typing
+
+variable {Var : Type u} {Base : Type v} {R : Term Var → Term Var → Prop}
+
+def PreservesTyping (R : Term Var → Term Var → Prop) (Base : Type v) := 
+  ∀ {Γ t t'} {τ : Ty Base}, Γ ⊢ t ∶ τ → R t t' → Γ ⊢ t' ∶ τ
+
+/-- If a reduction preserves types, so does its reflexive transitive closure. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem redex_preservesTyping : 
+    PreservesTyping R Base → PreservesTyping (Relation.ReflTransGen R) Base := by
+  intros _ _ _ _ _ _ redex
+  induction redex <;> aesop
+
+open Relation in
+/-- Confluence preserves type preservation. -/
+theorem confluence_preservesTyping {τ : Ty Base} : 
+    Confluence R → PreservesTyping R Base → Γ ⊢ a ∶ τ → 
+    (ReflTransGen R) a b → (ReflTransGen R) a c →
+    ∃ d, (ReflTransGen R) b d ∧ (ReflTransGen R) c d ∧ Γ ⊢ d ∶ τ := by
+  intros con p der ab ac
+  have ⟨d, bd, cd⟩ := con ab ac
+  exact ⟨d, bd, cd, redex_preservesTyping p der (ab.trans bd)⟩
+
+variable [HasFresh Var] [DecidableEq Var] {Γ : Context Var (Ty Base)}
+
+namespace Term.FullBeta
+
+/-- Typing preservation for full beta reduction. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ := by
+  intros der
+  revert t'
+  induction der <;> intros t' step <;> cases step
+  case' abs.abs xs _ _ _ xs' _=> apply Typing.abs (xs ∪ xs')
+  case' app.beta der_l _ _ => cases der_l
+  all_goals aesop
+
+omit [HasFresh Var] [DecidableEq Var] in
+/-- A typed term either full beta reduces or is a value. -/
+theorem progress {t : Term Var} {τ : Ty Base} (ht : [] ⊢ t ∶τ) : t.Value ∨ ∃ t', t ⭢βᶠ t' := by
+  generalize eq : [] = Γ at ht
+  induction ht
+  case var => aesop
+  case abs xs mem ih =>
+    left
+    constructor
+    apply Term.LC.abs xs
+    intros _ mem'
+    exact (mem _ mem').lc
+  case app Γ M σ τ N der_l der_r ih_l ih_r => 
+    simp only [eq, forall_const] at *
+    right
+    cases ih_l
+    -- if the lhs is a value, beta reduce the application
+    next val =>
+      cases val
+      next M M_abs_lc => exact ⟨M ^ N, FullBeta.beta M_abs_lc der_r.lc⟩
+    -- otherwise, propogate the step to the lhs of the application
+    next step =>
+      obtain ⟨M', stepM⟩ := step
+      exact ⟨M'.app N, FullBeta.appR der_r.lc stepM⟩ 
+
+end LambdaCalculus.LocallyNameless.Term.FullBeta

Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean → Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Basic.lean

@@ -6,7 +6,7 @@ Authors: Chris Henson
 
 import Cslib.Data.HasFresh
 import Cslib.Syntax.HasSubstitution
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.AesopRuleset
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.AesopRuleset
 
 /-! # λ-calculus
 
@@ -26,9 +26,9 @@ variable {Var : Type u} [HasFresh Var] [DecidableEq Var]
 
 namespace LambdaCalculus.LocallyNameless
 
-/-- Syntax of locally nameless absbda terms, with free variables over `Var`. -/
+/-- Syntax of locally nameless lambda terms, with free variables over `Var`. -/
 inductive Term (Var : Type u)
-/-- Bound variables that appear under a absbda abstraction, using a de-Bruijn index. -/
+/-- Bound variables that appear under a lambda abstraction, using a de-Bruijn index. -/
 | bvar : ℕ → Term Var
 /-- Free variables. -/
 | fvar : Var → Term Var
@@ -143,3 +143,6 @@ 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)
+
+inductive Value : Term Var → Prop
+| abs (e : Term Var) : e.abs.LC → e.abs.Value

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

@@ -4,8 +4,8 @@ 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.LocallyNameless.Untyped.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
 import Cslib.Semantics.ReductionSystem.Basic
 
 /-! # β-reduction for the λ-calculus

Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean → Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean

@@ -4,9 +4,9 @@ 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.FullBeta
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 import Cslib.Data.Relation
 
 /-! # β-confluence for the λ-calculus -/

Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean → Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Properties.lean

@@ -4,7 +4,7 @@ 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.LocallyNameless.Untyped.Basic
 
 universe u
 

CslibTests/LambdaCalculus.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Computability.LambdaCalculus.Untyped.Named.Basic
+import Cslib.Computability.LambdaCalculus.Named.Untyped.Basic
 
 open LambdaCalculus.Named
 open LambdaCalculus.Named.Term