A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums cover

📄 Executive Summary

Modern software systems and programming languages depend heavily on rigorous mathematical guarantees, such as confluence (which ensures that computations yield consistent outcomes regardless of evaluation order) and strong normalization (which guarantees that program executions always terminate). While these foundational properties are critical for ensuring reliable software behavior and coherent type systems, mechanized proofs in modern proof assistants are notoriously challenging and labor-intensive to construct. Projects often rely on unproven assumptions or shortcuts to circumvent tedious structural mechanics, leaving lingering verification gaps.

The article demonstrates a comprehensive, modular verification framework named Metatheory in the Lean 4 proof assistant. The objective is to establish fully machine-checked proofs of confluence and strong normalization across diverse core programming formalisms—culminating in the simply typed lambda calculus extended with both product and sum data types—entirely from first principles without introducing unproven assumptions.

To accomplish this, the authors implemented three classical meta-theorems for confluence: the diamond property via parallel reduction, Newman's lemma for terminating systems, and the Hindley-Rosen lemma for combining commuting relations. They evaluated this generic framework across six distinct case studies, encompassing untyped lambda calculus, combinatory logic, term rewriting, string rewriting, standard simply typed lambda calculus, and its extension with products and sums. Strong normalization was formalized using Tait's logical relations method. Crucially, the authors fully proved all underlying variable shifting and substitution mechanics using index-based representations, including a generalized composition lemma spanning over 700 lines of code.

The framework achieved an end-to-end formalization totaling 10,367 lines of code across 497 theorems, containing zero unproven axioms or placeholders. The extended system with product and sum types proved to be the most demanding component, accounting for roughly 37% of the total codebase (3,828 lines and 155 theorems) due to the complexity of reasoning about case-analysis constructs. The evaluation confirms that the diamond property serves as an effective general-purpose technique for non-terminating systems, whereas Newman's lemma significantly streamlines proofs when termination is present. Furthermore, the work establishes that variable substitution infrastructure can be fully proved from scratch without sacrificing mathematical tractability.

These results provide high-assurance verification that eliminates risks associated with unverified assumptions in programming language theory. For organizations engineering verified compilers, domain-specific languages, and automated theorem provers, this work demonstrates that Lean 4 is a viable, robust ecosystem for mechanized foundations. Stakeholders can adopt the authors' publicly available, open-source library to accelerate language formalization efforts. As immediate next steps, future developments should focus on integrating these foundational formalisms with broader mathematical libraries and extending verification to more advanced features, such as parametric polymorphism.

📚 What to read before this

Principles of Programming Languages, Mike Grant et al. (2002). This text establishes the core operational semantics, variable substitution mechanics, and typing rules for functional calculi with products and sums that the source mechanizes from first principles.

📚 What to read after this

No sufficiently relevant recommendations were found.

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums

Arthur F. Ramos

^{1}

^{1}

Microsoft, Tampa, FL, USA [email protected]

Anjolina G. de Oliveira

^{2}

^{2}

Centro de Informática, Universidade Federal de Pernambuco, Recife, PE, Brazil {ago,ruy}@cin.ufpe.br

Ruy J. G. B. de Queiroz

^{2}

^{2}

Centro de Informática, Universidade Federal de Pernambuco, Recife, PE, Brazil {ago,ruy}@cin.ufpe.br

Tiago M. L. de Veras

^{3}

^{3}

Departamento de Matemática, Universidade Federal Rural de Pernambuco, Recife, PE, Brazil [email protected]

Abstract

We present Metatheory, a comprehensive library for programming language foundations in Lean 4, featuring a modular framework for proving confluence of abstract rewriting systems. The library implements three classical proof techniques---the diamond property via parallel reduction, Newman's lemma for terminating systems, and the Hindley-Rosen lemma for unions of relations---within a single generic framework that is instantiated across six case studies: untyped lambda calculus, combinatory logic, simple term rewriting, string rewriting, simply typed lambda calculus (STLC), and STLC extended with products and sums. All theorems are fully mechanized with zero axioms or sorry placeholders. The de Bruijn substitution infrastructure, often axiomatized in similar developments, is completely proved, including the notoriously tedious substitution composition lemma. We demonstrate strong normalization via logical relations for both STLC and its extension with products (

\times B

) and sums (

A + B

), with the latter requiring a careful treatment of the case elimination form in our Lean 4 formalization. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4.

