Autosubst 2: Towards Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions

Saarland University Computer Science

Jonas Kaiser, Steven Schäfer and Kathrin Stark

Formalising metatheory in the Coq proof assistant is tedious as native support for reasoning about languages with binders is marginal at best. The Autosubst framework (Schäfer, Smolka and Tebbi, 2015) automates working with de Brujin terms: for each annotated inductive type, it generates a corresponding substitution operation and a decision procedure for assumption-free substitution lemmas. A key part of the equational theory are parallel substitutions which combine multiple single-variable substitutions. Among other limitations, however, Autosubst lacks support for mutual inductive types due to its separate treatment of sorts. This restriction is removed in our prototype implementation of Autosubst 2: second-order HOAS specifications are translated into potentially mutual inductive term sorts. Again, parallelising substitutions is the key: we introduce vector substitutions to combine the application of multiple parallel substitutions into exactly one instantiation operation for each sort. The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework.