Proof assistants like Coq are now eminently effective for formalizing
"research-grade" mathematics, verifying serious software systems, and,
more broadly, enabling researchers to mechanize and breed confidence
in their results. Nevertheless, the mechanization of substantial
proofs typically requires a significant amount of manual effort. To
alleviate this burden, proof assistants typically provide an
additional language for tactic programming. Tactics support
general-purpose scripting of automation routines, as well as fine
control over the state of an interactive proof. However, for most
existing tactic languages (e.g., ML, Ltac), the price to pay for this
freedom is that the behavior of a tactic lacks any static
specification within the base logic of the theorem prover (such as, in
Coq, a type). As a result of being untyped, tactics are known to be
difficult to compose, debug, and maintain.
In my thesis I present two different approaches to typed tactic
programming in the context of Coq: Lemma Overloading and Mtac. Both
approaches rely heavily on the unification algorithm of Coq, which is
a complex mixture of different heuristics and has not been formally
specified. Therefore, I also build and describe a new unification
algorithm better suited for tactic programming in Coq. In the talk I
will describe the high level achievements of my work and introduce in
depth Mtac, a new programming language for tactic programming.