1. Introduction

Confluence is a fundamental property of rewriting systems, guaranteeing that the order of reductions does not affect the final result. The Church-Rosser theorem for lambda calculus [1] established that

β\beta

-reduction is confluent, ensuring that every term has at most one normal form. This property is essential for programming language semantics: it guarantees that evaluation order does not change program meaning and that type systems are coherent.

Beyond confluence, strong normalization ensures that all reduction sequences terminate—a property that holds for well-typed terms in the simply typed lambda calculus. Together, confluence and normalization provide the foundation for reasoning about type-theoretic languages: they ensure that type checking is decidable and that types serve as meaningful specifications.

Despite decades of study, formalizing these results remains challenging. The standard confluence techniques—parallel reduction [2], Newman's lemma [3], decreasing diagrams [4]—have distinct proof patterns and preconditions. Strong normalization requires logical relations [5], involving subtle reasoning about term structure and reduction.

Moreover, the underlying infrastructure for lambda calculus with de Bruijn indices [6] requires numerous technical lemmas about shifting and substitution. These lemmas are notoriously tedious to prove and are often axiomatized [7] or avoided through named representations or locally nameless encodings. We prove all such lemmas completely.

Contributions. We present

METATHEORY{\mathchoice{\text{M{\scriptsize ETATHEORY}}}{\text{M{\scriptsize ETATHEORY}}}{\text{M{\scriptscriptstyle ETATHEORY}}}{\text{METATHEORY}}}

, a Lean 4 library that:

Provides a generic framework for abstract rewriting systems (ARS) with reusable definitions and three fully mechanized meta-theorems (Section 3);
Demonstrates three proof techniques for confluence—diamond property, Newman's lemma, and Hindley-Rosen—instantiated across multiple systems (Section 4);
Includes complete de Bruijn infrastructure with all substitution lemmas proved, including the $∼\sim$ 90-line proof of substitution composition (Section 4.1);
Provides strong normalization for STLC via Tait's method [5] with logical relations, fully mechanized (Section 5);
Extends to STLC with products and sums, requiring careful treatment of the case construct in reducibility proofs (Section 6);
Achieves zero axioms: all theorems across 10,367 lines of Lean 4 are complete proofs.

Why Lean 4? While formalizations exist in Coq [8] and Isabelle [9], Lean 4 [10] offers a modern type theory with excellent metaprogramming, fast compilation, and growing adoption. No comprehensive confluence framework previously existed for Lean 4.

2. Preliminaries: Abstract Rewriting Systems

An abstract rewriting system (ARS) is a pair

\rightarrow)

where

A

is a set and

→⊆A×A{\rightarrow} \subseteq A \times A

is a binary relation.

Definition: Key Properties

Joinable: $\downarrow b \iff \exists c.\, a \rightarrow^* c \land b \rightarrow^* c$
Diamond (= Locally Confluent): $b↓c\forall a,b,c.\, a \rightarrow b \land a \rightarrow c \implies b \downarrow c$
Confluent: $b↓c\forall a,b,c.\, a \rightarrow^* b \land a \rightarrow^* c \implies b \downarrow c$
Terminating: $→\rightarrow$ is well-founded (no infinite sequences)

Note: Our Diamond property coincides with local confluence as typically stated in Newman's lemma—both require that single-step divergence can be joined (in zero or more steps). This differs from the stricter "one-step diamond" where the join must also be in single steps.

In Lean 4:

inductive Star (r : a -> a -> Prop) : a -> a -> Prop where
  | refl : Star r a a
  | tail : Star r a b -> r b c -> Star r a c

def Diamond (r : a -> a -> Prop) : Prop :=
  forall a b c, r a b -> r a c -> Joinable r b c

def Confluent (r : a -> a -> Prop) : Prop :=
  forall a b c, Star r a b -> Star r a c -> Joinable r b c

3. Generic Framework

Our framework provides three meta-theorems for proving confluence.

3.1 Diamond Property Implies Confluence

Theorem: confluent_of_diamond

Confluent(r)\mathit{Diamond}(r) \implies \mathit{Confluent}(r)

The proof proceeds by induction on

\rightarrow^* b

, using the diamond property to "strip" one step at a time via a helper lemma diamond_strip.

3.2 Newman's Lemma

