Proof Pearl: Substitution Revisited, Again

Introduction

We revisit Allen Stoughton's 1988 paper "Substitution Revisited" and use it as our test case in exploring a nominal approach to variable binding in Coq. In our nominal approach, we use only one-sorted variable names as in pen-and-paper work. We show that it is not only feasible, but also convenient to work with the nominal approach in Coq. Furthermore, we figure out a light infrastructure which provides the base in proving a series of results about simultaneous substitution and alpha-congruence in the untyped lambda calculus.

The three main features of our paper are as follows:
  1. We apply nominal approach with one-sorted variable names to variable binding in Coq.
  2. We use Coq's internal equality instead of any kind of set-theoretic equalities or setoid equalities.
  3. We employ only Coq's basic terminology and techniques.
Our primary contribution is to demonstrate that it is not only feasible, but also convenient to work with the nominal approach in Coq. Most of all, our formalization is very compact and close to the original reasoning on paper. We even believe that it would satisfy the three criteria proposed in POPLmark Challenge, i.e., reasonable overheads, cost of entry, and transparency in evaluating mechanization of formal metatheory. However, this goes beyond the scope of this paper.


Papers


Library codes

The proof scripts along with required libraries can be downloaded as a gzip'd tarball [Stoughton.tgz]. Extracting the files creates a directory called Stoughton which contains six files. Among them, lambda_calculus.v is the main source code containing the formalization of (Stoughton 1988). You can compile the codes and generate all the documents by using make html. The proof scripts can be compiled on Coq8.3.pl4.

Untyped lambda calculus lambda_calculus Source HTML
lists_decidable Source HTML
fresh_variables Source HTML
functions_extra Source HTML
case_tac Source HTML


Main References

  1. Allen Stoughton. Substitution Revisited. Theor. Comput. Sci., 59: 317-325, 1988.