feat: LambdaCalculus.LocallyNameless.Coc

Cslib/Foundations/Syntax/HasBetaEquiv.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Init
+
+public section
+
+namespace Cslib
+
+/-- Typeclass for the β-equivalence notation `x =β y`. -/
+class HasBetaEquiv (α : Type u) where
+  /-- β-equivalence relation for type α. -/
+  BetaEquiv : α → α → Prop
+
+@[inherit_doc]
+notation m:max " =β " n:max => HasBetaEquiv.BetaEquiv m n
+
+end Cslib

Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
+
+@[expose] public section
+
+/-! # Calculus of Constructions
+
+The Calculus of Constructions
+
+## References
+
+* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+
+-/
+
+namespace Cslib
+
+universe u
+
+namespace LambdaCalculus.LocallyNameless.Coc
+
+/-- Syntax of locally nameless terms, with free variables over `Var`. -/
+inductive Term (Var : Type u) : Type u
+  /-- Bound term variables using a de-Bruijn index. -/
+  | bvar : ℕ → Term Var
+  /-- Free term variables. -/
+  | fvar : Var → Term Var
+  /-- Function application. -/
+  | app : Term Var → Term Var → Term Var
+  /-- Lambda abstraction. -/
+  | abs : Term Var → Term Var → Term Var
+  /-- Pi type. -/
+  | pi : Term Var → Term Var → Term Var
+  /-- Type universe. -/
+  | type : ℕ → Term Var
+deriving DecidableEq
+
+/-- Free variables. -/
+@[scoped grind =]
+def Term.fv [DecidableEq Var] : Term Var → Finset Var
+  | .bvar _ => ∅
+  | .fvar z => {z}
+  | .app f a => f.fv ∪ a.fv
+  | .abs t b => t.fv ∪ b.fv
+  | .pi t b => t.fv ∪ b.fv
+  | .type _ => ∅
+
+abbrev Env (Var : Type u) := Context Var (Term Var)
+
+end LambdaCalculus.LocallyNameless.Coc
+
+end Cslib

Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Syntax.HasSubstitution
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.Basic
+
+@[expose] public section
+
+/-! # Calculus of Constructions
+
+The Calculus of Constructions
+
+## References
+
+* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+
+-/
+
+set_option linter.unusedDecidableInType false
+
+namespace Cslib
+
+universe u
+
+namespace LambdaCalculus.LocallyNameless.Coc
+
+namespace Term
+
+/-- Variable opening of the ith bound variable. -/
+@[scoped grind =]
+def openRec (i : ℕ) (s : Term Var) : Term Var → Term Var
+  | .bvar y => if i = y then s else (bvar y)
+  | .fvar x => fvar x
+  | .app f a => .app (openRec i s f) (openRec i s a)
+  | .abs σ t₁ => abs (openRec i s σ) (openRec (i + 1) s t₁)
+  | .pi σ t₁ => .pi (openRec i s σ) (openRec (i + 1) s t₁)
+  | .type s => .type s
+
+/-- Variable opening of the closest binding. -/
+@[scoped grind =]
+def open' (s : Term Var) (t : Term Var) : Term Var := openRec 0 t s
+
+@[inherit_doc]
+scoped infixr:80 " ^ᵗ " => open'
+
+@[inherit_doc]
+scoped notation:68 γ "⟦" X " ↝ " δ "⟧"=> openRec X δ γ
+
+/--
+Capture-avoiding substitution.
+`m.subst x r` replaces the free occurrences of variable `x` in `m` with `r`.
+-/
+@[scoped grind =]
+def subst [DecidableEq Var] (m : Term Var) (x : Var) (r : Term Var) : Term Var :=
+  match m with
+  | .bvar n => .bvar n
+  | .fvar z => if z = x then r else .fvar z
+  | .app f a => .app (f.subst x r) (a.subst x r)
+  | .abs t b => .abs (t.subst x r) (b.subst x r)
+  | .pi t b => .pi (t.subst x r) (b.subst x r)
+  | .type s => .type s
+
+/-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
+instance instHasSubstitutionTerm [DecidableEq Var] :
+    HasSubstitution (Term Var) Var (Term Var) where
+  subst := Term.subst
+
+@[scoped grind _=_]
+lemma subst_def [DecidableEq Var] :
+    Term.subst (m : Term Var) (x : Var) (r : Term Var) = m[x := r] := rfl
+
+/-- Substitution of a free variable not present in a term leaves it unchanged. -/
+lemma subst_fresh [DecidableEq Var] {γ : Term Var}
+    (nmem : X ∉ γ.fv) (δ : Term Var) : γ = γ[X := δ] := by
+  induction γ <;> grind
+
+/-- An opening appearing in both sides of an equality of terms can be removed. -/
+lemma openRec_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ = t⟦y ↝ s₁⟧⟦x ↝ s₂⟧) :
+    t = t⟦x ↝ s₂⟧ := by
+  induction t generalizing x y <;> grind
+
+/-- Locally closed terms. -/
+inductive LC : Term Var → Prop
+  | var : LC (.fvar x)
+  | app : LC t₁ → LC t₂ → LC (app t₁ t₂)
+  | abs (L : Finset Var) : t₁.LC → (∀ x ∉ L, LC (t₂ ^ᵗ fvar x)) → LC (abs t₁ t₂)
+  | pi (L : Finset Var) : t₁.LC → (∀ x ∉ L, LC (t₂ ^ᵗ fvar x)) → LC (pi t₁ t₂)
+  | type : LC (.type _)
+
+attribute [scoped grind .] LC.var LC.app LC.type
+
+/-- Predicate for being a locally closed body of an abstraction. -/
+@[scoped grind =]
+def body (t : Term Var) := ∃ L : Finset Var, ∀ x ∉ L, LC (t ^ᵗ fvar x)
+
+/-- A locally closed term is unchanged by opening. -/
+lemma openRec_lc [DecidableEq Var] [HasFresh Var] {σ τ : Term Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ := by
+  induction lc generalizing X with
+  | abs | pi => grind [fresh_exists <| free_union Var, openRec_neq_eq]
+  | _ => grind
+
+/-- Substitution of a locally closed type distributes with opening. -/
+lemma openRec_subst [DecidableEq Var] [HasFresh Var] {δ : Term Var}
+    (Y : ℕ) (t₁ t₂ : Term Var) (lc : δ.LC) (X : Var) :
+    (t₁⟦Y ↝ t₂⟧)[X := δ] = t₁[X := δ]⟦Y ↝ t₂[X := δ]⟧ := by
+  induction t₁ generalizing Y <;> grind [openRec_lc]
+
+/-- A locally closed term remains locally closed after substitution. -/
+lemma subst_lc [DecidableEq Var] [HasFresh Var] {t₁ t₂ : Term Var}
+    (t₁_lc : t₁.LC) (t₂_lc : t₂.LC) (X : Var) : t₁[X := t₂].LC := by
+  induction t₁_lc with
+  | abs => grind [LC.abs (free_union Var), openRec_subst]
+  | pi => grind [LC.pi (free_union Var), openRec_subst]
+  | _ => grind [openRec_subst]
+
+end Term
+
+end LambdaCalculus.LocallyNameless.Coc
+
+end Cslib

Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean

@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Syntax.HasAlphaEquiv
+public import Cslib.Foundations.Syntax.HasBetaEquiv
+public import Cslib.Foundations.Syntax.HasSubstitution
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.Opening
+
+@[expose] public section
+
+/-! # Calculus of Constructions
+
+The Calculus of Constructions
+
+## References
+
+* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+
+-/
+
+namespace Cslib
+
+universe u
+
+namespace LambdaCalculus.LocallyNameless.Coc
+
+open Term
+
+/-- β-reduction. -/
+inductive BetaEquiv : Term Var → Term Var → Prop
+  /-- β-redex: `(λ A. B) N ⟶ B ^ᵗ N`. -/
+  | red : (abs A B).LC → N.LC → BetaEquiv (.app (.abs A B) N) (B ^ᵗ N)
+  /-- Congruence in the function position of an application. -/
+  | app₁ : t₂.LC → BetaEquiv t₁ t₁' → BetaEquiv (.app t₁ t₂) (.app t₁' t₂)
+  /-- Congruence in the argument position of an application. -/
+  | app₂ : t₁.LC → BetaEquiv t₂ t₂' → BetaEquiv (.app t₁ t₂) (.app t₁ t₂')
+  /-- Congruence in the type annotation of an abstraction. -/
+  | abs₁ : t₂.body → BetaEquiv t₁ t₁' → BetaEquiv (.abs t₁ t₂) (.abs t₁' t₂)
+  /-- Congruence in the body of an abstraction. -/
+  | abs₂ (ρ : Finset Var) :
+      t₁.LC →
+      (∀ x ∉ ρ, BetaEquiv (t₂ ^ᵗ .fvar x) (t₂' ^ᵗ .fvar x)) →
+      BetaEquiv (.abs t₁ t₂) (.abs t₁ t₂')
+  /-- Congruence in the domain of a pi type. -/
+  | pi₁ : t₂.body → BetaEquiv t₁ t₁' → BetaEquiv (.pi t₁ t₂) (.pi t₁' t₂)
+  /-- Congruence in the codomain of a pi type. -/
+  | pi₂ (ρ : Finset Var) :
+      t₁.LC →
+      (∀ x ∉ ρ, BetaEquiv (t₂ ^ᵗ .fvar x) (t₂' ^ᵗ .fvar x)) →
+      BetaEquiv (.pi t₁ t₂) (.pi t₁ t₂')
+
+instance instHasBetaEquivTerm : HasBetaEquiv (Term Var) where
+  BetaEquiv := BetaEquiv
+
+
+variable [DecidableEq Var]
+
+namespace Term
+
+/-- Well-formedness of terms. -/
+inductive Wf : Env Var → Term Var → Prop
+  | var : ⟨x, _⟩ ∈ Γ → Wf Γ (fvar x)
+  | app : Wf Γ f → Wf Γ a → Wf Γ (app f a)
+  | abs (L : Finset Var) :
+      Wf Γ σ →
+      (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
+      Wf Γ (abs σ τ)
+  | pi (L : Finset Var) :
+      Wf Γ σ →
+      (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
+      Wf Γ (pi σ τ)
+  | type : Wf Γ (type _)
+
+end Term
+
+mutual
+
+/-- An environment is well-formed if it binds each variable exactly once to a well-formed type. -/
+inductive Env.Wf : Env Var → Prop
+  | nil : Env.Wf {}
+  | cons : Env.Wf Γ → Typing Γ τ (.type i) → x ∉ Γ.dom → Env.Wf ({⟨x, τ⟩} ∪ Γ)
+
+/-- Typing judgement -/
+inductive Typing : Env Var → Term Var → Term Var → Prop
+  /-- Variable lookup in Γ -/
+  | var : Γ.Wf → ⟨x, A⟩ ∈ Γ → Typing Γ (.fvar x) A
+  /-- Function application -/
+  | app : Typing Γ M (.pi A B) → Typing Γ N A → Typing Γ (.app M N) (B ^ᵗ N)
+  /-- Lambda abstraction -/
+  | abs (ρ : Finset Var) :
+      Typing Γ A K →
+      (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (N ^ᵗ .fvar x) (B ^ᵗ .fvar x)) →
+      Typing Γ (.abs A N) (.pi A B)
+  /-- Pi type -/
+  | pi (ρ : Finset Var) :
+      Typing Γ A (.type k) →
+      (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (B ^ᵗ .fvar x) (.type i)) →
+      (i = k ∨ i = 0) →
+      Typing Γ (.pi A B) (.type i)
+  /-- Type universe -/
+  | type : Typing Γ (.type s) (.type (s + 1))
+  /-- β-conversion -/
+  | conv : Typing Γ M A → A =β B → Typing Γ B (.type i) → Typing Γ M B
+
+end
+
+end LambdaCalculus.LocallyNameless.Coc
+
+end Cslib

references.bib

@@ -28,6 +28,20 @@ @book{Baader1998
 address = {USA}
 }
 
+@article{Coquand1996,
+title = {An algorithm for type-checking dependent types},
+journal = {Science of Computer Programming},
+volume = {26},
+number = {1},
+pages = {167-177},
+year = {1996},
+issn = {0167-6423},
+doi = {https://doi.org/10.1016/0167-6423(95)00021-6},
+url = {https://www.sciencedirect.com/science/article/pii/0167642395000216},
+author = {Thierry Coquand},
+abstract = {We present a simple type-checker for a language with dependent types and let expressions, with a simple proof of correctness.}
+}
+
 @inproceedings{Danielsson2008,
 author = {Danielsson, Nils Anders},
 title = {Lightweight semiformal time complexity analysis for purely functional data structures},