Explicit Weakening

TL;DR

The paper addresses the burden of substitution reasoning in proof assistants by introducing explicit weakening, a formulation that makes key equations definitional. It presents a literate Agda implementation using de Bruijn indices and intrinsic types, with an explicit weakening operation and a separate substitution composition, enabling automatic rewrites and reflexive proofs for core lemmas. The approach yields trivial proofs for classic substitution properties, such as left identity, associativity, and beta-like reductions, demonstrated through concrete examples and exercises tied to the PLFA development. While the method offers potential for simpler formalizations and automation, it acknowledges that distinguishing certain terms may complicate equivalence checks, leaving practical impact an open question requiring further experience.

Abstract

I present a novel formulation of substitution, where facts about substitution that previously required tens or hundreds of lines to justify in a proof assistant now follow immediately - they can be justified by writing the four letters "refl". The paper is an executable literate Agda script, and source of the paper is available as an artifact in the file Weaken.lagda.md. Not all consequences of the pandemic have been awful. For the last three years, I've had the great pleasure of meeting with Peter Thiemann and Jeremy Siek for a couple of hours every week, via Zoom, exploring topics including core calculi, gradual typing, and formalisation in Agda. The work reported here arose from those discussions, and is dedicated to Peter on the occasion of his 60th birthday.