For terminating systems, local confluence suffices:

Theorem: Newman's Lemma

Termination and local confluence imply confluence.

The proof uses well-founded induction on the termination order.

3.3 Hindley-Rosen Lemma

When combining confluent relations that commute, their union is confluent [11]:

Theorem: Hindley-Rosen

r

and

s

are confluent and commute, then

\cup s

is confluent.

3.4 Technique Comparison

Table 1: Comparison of confluence proof techniques

Technique	Precondition	Proof Effort	Applicability
Diamond	None	Define parallel reduction	Non-terminating
Newman	Termination	Prove termination + LC	Terminating
Hindley-Rosen	Two confluent rels.	Prove commutation	Modular

4. Case Studies

We instantiate our framework across six systems.

4.1 Lambda Calculus via Diamond Property

The untyped

λ\lambda

-calculus [12] with de Bruijn indices [6] is our primary case study. Terms are:

\mathtt{var}(n) \mid M\, N \mid \lambda M

De Bruijn Infrastructure. In de Bruijn notation, variables are represented by natural numbers indicating how many binders to cross to reach the binding site. This eliminates

α\alpha

-equivalence but requires careful bookkeeping via shifting (adjusting indices when passing under binders) and substitution:

def shift (d : Int) (c : Nat) : Term -> Term
  | var n => var (if n < c then n else n + d)
  | app M N => app (shift d c M) (shift d c N)
  | lam M => lam (shift d (c + 1) M)

def subst (k : Nat) (N : Term) : Term -> Term
  | var n => if n < k then var n
             else if n = k then shift k 0 N
             else var (n - 1)
  | app M1 M2 => app (subst k N M1) (subst k N M2)
  | lam M => lam (subst (k + 1) (shift 1 0 N) M)

A major contribution is fully proving the substitution lemmas. The key lemmas are:

Theorem: Shifting Lemmas

$↑c0M=M\uparrow^0_c M = M$ (identity)
$↑cd1(↑cd2M)=↑cd1+d2M\uparrow^{d_1}_c (\uparrow^{d_2}_c M) = \uparrow^{d_1+d_2}_c M$ (composition)
$↑c1d1(↑c2d2M)=↑c2+d1d2(↑c1d1M)\uparrow^{d_1}_{c_1} (\uparrow^{d_2}_{c_2} M) = \uparrow^{d_2}_{c_2+d_1} (\uparrow^{d_1}_{c_1} M)$ when $c1≤c2c_1 \le c_2$ (commutation)

Theorem: Substitution Composition

Our proof (709 lines in Term.lean) uses a generalized lemma with a "level" parameter

ℓ\ell

tracking nesting depth under binders:

The base case

ℓ=0\ell = 0

gives the standard composition lemma; the general case handles the interaction with shifting under

λ\lambda

-binders.

Parallel Reduction. Following Takahashi [2], we define parallel reduction

\Rightarrow N

that contracts any subset of redexes simultaneously:

inductive ParRed : Term -> Term -> Prop where
  | var : ParRed (var n) (var n)
  | app : ParRed M M' -> ParRed N N' -> ParRed (app M N) (app M' N')
  | lam : ParRed M M' -> ParRed (lam M) (lam M')
  | beta : ParRed M M' -> ParRed N N' ->
           ParRed (app (lam M) N) (M'[N'])

The complete development

M^*

contracts all redexes:

def complete : Term -> Term
  | var n => var n
  | lam M => lam (complete M)
  | app (lam M) N => (complete M)[complete N]
  | app M N => app (complete M) (complete N)

Theorem: Takahashi's Method

\Rightarrow N \implies N \Rightarrow M^*

. Hence parallel reduction has the diamond property, and

β\beta

-reduction is confluent.

4.2 Combinatory Logic via Diamond Property

Combinatory logic uses combinators S and K instead of binding:

\mathbf{S} \mid \mathbf{K} \mid M\, N

with rules

y→x\mathbf{K}\, x\, y \rightarrow x

and

z)\mathbf{S}\, x\, y\, z \rightarrow x\, z\, (y\, z)

. The parallel reduction technique applies without substitution complexity (285 lines).

4.3 Term and String Rewriting via Newman's Lemma

For terminating systems, Newman's lemma provides a simpler path. We demonstrate with arithmetic expressions (

