A Generic Approach to Proofs about Substitution
Abhishek Anand, Vincent Rahli · 2014
It is well known that reasoning about substitution is a huge "distraction" that inevitably gets in the way of formalizing interesting properties of languages with variable bindings. Most formalizations have their own separate definitions of terms and substitution, and properties about it. However there is a great deal of uniformity in the way substitution works and the reasons why its properties hold. We expose this uniformity by defining terms, substitution and α-equality generically in Coq by parametrizing them over a Context Free Grammar annotated with Variable binding information (CFGV).