Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac

Jason Gross, Andres Erbsen, Adam Chlipala. Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac. Proceedings of the Interactive Theorem Proving - Ninth International Conference (ITP'18). July 2018.

Coming soon!

We present a new strategy for performing reification in Coq. That is, we show how to generate first-class abstract syntax trees from "native" terms of Coq's logic, suitable as inputs to verified proof procedures in the proof by reflection style. Our new strategy, based on the pattern tactic, is simple, short, and fast. We survey the existing methods of reification, describing various design choices and tricks that can be used to speed them up, as well as various limitations. Our strategy is not a good fit, for example, when a term must be reified without performing beta-iota-zeta reduction. We describe the results of benchmarking 18 variants of reification, in addition to our own, finding that our own reification outperforms 16 of these methods in all cases, and one additional method in some cases; the fastest method of reification we tested is writing an OCaml plugin. Our method is the most concise of the strategies we considered, requiring only two to four lines of Ltac -- beyond lists of the identifiers to reify and their reified variants -- to reify a term. Additionally, our strategy automatically provides error messages which are no less helpful than Coq's own error messages.

Source code