Metatheory

A comprehensive programming language metatheory library for Lean 4, now spanning 130+ Lean files and 58K+ lines of mechanized proofs and metatheoretic case studies.

Overview

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, critical pair analysis, and first-order TRS completion (KBO/LPO)
TRS Proof Comparison: Diamond vs Newman confluence for a tiny deterministic TRS
Extended Formalizations: 78 standalone modules covering type systems, semantics, compilation, effects, logic, macros, and automation

Project Scale

Tracked Lean files: 155 (git ls-files '*.lean')
Tracked Lean LOC: 58,126
Lean files under Metatheory/: 153
Standalone modules under Metatheory/*.lean: 78
Top-level dependency model: no Mathlib requirement in lakefile.toml; many standalone modules are self-contained

Why Metatheory?

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
Dependency-light design	Top-level build has no Mathlib requirement; many modules are self-contained
Axiom/placeholder free	No `axiom`/`constant` declarations and no `sorry`/`admit`
Extensively documented	Docstrings, references, and proof explanations

Installation

Prerequisites

Lean 4 (version 4.24.0 or compatible)
Lake (included with Lean)

Building

git clone https://github.com/Arthur742Ramos/Metatheory.git
cd Metatheory
lake build

Optional strict check (placeholders + axioms/constants):

powershell -ExecutionPolicy Bypass -File scripts/check.ps1

No Sorries / Axioms

All modules must remain sorry-free and axiom-free, including new extensions.

Using as a Dependency

Add to your lakefile.toml:

[[require]]
name = "Metatheory"
git = "https://github.com/Arthur742Ramos/Metatheory.git"
rev = "main"

Quick Start

Import the Library

import Metatheory

Lambda Calculus Example

import 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 h2

Generic Rewriting Framework

import 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 h

First-Order TRS (Completion + Orderings)

import Metatheory.TRS.FirstOrder.Ordering
import Metatheory.TRS.FirstOrder.Confluence

open Metatheory.TRS.FirstOrder

-- LPO-based termination criterion
example {sig : Signature} {rules : RuleSet sig} (prec : Precedence sig)
    (hord : ∀ r, rules r → StableLPOplus prec r.rhs r.lhs) :
    Terminating rules :=
  terminating_of_lpo (sig := sig) (prec := prec) hord

Simply Typed Lambda Calculus

import 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 h

Extended STLC with Products, Sums, and Unit

import 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 h

STLC with Booleans (CBV Determinism)

import Metatheory.STLCextBool.CBV

open Metatheory.STLCextBool

example {M N₁ N₂ : Term} (h1 : CBVStep M N₁) (h2 : CBVStep M N₂) : N₁ = N₂ :=
  CBVStep.deterministic h1 h2

System F (Polymorphic Lambda Calculus)

import 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

Extended Formalizations (Standalone Modules)

In addition to the layered core directories (Rewriting/, Lambda/, CL/, TRS/, StringRewriting/, STLC/, STLCext/, STLCextBool/, SystemF/), the project includes 78 standalone modules at Metatheory/*.lean.

Type systems and typing disciplines

AbstractionSafety.lean — Safety-oriented typing relation with abstraction-preservation lemmas.
AffineTypes.lean — Affine ownership typing inspired by Rust-style single-use resources.
Bidirectional.lean — Bidirectional typing (synthesis/checking) for concise typing derivations.
ContractTypes.lean — Contract-annotated typing with interface-level guarantees.
DependentPattern.lean — Dependently typed pattern matching and indexed elimination structure.
EffectSystems.lean — Type-and-effect judgments with explicit effect labels.
Gradual.lean — Gradual typing with dynamic type and consistency relations.
GradedTypeTheory.lean — Graded modality/type usage tracking (0/1/ω-style discipline).
InformationFlow.lean — Security typing over a lattice of confidentiality levels.
Intersection.lean — Intersection type operators and associated metatheoretic lemmas.
LinearTypes.lean — Linear usage-sensitive typing and structural control.
PolymorphismVariants.lean — Comparative formalization of polymorphism design variants.
QuantitativeTypes.lean — Quantitative type usage accounting for resource-aware typing.
RecursiveTypes.lean — Recursive type constructors with unfold/fold metatheory.
Refinement.lean — Refinement-annotated base types with predicate-indexed judgments.
RefinementTypes.lean — Predicate subtyping and refinement typing rules.
RowPoly.lean — Row polymorphism for extensible typing contexts/signatures.
SecrecyTypes.lean — Secrecy/security labels integrated into typing judgments.
SessionTypes.lean — Binary session type protocols for typed communication.
SizedTypes.lean — Size indices for termination/productivity-aware typing.
TemporalTypes.lean — Temporal type structure over trace-indexed behavior.
TypeClasses.lean — Type-class declarations and resolution-oriented typing scaffolding.
TypeInference.lean — Constraint-based type inference for monomorphic fragments.
TypeInhabitance.lean — Constructive inhabitation results (type-to-term witness style).
TypePreservation.lean — Standalone substitution and preservation theorems.
UniversePolymorphism.lean — Universe-level expressions and polymorphic universe handling.

Semantics, normalization, and equivalence

AbstractInterpretation.lean — Abstract interpretation skeletons with soundness-oriented structure.
AbstractMachines.lean — CEK/Krivine/SECD-style machine encodings and transitions.
CallByPushValue.lean — Call-by-push-value syntax, translation, and metatheory lemmas.
CategorySemantics.lean — Categorical semantics building blocks for typed languages.
Coinduction.lean — Coinductive streams/processes and bisimulation-style reasoning.
DomainTheory.lean — Domain/path-style order-theoretic lemmas for denotational settings.
Erasure.lean — Erasure translation preserving key typing/evaluation structure.
GameSemantics.lean — Game-semantic traces/plays with compositional properties.
LogicalRelations.lean — Logical-relations framework for normalization/equivalence proofs.
ModalTypeTheory.lean — Modal type-theoretic syntax and proof obligations.
NormByEval.lean — Normalization by evaluation (NbE) core constructions.
Normalization.lean — Generic normalization-oriented lemmas and structures.
ObservationalEquality.lean — Observational/contextual equality formulations.
ParallelReduction.lean — Parallel reduction relation and confluence-support infrastructure.
Parametricity.lean — Relational parametricity setup for polymorphic calculi.
ProgramEquivalence.lean — Program equivalence relations and congruence toolkit.
Realizability.lean — Realizability semantics over combinatory-style structures.
Termination.lean — Well-founded termination analysis and accessibility lemmas.

Compilation and transformation pipeline

ANFRegAlloc.lean — ANF conversion plus register-allocation metatheory.
CPS.lean — CPS-focused typed syntax and proof support.
CPSTransformation.lean — Source-to-CPS transformation and simulation lemmas.
CompilerOptimizations.lean — Verified optimization rewrites for a small compiler core.
ElaborationAlgorithm.lean — Surface-to-core elaboration algorithm components.
StackMachineCompilation.lean — Compilation to stack machine code with correctness statements.
StackMachines.lean — Stack machine semantics and execution lemmas.
SyntaxTransformers.lean — Generic syntax transformer combinators and properties.

Effects, concurrency, and resource management

AlgebraicEffects.lean — Algebraic effects with handlers and effect-row-style structure.
EffectHandlers.lean — Typed handler interfaces and operational effect handling.
ConcurrencyTypes.lean — Typing-oriented concurrency process/rewrite structure.
MemoryManagement.lean — Memory-aware terms/types and management invariants.
SessionProc.lean — Session-typed process calculus fragments and safety scaffolding.

Logic, proof theory, and structural systems

Focusing.lean — Focused proof search structure with polarized connectives.
LinearLogic.lean — Linear logic formulae and proof-theoretic infrastructure.
ModalLogic.lean — Modal proof system lemmas and formula structure.
OTT.lean — OTT-style syntax/typing support definitions.
ProofIrrelevance.lean — Proof irrelevance principles and consequences.
ProofNets.lean — Proof-net representation for linear logic fragments.
ResourceLogic.lean — Resource-sensitive logic connectives and judgments.
SeparationLogic.lean — Separation logic structures and composition lemmas.
Sequent.lean — Sequent calculus style rewriting/judgment relations.
Substructural.lean — Substructural logic framework controlling structural rules.

Macros, metaprogramming, and proof automation

HigherOrderUnification.lean — Higher-order unification syntax and solving scaffolding.
HygienicMacros.lean — Hygienic macro expansion and scope-safety metatheory.
InductionRecursion.lean — Induction-recursion universes and code interpretations.
MacroSystems.lean — Macro system core with scoped marks and expansion relations.
MacroTyping.lean — Macro typing/staging rules for typed expansion.
TacticFrameworks.lean — Lightweight tactic framework formalization hooks.

Project scaffolding and integration modules

Basic.lean — Minimal sandbox module used for local sanity checks.
Confluence.lean — Standalone confluence/closure helper development.
DeBruijn.lean — De Bruijn-indexed substitution/renaming infrastructure.
Metrics.lean — Project metrics and theorem inventory checks.
MetatheoryGrandTour.lean — Grand tour module connecting major components.

Key Theorems

Generic Rewriting Framework

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 |

Lambda Calculus

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`

Combinatory Logic

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`

Simply Typed Lambda Calculus

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`

Extended STLC (Products and Sums)

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`

STLC with Booleans

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`

TRS Proof Comparison

Theorem	Statement	File
`confluence_via_diamond`	Confluent TinyStep	`TRS/DiamondComparison.lean`
`confluence_via_newman`	Confluent TinyStep	`TRS/DiamondComparison.lean`

First-Order TRS (Completion + Orderings)

Theorem	Statement	File
`terminating_of_kbo`	Weight ordering orients all rules → Terminating	`TRS/FirstOrder/Ordering.lean`
`terminating_of_lpo`	Stable LPO orients all rules → Terminating	`TRS/FirstOrder/Ordering.lean`
`confluent_of_knuthBendixComplete`	KB certificate → Confluent	`TRS/FirstOrder/Confluence.lean`

System F (Polymorphic Lambda Calculus)

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`

Project Structure

Metatheory/
├── Metatheory.lean              # Main entry point
├── Metrics.lean                 # Project statistics and theorem summary
├── *.lean (78 standalone modules) # Extended formalizations; see section above
│
├── 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
│   └── FirstOrder/              # First-order TRS, completion, KBO/LPO

│
├── 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)

Proof Techniques

1. Diamond Property (Takahashi's 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 simultaneously
parRed_complete: Any parallel reduction reaches the complete development

2. Hindley-Rosen Lemma

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 joined
eta_beta_seq_swap: Sequential η;β can be reordered to β*;η*
commute_beta_eta_stars: Star relations β* and η* commute
betaeta_decompose: Any βη* path decomposes into β* followed by η*

3. Newman's Lemma

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

4. Logical Relations (Tait's Method)

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.

Mathematical Background

De Bruijn Indices

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

Reflexive-Transitive Closure

inductive Star (r : α → α → Prop) : α → α → Prop where
  | refl : Star r a a
  | tail : Star r a b → r b c → Star r a c

Confluence

A relation r is confluent if whenever a →* b and a →* c, there exists d with b →* d and c →* d.

API Reference

Core Definitions

-- 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

Lambda Calculus

-- 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')

Combinatory Logic

-- 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')

STLC

-- 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

Extended STLC

-- 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

References

Papers

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

Books

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

Related Formalizations

Software Foundations (Coq)
CoLoR - Certified termination and confluence (Coq)
Nominal Isabelle - Lambda calculus with names
PLFA - Programming Language Foundations in Agda

Contributing

Contributions are welcome! Please feel free to submit issues and pull requests.

Development Guidelines

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

Running Tests

lake build  # Compiles and type-checks all proofs

License

MIT License - see LICENSE for details.

Acknowledgments

This project was developed with assistance from Claude Code, Anthropic's AI assistant for software engineering.

Name		Name	Last commit message	Last commit date
Latest commit History 80 Commits
.claude		.claude
.github		.github
Metatheory		Metatheory
docs		docs
paper		paper
scripts		scripts
.gitignore		.gitignore
AGENTS.md		AGENTS.md
CLAUDE.md		CLAUDE.md
LICENSE		LICENSE
Main.lean		Main.lean
Metatheory.lean		Metatheory.lean
README.md		README.md
lake-manifest.json		lake-manifest.json
lakefile.toml		lakefile.toml
lean-toolchain		lean-toolchain

License

Arthur742Ramos/Metatheory

Folders and files

Latest commit

History

Repository files navigation

Metatheory

Overview

Project Scale

Why Metatheory?

Installation

Prerequisites

Building

No Sorries / Axioms

Using as a Dependency

Quick Start

Import the Library

Lambda Calculus Example

Generic Rewriting Framework

First-Order TRS (Completion + Orderings)

Simply Typed Lambda Calculus

Extended STLC with Products, Sums, and Unit

STLC with Booleans (CBV Determinism)

System F (Polymorphic Lambda Calculus)

Extended Formalizations (Standalone Modules)

Type systems and typing disciplines

Semantics, normalization, and equivalence

Compilation and transformation pipeline

Effects, concurrency, and resource management

Logic, proof theory, and structural systems

Macros, metaprogramming, and proof automation

Project scaffolding and integration modules

Key Theorems

Generic Rewriting Framework

Lambda Calculus

Combinatory Logic

Simply Typed Lambda Calculus

Extended STLC (Products and Sums)

STLC with Booleans

TRS Proof Comparison

First-Order TRS (Completion + Orderings)

System F (Polymorphic Lambda Calculus)

Project Structure

Proof Techniques

1. Diamond Property (Takahashi's Method)

2. Hindley-Rosen Lemma

3. Newman's Lemma

4. Logical Relations (Tait's Method)

Mathematical Background

De Bruijn Indices

Reflexive-Transitive Closure

Confluence

API Reference

Core Definitions

Lambda Calculus

Combinatory Logic

STLC

Extended STLC

References

Papers

Books

Related Formalizations

Contributing

Development Guidelines

Running Tests

License

Acknowledgments

About

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Contributors 4

Uh oh!

Languages

Packages