Effective support for custom proof automation is essential for large-scale
interactive proof development. However, existing languages for automation
via tactics either (a) provide no way to specify the behavior of tactics
within the base logic of the accompanying theorem prover, or (b) rely on
advanced type-theoretic machinery that is not easily integrated into
established theorem provers.
My thesis is that typechecked tactic programming in Coq is possible in two
different programming styles: (1) logic programming (by exploiting Coq’s
existing overloading mechanism) and (2) functional programming (by a new
monadic language, Mtac). The combination of both styles leads to a novel
way of creating extensible tactics.