\mid 1 \mid e + e \mid e \times e

) and string rewriting over

{a, b\}^*

with idempotency rules

\rightarrow a

and

\rightarrow b

. Termination is proved via size/length measures; local confluence via critical pair analysis.

5. Simply Typed Lambda Calculus

We extend untyped

λ\lambda

-calculus with simple types:

\mathtt{base}(n) \mid A \to B

5.1 Typing and Subject Reduction

Typing contexts

Γ\Gamma

are lists of types, with

Γ(n)=A\Gamma(n) = A

meaning the

n

-th variable has type

A

. The typing judgment

Γ⊢M:A\Gamma \vdash M : A

is defined by the usual rules:

\dfrac{\Gamma(n) = A}{\Gamma \vdash \mathtt{var}(n) : A}\;{\scriptstyle\mathsf{Var}} \quad \dfrac{A :: \Gamma \vdash M : B}{\Gamma \vdash \lambda M : A \to B}\;{\scriptstyle\mathsf{Lam}} \quad \dfrac{\Gamma \vdash M : A \to B \;\; \Gamma \vdash N : A}{\Gamma \vdash M\, N : B}\;{\scriptstyle\mathsf{App}}

Theorem: subject_reduction

Γ⊢N:A\Gamma \vdash M : A \land M \rightarrow_\beta N \implies \Gamma \vdash N : A

The proof requires a substitution lemma: if

Γ⊢N:A\Gamma \vdash N : A

and

\Gamma \vdash M : B

, then

Γ⊢M[N]:B\Gamma \vdash M[N] : B

5.2 Strong Normalization via Logical Relations

We prove strong normalization using Tait's method [5]. The key is a reducibility predicate defined by induction on types:

def Reducible : Ty -> Term -> Prop
  | base _, M => SN M
  | arr A B, M => forall N, Reducible A N -> Reducible B (M N)

The definition for arrow types is the crucial insight: a function is reducible if applying it to any reducible argument yields a reducible result. This semantic definition enables induction on type structure.

Candidate Properties. Reducibility satisfies three key properties that Girard [13] calls the "candidat de réductibilité" conditions:

CR1 $SN(M)\mathit{Reducible}(A, M) \implies \mathit{SN}(M)$

Reducible terms are strongly normalizing.
CR2 $Reducible(A,N)\mathit{Reducible}(A, M) \land M \rightarrow N \implies \mathit{Reducible}(A, N)$

Reducibility is closed under reduction.
CR3 $Reducible(A,M)\mathit{Neutral}(M) \land (\forall N.\, M \rightarrow N \implies \mathit{Reducible}(A, N)) \implies \mathit{Reducible}(A, M)$

A neutral term is reducible if all its reducts are reducible.

Here,

Neutral(M)\mathit{Neutral}(M)

means

M

is not a redex—i.e., not of the form

