Explicit Weakening

TL;DR

This paper introduces a new, simplified formulation of substitution in proof assistants, enabling immediate justification of facts with minimal proof effort, demonstrated through an executable Agda script.

Contribution

It presents a novel, concise approach to substitution in proof assistants, reducing complex proofs to a simple 'refl' justification.

Findings

Substitution facts can be justified instantly with 'refl'

The approach is implemented as an executable Agda script

Simplifies formal proofs significantly

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.