When formalizing the meta-theory of programming languages or type systems in proof assistants such as Rocq, a key design decision is the choice of variable representation (see e.g. the PoplMark challenge). De Bruijn indices are a popular option because they make alpha-equivalence coincide with syntactic equality. However, de Bruijn indices also introduce significant overhead in the form of lift and renaming operations, which require many technical lemmas and can make proofs tedious.

To address this, many libraries attempt to automate repetitive aspects of dealing with de Bruijn indices and substitution, both in programming languages and in proof assistants. In particular, while Autosubst has been successfully used in many formalizations, its simplification tactic \emph{asimpl} suffers from significant performance issues when used in large developments. In this talk, we present Sulfur (\underline{su}bstitution \underline{l}ogical \underline{f}ramework \underline{u}sing \underline{r}eflection), a Rocq plugin that attempts to solve the performance issues of Autosubst’s \emph{asimpl} tactic by implementing it as a \emph{reflective tactic}. For now, Sulfur supports single-sorted, extrinsic syntax: extensions to more complex signatures are discussed in the future work section.