N(\lambda M')\, N

. Variables and applications

Nx\, N

are neutral.

Fundamental Lemma. The main lemma states that well-typed terms are reducible under any reducible substitution:

Theorem: fundamental_lemma

Γ⊢M:A\Gamma \vdash M : A

and

σ\sigma

is a substitution such that

Reducible(Γ(i),σ(i))\mathit{Reducible}(\Gamma(i), \sigma(i))

for all

i

, then

Reducible(A,M[σ])\mathit{Reducible}(A, M[\sigma])

Theorem: strong_normalization

SN(M)\Gamma \vdash M : A \implies \mathit{SN}(M)

Proof: Apply the fundamental lemma with the identity substitution (variables are reducible by CR3), then extract SN by CR1.

6. Extended STLC with Products and Sums

A significant extension is STLC with product types (

\times B

) and sum types (

A + B

). This extension is standard in programming language theory but requires substantial additional machinery in the strong normalization proof. The STLCext module is our largest (3,828 lines, 155 theorems), reflecting this complexity.

6.1 Extended Types and Terms

Types are extended to:

\mathtt{base}(n) \mid A \to B \mid A \times B \mid A + B

Terms include pairs, projections, injections, and case analysis:

The new typing rules are standard:

\dfrac{\Gamma \vdash M : A \quad \Gamma \vdash N : B}{\Gamma \vdash (M, N) : A \times B}\;{\scriptstyle\mathsf{Pair}} \quad \dfrac{\Gamma \vdash M : A \times B}{\Gamma \vdash \mathtt{fst}\, M : A}\;{\scriptstyle\mathsf{Fst}} \quad \dfrac{\Gamma \vdash M : A \times B}{\Gamma \vdash \mathtt{snd}\, M : B}\;{\scriptstyle\mathsf{Snd}}

6.2 Reduction Rules

Beyond

β\beta

-reduction, we add:

Note that case analysis binds the injected value: the branches

N_1

and

N_2

have an additional free variable (index 0) representing the scrutinee value.

6.3 Reducibility for Products and Sums

The key challenge is extending the reducibility predicate. For products, we use a projection-based definition; for sums, we track what values the term may reduce to:

def Reducible : Ty -> Term -> Prop
  | base _, M => SN M
  | arr A B, M => forall N, Reducible A N -> Reducible B (M N)
  | prod A B, M => Reducible A (fst M) /\ Reducible B (snd M)
  | sum A B, M => SN M /\ (forall V, M ->* inl V -> Reducible A V)
                       /\ (forall V, M ->* inr V -> Reducible B V)

The product case says

M

is reducible at

\times B

iff both projections are reducible. This is well-defined because

fst\mathtt{fst}

and

snd\mathtt{snd}

are smaller terms in the structural sense.

The sum case requires: (1)

M

is SN; (2) if

M

reduces to

V\mathtt{inl}\, V

, then

V

is reducible at

A

; (3) similarly for

inr\mathtt{inr}

. This ensures that case analysis on

M

produces reducible results.

6.4 The Case Construct Challenge

The most complex proof is showing

N2\mathtt{case}\, M\, N_1\, N_2

is reducible. Unlike applications or projections, the case form has three subterms that can reduce independently, and its neutrality depends on

M

def IsNeutral : Term -> Prop
  | var _ => True
  | app M _ => not (isLam M)
  | fst M => not (isPair M)
  | snd M => not (isPair M)
  | case M _ _ => not (isInl M) /\ not (isInr M)
  | _ => False

case\mathtt{case}

is neutral only when its scrutinee is neither

inl\mathtt{inl}

nor

inr\mathtt{inr}

. This complicates CR3 arguments.

Theorem: reducible_case

Given:

$SN(M)\mathit{SN}(M)$ , $SN(N1)\mathit{SN}(N_1)$ , $SN(N2)\mathit{SN}(N_2)$
For all $V$ : if $\rightarrow^* \mathtt{inl}\, V$ and $Reducible(A,V)\mathit{Reducible}(A, V)$ , then $Reducible(C,N1[V])\mathit{Reducible}(C, N_1[V])$
Similarly for $inr\mathtt{inr}$ and $N_2$

Then

N2)\mathit{Reducible}(C, \mathtt{case}\, M\, N_1\, N_2)

holds.

The proof (337 lines) proceeds by case analysis on the result type

C

Base type. We must show

N2)\mathit{SN}(\mathtt{case}\, M\, N_1\, N_2)

. The proof uses triple nested induction on

SN(M)\mathit{SN}(M)

SN(N1)\mathit{SN}(N_1)

, and

SN(N2)\mathit{SN}(N_2)

, analyzing each possible reduction.

Arrow type. We must show reducibility at

C1→C2C_1 \to C_2

. The key:

P(\mathtt{case}\, M\, N_1\, N_2)\, P

is always neutral, regardless of whether

M

is an injection. The outermost constructor is application, whose head is case, not a

λ\lambda

. Thus CR3 applies directly.

Product type. Similarly,

N2)\mathtt{fst}\,(\mathtt{case}\, M\, N_1\, N_2)

and

N2)\mathtt{snd}\,(\mathtt{case}\, M\, N_1\, N_2)

are always neutral because their head is

case\mathtt{case}

, not a pair.

Sum type. We show SN (as for base type) plus track multi-step reductions. If

V\mathtt{case}\, M\, N_1\, N_2 \rightarrow^* \mathtt{inl}\, V

, this can only happen if

\rightarrow^* \mathtt{inl}\, W

for some

W

, making

VN_1[W] \rightarrow^* \mathtt{inl}\, V

. By hypothesis,

N_1[W]

is reducible, so

V

is reducible as required.

Theorem: strong_normalization for STLCext

SN(M)\Gamma \vdash M : A \implies \mathit{SN}(M)

for the extended system.

