Scrap your boilerplate definitions in 10 lines of Ltac!

Mechanized metatheory proofs often feature many similar proof obligations which Coq users can automatically discharge using Ltac. Unfortunately, there is no comparable solution to help users state many similar lemmas or write inductive definitions with many closely related cases. This talk presents IDT, a Coq library for automatically generating these sorts of boilerplate definitions, powered by Template-Coq and using Ltac to do all the heavy lifting. We give several examples of IDT in action, drawn from a formalization of a language for oblivious computation. Using IDT, we can generate dozens of definitions from just a few lines of Ltac.