A Formalized Extension of the Substitution Lemma in Coq

TL;DR

This paper extends the lambda-calculus with explicit substitutions and formally verifies the preservation of the substitution lemma using Coq, employing a nominal approach for alpha-equivalence.

Contribution

It introduces an uninterpreted explicit substitution operator into lambda-calculus and formally proves the lemma's validity within this extended framework using Coq.

Findings

The substitution lemma remains valid in the extended calculus.

Formal verification was successfully conducted in Coq.

The nominal approach effectively handled alpha-equivalence in proofs.

Abstract

The substitution lemma is a renowned theorem within the realm of lambda-calculus theory and concerns the interactional behaviour of the metasubstitution operation. In this work, we augment the lambda-calculus's grammar with an uninterpreted explicit substitution operator, which allows the use of our framework for different calculi with explicit substitutions. Our primary contribution lies in verifying that, despite these modifications, the substitution lemma continues to remain valid. This confirmation was achieved using the Coq proof assistant. Our formalization methodology employs a nominal approach, which provides a direct implementation of the alpha-equivalence concept. The strategy involved in variable renaming within the proofs presents a challenge, specially on ensuring an exploration of the implications of our extension to the grammar of the lambda-calculus.