6.5 Progress

We also prove progress for closed well-typed terms:

Theorem: progress

M→N\varnothing \vdash M : A \implies \mathit{IsValue}(M) \lor \exists N.\, M \rightarrow N

Values include

λ\lambda

-abstractions, pairs of values, and injections of values. The proof analyzes the typing derivation and shows that non-value well-typed closed terms always have a redex.

7. Quantitative Summary

Table 2: Library statistics by module

Module	Lines	Theorems	Technique
Rewriting (generic)	1,301	45	—
Lambda calculus	1,498	89	Diamond property
Combinatory logic	584	42	Diamond property
Term rewriting	428	31	Newman's lemma
String rewriting	776	48	Newman's lemma
STLC	1,792	87	Logical relations
STLCext (products + sums)	3,828	155	Logical relations
Total	10,367	497	—

Table 2 summarizes the library. All 497 theorems are fully proved with zero sorry placeholders or axioms. The STLCext module is the largest, reflecting the complexity of strong normalization with products and sums.

8. Related Work

CoLoR. The Coq library on rewriting and termination [8] is the most comprehensive formalization of term rewriting in a proof assistant. It includes termination orderings, polynomial interpretations, and dependency pairs. Our work differs in language (Lean 4), scope (we focus on confluence techniques plus strong normalization rather than termination), and the inclusion of complete de Bruijn proofs without axiomatization.

Isabelle Formalizations. Nipkow [9] formalized multiple Church-Rosser proofs in Isabelle/HOL, comparing parallel reduction, residuals, and complete developments. Our parallel reduction approach follows similar lines. The Nominal Isabelle framework provides elegant binder handling but requires specialized infrastructure. We demonstrate that de Bruijn indices, while requiring more lemmas, can be completely formalized.

POPLmark Challenge. The POPLmark challenge [14] benchmarked different approaches to binding in mechanized metatheory. Solutions ranged from named representations to de Bruijn indices to locally nameless encodings. Aydemir et al. [7] popularized the locally nameless approach. Many POPLmark solutions axiomatized substitution lemmas; we prove all lemmas completely, demonstrating that full formalization is tractable.

Agda Formalizations. Various Agda developments formalize lambda calculus with de Bruijn indices, including strong normalization proofs for STLC. Our work differs in being a unified framework for multiple techniques and systems, culminating in the products-and-sums extension.

Software Foundations. The PLF volume of Software Foundations [15] includes strong normalization for STLC in Coq using logical relations. Our development extends to products and sums, which are not covered there, and demonstrates the additional complexity this introduces.

9. Conclusion

We presented

METATHEORY{\mathchoice{\text{M{\scriptsize ETATHEORY}}}{\text{M{\scriptsize ETATHEORY}}}{\text{M{\scriptscriptstyle ETATHEORY}}}{\text{METATHEORY}}}

, a modular confluence and normalization framework for Lean 4 featuring three proof techniques across six case studies, culminating in strong normalization for STLC extended with products and sums. Our fully mechanized development (10,367 LOC, 497 theorems, 0 axioms) demonstrates that de Bruijn infrastructure can be completely proved and that Lean 4 is viable for programming language metatheory.

Lessons Learned.

Technique selection matters: Diamond property works broadly; Newman's lemma is simpler when termination holds.
De Bruijn is tractable: With careful generalization, substitution lemmas are provable without axiomatization.
Sum types are subtle: The case construct requires careful strategies (wrapping in eliminators) for reducibility proofs.

Future Work. We plan to add decreasing diagrams, System F with parametric polymorphism, and integration with Lean 4's Mathlib.

Availability. The library is open-source at: https://github.com/arthuraa/metatheory

Appendix

A. De Bruijn Substitution Lemmas

We provide the complete list of de Bruijn substitution lemmas proved in our development. These lemmas are often axiomatized or omitted in formalizations; we prove all of them completely (709 lines total).

A.1 Shifting Lemmas

-- Identity: shifting by 0 does nothing
theorem shift_zero : shift 0 c M = M

-- Composition at same cutoff
theorem shift_shift : shift d1 c (shift d2 c M) = shift (d1 + d2) c M

-- Commutation at different cutoffs (when c1 <= c2)
theorem shift_shift_comm :
  shift d1 c1 (shift d2 c2 M) = shift d2 (c2 + d1) (shift d1 c1 M)

