A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
Arthur Ramos, Anjolina Oliveira, Ruy de Queiroz, Tiago de Veras
TL;DR
This work introduces Metatheory, a modular Lean 4 framework for proving confluence and strong normalization across multiple lambda-calculus variants, including STLC with products and sums. It implements three core meta-theorems (Diamond Property, Newman's Lemma, Hindley-Rosen) and applies them to six case studies, with fully mechanized proofs and complete de Bruijn infrastructure. A major achievement is the STLC extension with products and sums, for which a sophisticated reducibility proof is developed, including a complex Case construct analysis. The library comprises 10,367 lines of Lean 4 code, 497 theorems, and zero axioms, underscoring Lean 4’s viability for rigorous metatheory and offering a comprehensive resource for future polymorphic and polymorphic-type extensions.
Abstract
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond property, Newmans lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. All theorems are fully mechanized with zero axioms or sorry statements. We provide complete proofs of de Bruijn substitution infrastructure and demonstrate strong normalization via logical relations. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4.