A comprehensive programming language metatheory library for Lean 4, providing formally verified proofs of fundamental results in rewriting theory and type systems.
Metatheory formalizes core results from programming language theory:
- Generic Rewriting Framework: Abstract rewriting systems with multiple confluence proof techniques
- Decreasing Diagrams: Non-terminating confluence example and parameterized family
- Lambda Calculus: Church-Rosser theorem via parallel reduction (Takahashi's method), βη-confluence via Hindley-Rosen, call-by-value reduction
- Combinatory Logic: Confluence of SK-combinators, derived combinators (I, B, C, W) with identity proofs
- Simply Typed Lambda Calculus: Subject reduction and strong normalization (Tait's method)
- Extended STLC: Products, sums, and unit type with progress and strong normalization
- STLC with Booleans: Conditional reduction with subject reduction, progress, confluence, and CBV determinism
- System F (Polymorphic Lambda Calculus): Subject reduction with type substitution
- Term/String Rewriting: Confluence via Newman's lemma and critical pair analysis
- TRS Proof Comparison: Diamond vs Newman confluence for a tiny deterministic TRS
| Feature | Benefit |
|---|---|
| Multiple proof techniques | Learn different approaches to confluence (Diamond, Newman, Hindley-Rosen) |
| Layered architecture | Generic framework instantiated by specific systems |
| De Bruijn indices | Capture-avoiding substitution without alpha-equivalence |
| Mathlib integration | Uses Mathlib for standard lemmas; core theorems axiom-free |
| Axiom/placeholder free | No axiom/constant declarations and no sorry/admit |
| Extensively documented | Docstrings, references, and proof explanations |
- Lean 4 (version 4.24.0 or compatible)
- Lake (included with Lean)
- Mathlib (automatically fetched by Lake)
git clone https://github.com/Arthur742Ramos/Metatheory.git
cd Metatheory
lake buildOptional strict check (placeholders + axioms/constants):
powershell -ExecutionPolicy Bypass -File scripts/check.ps1All modules must remain sorry-free and axiom-free, including new extensions.
Add to your lakefile.toml:
[[require]]
name = "Metatheory"
git = "https://github.com/Arthur742Ramos/Metatheory.git"
rev = "main"import Metatheoryimport Metatheory.Lambda.Term
import Metatheory.Lambda.Confluence
open Metatheory.Lambda
open Term
-- Define terms using de Bruijn indices
-- λx. λy. x y is lam (lam (app (var 1) (var 0)))
def example1 : Term := ƛ (ƛ (var 1 @ var 0))
-- The identity combinator: λx. x
def I : Term := ƛ (var 0)
-- Use the Church-Rosser theorem
example {M N₁ N₂ : Term} (h1 : M →* N₁) (h2 : M →* N₂) :
∃ P, (N₁ →* P) ∧ (N₂ →* P) :=
confluence h1 h2import Metatheory.Rewriting.Basic
import Metatheory.Rewriting.Diamond
open Rewriting
-- Use the generic framework for any relation
example {α : Type} {r : α → α → Prop} (h : Diamond r) : Confluent r :=
confluent_of_diamond himport Metatheory.STLC.Typing
import Metatheory.STLC.Normalization
open Metatheory.STLC
-- Well-typed terms are strongly normalizing
example {Γ : Context} {M : Term} {A : Ty} (h : HasType Γ M A) : SN M :=
strong_normalization himport Metatheory.STLCext.Typing
import Metatheory.STLCext.Normalization
open Metatheory.STLCext
-- Progress: well-typed closed terms are values or can step
example {M : Term} {A : Ty} (h : HasType [] M A) : IsValue M ∨ ∃ N, M ⟶ N :=
progress h
-- Strong normalization for extended STLC
example {Γ : Context} {M : Term} {A : Ty} (h : HasType Γ M A) : SN M :=
strong_normalization himport Metatheory.STLCextBool.CBV
open Metatheory.STLCextBool
example {M N₁ N₂ : Term} (h1 : CBVStep M N₁) (h2 : CBVStep M N₂) : N₁ = N₂ :=
CBVStep.deterministic h1 h2import Metatheory.SystemF.Typing
import Metatheory.SystemF.SubjectReduction
open Metatheory.SystemF
-- System F types use de Bruijn indices for type variables
-- ∀α. α → α is Ty.all (Ty.tvar 0 ⇒ Ty.tvar 0)
-- Subject reduction: types preserved under reduction
example {Γ : Context} {M N : Term} {τ : Ty}
(hM : Γ ⊢ M : τ) (hstep : M.Step N) : Γ ⊢ N : τ :=
subject_reduction hM hstep
-- Progress for closed terms
example {M : Term} {τ : Ty} (h : ⊢ M : τ) : M.IsValue ∨ ∃ N, M.Step N :=
progress h| Theorem | Statement | File |
|---|---|---|
confluent_of_diamond |
Diamond r → Confluent r | Rewriting/Diamond.lean |
confluent_of_terminating_localConfluent |
Terminating r → LocalConfluent r → Confluent r | Rewriting/Newman.lean |
confluent_union |
Confluent r → Confluent s → Commute r s → Confluent (Union r s) | Rewriting/HindleyRosen.lean |
confluent_of_locallyDecreasing |
WellFounded lt → LocallyDecreasing r lt → Confluent (LabeledUnion r) | Rewriting/DecreasingDiagrams.lean |
church_rosser_of_locallyDecreasing |
WellFounded lt → LocallyDecreasing r lt → Metatheory (LabeledUnion r) | Rewriting/DecreasingDiagrams.lean |
hasNormalForm_of_terminating |
Terminating r → ∀ a, HasNormalForm r a | Rewriting/Basic.lean |
| existsUnique_normalForm_of_terminating_confluent | Terminating r → Confluent r → ∀ a, ∃ n, a →* n ∧ NF n ∧ (∀ n', ...) | Rewriting/Basic.lean |
| Theorem | Statement | File |
|---|---|---|
confluence |
M →* N₁ → M →* N₂ → ∃ P, N₁ →* P ∧ N₂ →* P | Lambda/Confluence.lean |
parRed_diamond |
Diamond ParRed | Lambda/Diamond.lean |
parRed_complete |
M ⇒ N → N ⇒ complete M | Lambda/Complete.lean |
beta_eta_confluent |
Confluent BetaEtaStep | Lambda/Eta.lean |
beta_eta_diamond |
β a b → η a c → ∃ d, η* b d ∧ β* c d | Lambda/Eta.lean |
eta_confluent |
Confluent EtaStep | Lambda/Eta.lean |
CBVStep.deterministic |
M →cbv N₁ → M →cbv N₂ → N₁ = N₂ | Lambda/CBV.lean |
progress_trichotomy |
IsValue M ∨ (∃ N, M →cbv N) ∨ IsStuck M | Lambda/CBV.lean |
| Theorem | Statement | File |
|---|---|---|
confluent |
Confluent WeakStep | CL/Confluence.lean |
I_identity |
(I ⬝ x) →* x | CL/Reduction.lean |
K_identity |
(K ⬝ x ⬝ y) →* x | CL/Reduction.lean |
S_identity |
(S ⬝ x ⬝ y ⬝ z) →* ((x ⬝ z) ⬝ (y ⬝ z)) | CL/Reduction.lean |
B_identity |
(B ⬝ f ⬝ g ⬝ x) →* (f ⬝ (g ⬝ x)) | CL/Reduction.lean |
C_identity |
(C ⬝ x ⬝ y ⬝ z) →* ((x ⬝ z) ⬝ y) | CL/Reduction.lean |
W_identity |
(W ⬝ x ⬝ y) →* ((x ⬝ y) ⬝ y) | CL/Reduction.lean |
| Theorem | Statement | File |
|---|---|---|
subject_reduction |
HasType Γ M A → BetaStep M N → HasType Γ N A | STLC/Typing.lean |
strong_normalization |
HasType Γ M A → SN M | STLC/Normalization.lean |
| Theorem | Statement | File |
|---|---|---|
subject_reduction |
HasType Γ M A → M ⟶ N → HasType Γ N A | STLCext/Typing.lean |
progress |
HasType [] M A → IsValue M ∨ ∃ N, M ⟶ N | STLCext/Typing.lean |
strong_normalization |
HasType Γ M A → SN M | STLCext/Normalization.lean |
| Theorem | Statement | File |
|---|---|---|
subject_reduction |
HasType Γ M A → M ⟶ N → HasType Γ N A | STLCextBool/Typing.lean |
progress |
[] ⊢ M : A → IsValue M ∨ ∃ N, M ⟶ N | STLCextBool/Typing.lean |
confluence |
M ⟶* N₁ → M ⟶* N₂ → ∃ P, N₁ ⟶* P ∧ N₂ ⟶* P | STLCextBool/Confluence.lean |
cbv_deterministic |
Deterministic CBVStep | STLCextBool/CBV.lean |
cbv_confluent |
Confluent CBVStep | STLCextBool/CBV.lean |
strong_normalization |
HasType Γ M A → SN (erase M) | STLCextBool/Normalization.lean |
| Theorem | Statement | File |
|---|---|---|
confluence_via_diamond |
Confluent TinyStep | TRS/DiamondComparison.lean |
confluence_via_newman |
Confluent TinyStep | TRS/DiamondComparison.lean |
| Theorem | Statement | File |
|---|---|---|
subject_reduction |
(Γ ⊢ M : τ) → M.Step N → (Γ ⊢ N : τ) | SystemF/SubjectReduction.lean |
substitution_typing |
(A :: Γ ⊢ M : B) → (Γ ⊢ N : A) → (Γ ⊢ M[N] : B) | SystemF/SubjectReduction.lean |
type_substitution_typing |
(shiftContext Γ ⊢ M : τ) → WF k σ → (Γ ⊢ M[σ] : τ[σ]) | SystemF/SubjectReduction.lean |
progress |
(⊢ M : τ) → IsValue M ∨ ∃ N, M.Step N | SystemF/Typing.lean |
confluence |
M →ₛ* N₁ → M →ₛ* N₂ → ∃ P, N₁ →ₛ* P ∧ N₂ →ₛ* P | SystemF/Confluence.lean |
parRed_diamond |
Diamond ParRed | SystemF/Diamond.lean |
strongStep_confluent |
Confluent StrongStep | SystemF/Confluence.lean |
strong_normalization |
(Γ ⊢ M : τ) → SN M | SystemF/StrongNormalization.lean |
Metatheory/
├── Metatheory.lean # Main entry point
├── Metrics.lean # Project statistics and theorem summary
│
├── Rewriting/ # Layer 0: Generic ARS Framework
│ ├── Basic.lean # Star, Plus, Joinable, Diamond, Confluent
│ ├── Diamond.lean # Diamond property → Confluence
│ ├── Newman.lean # Newman's lemma
│ ├── HindleyRosen.lean # Union of commuting confluent relations
│ ├── DecreasingDiagrams.lean # van Oostrom's decreasing diagrams
│ ├── DecreasingDiagramsExample.lean # Non-terminating decreasing diagrams example
│ ├── DecreasingDiagramsFamily.lean # Parameterized non-terminating family
│ └── Compat.lean # Mathlib-style compatibility
│
├── Lambda/ # Layer 1a: Untyped Lambda Calculus
│ ├── Term.lean # De Bruijn terms, shift, substitution
│ ├── Beta.lean # β-reduction relation
│ ├── MultiStep.lean # Multi-step reduction (→*)
│ ├── Parallel.lean # Parallel reduction (⇒)
│ ├── Complete.lean # Complete development
│ ├── Diamond.lean # Diamond property for ⇒
│ ├── Confluence.lean # Church-Rosser theorem
│ ├── Eta.lean # η-reduction and βη-confluence
│ ├── Generic.lean # Bridge to generic framework
│ └── CBV.lean # Call-by-value reduction
│
├── CL/ # Layer 1b: Combinatory Logic
│ ├── Syntax.lean # S, K, I, B, C, W combinators
│ ├── Reduction.lean # Weak reduction + combinator identities
│ ├── Parallel.lean # Parallel reduction
│ └── Confluence.lean # Church-Rosser for CL
│
├── TRS/ # Layer 2a: Simple Term Rewriting
│ ├── Syntax.lean # Expressions (0, 1, +, *)
│ ├── Rules.lean # Rewrite rules
│ ├── Confluence.lean # Confluence via Newman
│ └── DiamondComparison.lean # Diamond vs Newman comparison
│
├── StringRewriting/ # Layer 2b: String Rewriting
│ ├── Syntax.lean # Alphabet and strings
│ ├── Rules.lean # aa→a, bb→b rules
│ └── Confluence.lean # Confluence via Newman + critical pairs
│
├── STLC/ # Layer 3: Simply Typed Lambda Calculus
│ ├── Types.lean # Ty ::= base n | A → B
│ ├── Terms.lean # Re-exports Lambda.Term
│ ├── Typing.lean # Γ ⊢ M : A, subject reduction
│ └── Normalization.lean # Strong normalization (Tait's method)
│
├── STLCext/ # Layer 4: Extended STLC with Products, Sums, Unit
│ ├── Types.lean # Ty ::= base n | A → B | A × B | A + B | unit
│ ├── Terms.lean # De Bruijn terms: pair, fst, snd, inl, inr, case, unit
│ ├── Reduction.lean # Beta + product/sum reduction rules
│ ├── Typing.lean # Typing, subject reduction, progress
│ └── Normalization.lean # Strong normalization (logical relations)
│
├── STLCextBool/ # Layer 4b: STLC with booleans and conditionals
│ ├── Types.lean # Ty ::= base n | A → B | bool
│ ├── Terms.lean # De Bruijn terms with true/false/ite
│ ├── Reduction.lean # Beta + if-true/if-false reduction rules
│ ├── CBV.lean # Call-by-value reduction (deterministic)
│ ├── Parallel.lean # Parallel reduction (diamond property tool)
│ ├── Complete.lean # Complete development for parallel reduction
│ ├── Confluence.lean # Church-Rosser theorem
│ ├── Typing.lean # Typing, subject reduction, progress
│ └── Normalization.lean # Strong normalization via erasure
│
└── SystemF/ # Layer 5: System F (Polymorphic Lambda Calculus)
├── Types.lean # Ty ::= tvar n | τ → σ | ∀α.τ (de Bruijn)
├── Terms.lean # Terms with type abstraction/application
├── Typing.lean # Polymorphic typing, progress
├── SubjectReduction.lean # Type preservation under reduction
├── StrongReduction.lean # Full (strong) β-reduction relation
├── Parallel.lean # Parallel reduction for System F
├── Complete.lean # Complete development
├── Diamond.lean # Diamond property for parallel reduction
├── Confluence.lean # Church-Rosser theorem for System F
└── StrongNormalization.lean # Strong normalization (Girard/Tait method)
Used for: Lambda Calculus, Combinatory Logic, Tiny TRS (comparison)
The key insight is that single-step reduction doesn't have the diamond property, but parallel reduction does:
M
/ \
⇒ ⇒ Parallel reduction: contract any subset of redexes
/ \
N₁ N₂
\ /
⇒ ⇒
\ /
P P = complete(M) contracts ALL redexes
Key definitions:
ParRed M N: M parallel-reduces to N (any subset of redexes)complete M: Contracts all redexes simultaneouslyparRed_complete: Any parallel reduction reaches the complete development
Used for: βη-Confluence
When two confluent relations commute, their union is confluent:
Confluent β + Confluent η + Commute(β, η) → Confluent (β ∪ η)
Key lemmas for βη:
beta_eta_diamond: β and η single-step divergences can be joinedeta_beta_seq_swap: Sequential η;β can be reordered to β*;η*commute_beta_eta_stars: Star relations β* and η* commutebetaeta_decompose: Any βη* path decomposes into β* followed by η*
Used for: TRS, String Rewriting, η-reduction, Tiny TRS (comparison)
For terminating systems, local confluence implies global confluence:
Terminating + LocalConfluent → Confluent
Strategy:
- Prove termination via a well-founded measure (size, length)
- Prove local confluence (one-step divergences join)
- Apply Newman's lemma
Used for: Strong Normalization of STLC
Define a "reducibility" predicate by induction on types:
def Reducible : Ty → Term → Prop
| base _, M => SN M
| A → B, M => ∀ N, Reducible A N → Reducible B (M @ N)Key properties (CR1-CR3):
- CR1: Reducible terms are SN
- CR2: Reducibility is closed under reduction
- CR3: Neutral terms with reducible reducts are reducible
Fundamental Lemma: Well-typed terms are reducible under reducible substitutions.
Variables are represented by natural numbers indicating the number of binders between the variable and its binding λ:
λx. λy. x y → λ. λ. (var 1) (var 0)
│ │ │ │ │
│ │ └──────────────┼────────┘ bound by inner λ
│ └────────────────┘ bound by outer λ
└─ binds x
Advantages:
- No α-equivalence needed (terms equal up to renaming are identical)
- Substitution is capture-avoiding by construction
inductive Star (r : α → α → Prop) : α → α → Prop where
| refl : Star r a a
| tail : Star r a b → r b c → Star r a c a
/ \
* *
/ \
b c
\ /
* *
\ /
d
A relation r is confluent if whenever a →* b and a →* c, there exists d with b →* d and c →* d.
-- Reflexive-transitive closure
inductive Star (r : α → α → Prop) : α → α → Prop
-- Joinability
def Joinable (r : α → α → Prop) (a b : α) : Prop :=
∃ c, Star r a c ∧ Star r b c
-- Diamond property
def Diamond (r : α → α → Prop) : Prop :=
∀ a b c, r a b → r a c → ∃ d, r b d ∧ r c d
-- Confluence
def Confluent (r : α → α → Prop) : Prop :=
∀ a b c, Star r a b → Star r a c → Joinable r b c
-- Termination (well-foundedness)
def Terminating (r : α → α → Prop) : Prop :=
∀ a, Acc (fun x y => r y x) a-- Terms
inductive Term : Type where
| var : Nat → Term
| app : Term → Term → Term
| lam : Term → Term
-- Shifting (adjusts free variables)
def shift (d : Int) (c : Nat) : Term → Term
-- Substitution
def subst (j : Nat) (N : Term) : Term → Term
-- Notation: M[N] = subst 0 N M
notation M "[" N "]" => subst0 N M
-- β-reduction
inductive BetaStep : Term → Term → Prop where
| beta : BetaStep (app (lam M) N) (M[N])
| appL : BetaStep M M' → BetaStep (app M N) (app M' N)
| appR : BetaStep N N' → BetaStep (app M N) (app M N')
| lam : BetaStep M M' → BetaStep (lam M) (lam M')
-- Call-by-value reduction (CBV)
def IsValue : Term → Prop
| lam _ => True
| _ => False
inductive CBVStep : Term → Term → Prop where
| beta : IsValue V → CBVStep (app (lam M) V) (M[V])
| appL : CBVStep M M' → CBVStep (app M N) (app M' N)
| appR : IsValue V → CBVStep N N' → CBVStep (app V N) (app V N')-- Terms: S, K combinators and application
inductive Term : Type where
| S : Term
| K : Term
| app : Term → Term → Term
-- Derived combinators
def I : Term := S ⬝ K ⬝ K -- Identity: I x →* x
def B : Term := S ⬝ (K ⬝ S) ⬝ K -- Composition: B f g x →* f (g x)
def C : Term := S ⬝ (S ⬝ (K ⬝ B) ⬝ S) ⬝ (K ⬝ K) -- Flip: C x y z →* x z y
def W : Term := S ⬝ S ⬝ (S ⬝ K) -- Duplicate: W x y →* x y y
-- Weak reduction
inductive WeakStep : Term → Term → Prop where
| k_red : WeakStep (K ⬝ M ⬝ N) M
| s_red : WeakStep (S ⬝ M ⬝ N ⬝ P) ((M ⬝ P) ⬝ (N ⬝ P))
| appL : WeakStep M M' → WeakStep (M ⬝ N) (M' ⬝ N)
| appR : WeakStep N N' → WeakStep (M ⬝ N) (M ⬝ N')-- Simple types
inductive Ty : Type where
| base : Nat → Ty
| arr : Ty → Ty → Ty
-- Typing judgment
inductive HasType : Context → Term → Ty → Prop where
| var : Γ.get? n = some A → HasType Γ (var n) A
| lam : HasType (A :: Γ) M B → HasType Γ (lam M) (A → B)
| app : HasType Γ M (A → B) → HasType Γ N A → HasType Γ (app M N) B
-- Strong normalization
def SN (M : Term) : Prop := Acc (fun a b => BetaStep b a) M-- Types with products, sums, and unit
inductive Ty where
| base : Nat → Ty -- Base type
| arr : Ty → Ty → Ty -- A → B
| prod : Ty → Ty → Ty -- A × B
| sum : Ty → Ty → Ty -- A + B
| unit : Ty -- Unit type
-- Terms with pairs, projections, injections, case, and unit
inductive Term where
| var : Nat → Term -- Variable
| lam : Term → Term -- λ.M
| app : Term → Term → Term -- M N
| pair : Term → Term → Term -- (M, N)
| fst : Term → Term -- π₁ M
| snd : Term → Term -- π₂ M
| inl : Term → Term -- inl M
| inr : Term → Term -- inr M
| case : Term → Term → Term → Term -- case M of inl → N₁ | inr → N₂
| unit : Term -- Unit value ()
-- Values
inductive IsValue : Term → Prop where
| lam : IsValue (lam M)
| pair : IsValue M → IsValue N → IsValue (pair M N)
| inl : IsValue M → IsValue (inl M)
| inr : IsValue M → IsValue (inr M)
| unit : IsValue unit-
Takahashi, M. (1995). "Parallel Reductions in λ-Calculus". Information and Computation, 118(1), 120-127.
- The parallel reduction technique for Church-Rosser
-
Newman, M.H.A. (1942). "On Theories with a Combinatorial Definition of 'Equivalence'". Annals of Mathematics, 43(2), 223-243.
- Newman's lemma: termination + local confluence → confluence
-
van Oostrom, V. (1994). "Confluence for Abstract and Higher-Order Rewriting". PhD thesis, Vrije Universiteit Amsterdam.
- Decreasing diagrams technique
-
Tait, W.W. (1967). "Intensional Interpretations of Functionals of Finite Type I". Journal of Symbolic Logic, 32(2), 198-212.
- Logical relations method for strong normalization
-
Hindley, J.R. (1969). "An Abstract Church-Rosser Theorem". Journal of Symbolic Logic, 34(4), 545-560.
- Hindley-Rosen lemma for union of relations
-
Barendregt, H.P. (1984). The Lambda Calculus: Its Syntax and Semantics. North-Holland.
- Comprehensive reference for lambda calculus
-
Terese (2003). Term Rewriting Systems. Cambridge University Press.
- Standard reference for term rewriting theory
-
Girard, J.-Y., Lafont, Y., & Taylor, P. (1989). Proofs and Types. Cambridge University Press.
- Logical relations and normalization proofs
-
Pierce, B.C., et al. (2023). Software Foundations, Volume 2: Programming Language Foundations.
- Formal verification of PL metatheory in Coq
- Software Foundations (Coq)
- CoLoR - Certified termination and confluence (Coq)
- Nominal Isabelle - Lambda calculus with names
- PLFA - Programming Language Foundations in Agda
Contributions are welcome! Please feel free to submit issues and pull requests.
- No
sorry: All theorems must be fully proven (current count: 0 sorries) - Documentation: Add docstrings to public definitions
- References: Cite sources for non-trivial lemmas
- Style: Follow existing code conventions
lake build # Compiles and type-checks all proofsMIT License - see LICENSE for details.
This project was developed with assistance from Claude Code, Anthropic's AI assistant for software engineering.