-- Special case: shifting by 1 twice
theorem shift_shift_succ :
  shift 1 (c + 1) (shift 1 c M) = shift 2 c M

A.2 Shift-Substitution Interaction

-- Key interaction lemma
theorem shift_subst :
  shift d c (subst k N M) =
    subst (k + d) (shift d c N) (shift d (c + 1) M)

-- Substitution after shift cancels
theorem subst_shift_cancel :
  subst k N (shift 1 k M) = M

A.3 Substitution Composition

The main substitution composition lemma and its generalization:

-- Generalized version with level parameter
theorem subst_subst_gen_full (l k j : Nat) (M N P : Term) :
  subst k (shift l 0 P)
    (subst (k + j + 1) (shift (k + l + 1) 0 N) M) =
  subst (k + j) (shift l 0 (subst j N P))
    (subst k (shift (l + 1) 0 P) M)

-- Standard composition (l = 0, k = 0, j = 0)
theorem subst_subst : (M[N])[P] = (subst 1 (shift 1 0 P) M)[N[P]]

B. CR Properties: Detailed Proofs

B.1 CR1: Reducible Implies SN

theorem cr1 (A : Ty) (M : Term) : Reducible A M -> SN M := by
  intro hRed
  induction A generalizing M with
  | base _ => exact hRed
  | arr A B ihA ihB =>
    -- Apply M to a reducible argument (var 0)
    have hVar : Reducible A (var 0) := var_reducible 0 A
    have hApp : Reducible B (app M (var 0)) := hRed (var 0) hVar
    have hSN_app : SN (app M (var 0)) := ihB _ hApp
    exact sn_of_sn_app_var hSN_app
  | prod A B ihA ihB =>
    have hFst, hSnd := hRed
    exact sn_of_sn_fst_snd (ihA _ hFst) (ihB _ hSnd)
  | sum A B _ _ => exact hRed.1

B.2 CR3: Neutral Terms

The CR3 property is most complex for STLCext. We show the key insight for arrow types:

-- When the result type is an arrow, we show app (case M N1 N2) P is reducible
-- Key: app (case ...) P is ALWAYS neutral, regardless of M
theorem reducible_case_arr :
  SN M -> SN N1 -> SN N2 ->
  (forall V, M ->* inl V -> Reducible A V -> Reducible (arr C1 C2) (N1[V])) ->
  (forall V, M ->* inr V -> Reducible B V -> Reducible (arr C1 C2) (N2[V])) ->
  Reducible (arr C1 C2) (case M N1 N2) := by
  intro hSN_M hSN_N1 hSN_N2 hInl hInr
  intro P hP_red
  -- Show: Reducible C2 (app (case M N1 N2) P)
  -- Key insight: app (case M N1 N2) P is ALWAYS neutral!
  -- Because: app has a case as its function, which is not a lambda
  apply cr3_neutral C2 (app (case M N1 N2) P)
  . -- Show all reducts are reducible (by nested induction)
    ...
  . -- Show app (case ...) P is neutral
    exact neutral_app_case M N1 N2 P

C. Full Typing Rules for STLCext

\dfrac{\Gamma(n) = A}{\Gamma \vdash \mathtt{var}(n) : A}\;{\scriptstyle\mathsf{Var}} \quad \dfrac{A :: \Gamma \vdash M : B}{\Gamma \vdash \lambda M : A \to B}\;{\scriptstyle\mathsf{Lam}} \quad \dfrac{\Gamma \vdash M : A \to B \quad \Gamma \vdash N : A}{\Gamma \vdash M\, N : B}\;{\scriptstyle\mathsf{App}}

\dfrac{\Gamma \vdash M : A \quad \Gamma \vdash N : B}{\Gamma \vdash (M, N) : A \times B}\;{\scriptstyle\mathsf{Pair}} \quad \dfrac{\Gamma \vdash M : A \times B}{\Gamma \vdash \mathtt{fst}\, M : A}\;{\scriptstyle\mathsf{Fst}} \quad \dfrac{\Gamma \vdash M : A \times B}{\Gamma \vdash \mathtt{snd}\, M : B}\;{\scriptstyle\mathsf{Snd}}

D. Reduction Rules for STLCext

Computational Rules.

\begin{aligned} &(\mathsf{Beta}) && (\lambda M)\, N \rightarrow M[N] \\ &(\mathsf{FstPair}) && \mathtt{fst}\,(M, N) \rightarrow M \\ &(\mathsf{SndPair}) && \mathtt{snd}\,(M, N) \rightarrow N \\ &(\mathsf{CaseInl}) && \mathtt{case}\,(\mathtt{inl}\, V)\, N_1\, N_2 \rightarrow N_1[V] \\ &(\mathsf{CaseInr}) && \mathtt{case}\,(\mathtt{inr}\, V)\, N_1\, N_2 \rightarrow N_2[V] \end{aligned}

Congruence Rules.

\begin{aligned} &(\mathsf{AppL}) && M \rightarrow M' \implies M\, N \rightarrow M'\, N \\ &(\mathsf{AppR}) && N \rightarrow N' \implies M\, N \rightarrow M\, N' \\ &(\mathsf{Lam}) && M \rightarrow M' \implies \lambda M \rightarrow \lambda M' \\ &(\mathsf{PairL}) && M \rightarrow M' \implies (M, N) \rightarrow (M', N) \\ &(\mathsf{PairR}) && N \rightarrow N' \implies (M, N) \rightarrow (M, N') \\ &(\mathsf{Fst}) && M \rightarrow M' \implies \mathtt{fst}\, M \rightarrow \mathtt{fst}\, M' \\ &(\mathsf{Snd}) && M \rightarrow M' \implies \mathtt{snd}\, M \rightarrow \mathtt{snd}\, M' \\ &(\mathsf{Inl}) && M \rightarrow M' \implies \mathtt{inl}\, M \rightarrow \mathtt{inl}\, M' \\ &(\mathsf{Inr}) && M \rightarrow M' \implies \mathtt{inr}\, M \rightarrow \mathtt{inr}\, M' \\ &(\mathsf{CaseM}) && M \rightarrow M' \implies \mathtt{case}\, M\, N_1\, N_2 \rightarrow \mathtt{case}\, M'\, N_1\, N_2 \\ &(\mathsf{CaseN_1}) && N_1 \rightarrow N_1' \implies \mathtt{case}\, M\, N_1\, N_2 \rightarrow \mathtt{case}\, M\, N_1'\, N_2 \\ &(\mathsf{CaseN_2}) && N_2 \rightarrow N_2' \implies \mathtt{case}\, M\, N_1\, N_2 \rightarrow \mathtt{case}\, M\, N_1\, N_2' \end{aligned}

References

[1] Church, A., Rosser, J.B.: Some properties of conversion. Transactions of the American Mathematical Society 39(3), 472–482 (1936)

[2] Takahashi, M.: Parallel reductions in

λ\lambda

-calculus. Information and Computation 118(1), 120–127 (1995)

[3] Newman, M.H.A.: On theories with a combinatorial definition of "equivalence". Annals of Mathematics 43(2), 223–243 (1942)

[4] van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. Ph.D. thesis, Vrije Universiteit Amsterdam (1994)

[5] Tait, W.W.: Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32(2), 198–212 (1967)

[6] de Bruijn, N.G.: Lambda calculus notation with nameless dummies. Indagationes Mathematicae 34, 381–392 (1972)

[7] Aydemir, B., et al.: Engineering formal metatheory. In: Proc. 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). pp. 3–15 (2008)

[8] Blanqui, F., Koprowski, A.: CoLoR: A Coq library on rewriting and termination. In: Proc. 8th International Workshop on Termination (WST). pp. 69–73 (2006)

[9] Nipkow, T.: More Church-Rosser proofs (in Isabelle/HOL). In: Automated Deduction — CADE-18. LNCS, vol. 2392, pp. 733–747. Springer (2002)

[10] de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Automated Deduction — CADE-28. LNCS, vol. 12699, pp. 625–635. Springer (2021)

[11] Hindley, J.R.: An abstract Church-Rosser theorem. II: Applications. Journal of Symbolic Logic 34(4), 545–560 (1969)

[12] Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edn. (1984)

[13] Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press (1989)

[14] Aydemir, B.E., et al.: Mechanized metatheory for the masses: The PoplMark challenge. In: Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol. 3603, pp. 50–65. Springer (2005)

[15] Pierce, B.C., et al.: Software Foundations. Electronic textbook (2019), https://softwarefoundations.cis.upenn.edu/