Ryan Doenges

tactic : tactical :: function : functional

I’m going to try using this blog as a lab notebook. As a first entry in that style, here’s a note about names.

In Coq, tactics build proofs and tacticals build complex tactics from simpler ones. These names, particularly “tactical”, have always seemed strange to me. While the Coq reference manual does explain what tactics and tacticals are, it rejects “tactical” as a vague “folklore notion” and never elaborates on how the names came to be.

Tactics are built from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics.

It turns out that the people who invented tactic-based interactive theorem proving in the LCF project also invented the names “tactic” and “tactical”. In their 1972 paper “A Metalanguage for Interactive Proof in LCF”, Gordon et al. are nice enough to explain why they choose the names they do:

A strategy—or recipe for proof—could be something like “induction on f and g, followed by assuming antecedents and doing case analysis, all interleaved with simplification”. This is imprecise—analysis of what cases?—what kind of induction, etc, etc.—but these in turn may well be given by further recipes still in the same style. The point is that such strategies appear to be built from simpler ones (which we call tactics rather than strategies) by a number of general operations in fairly regular ways; we call these operations tacticals by analogy with functionals.

A functional is a function that takes functions as arguments. For example, integration on the unit interval is a functional which takes a function integrable on [0, 1] and produces a real number.

The use of “tactic” has migrated a bit since 1972. In LCF a tactic is an atomic action on proof state and a strategy is built from tactics or sub-strategies structured by tacticals. In Coq an LCF tactic is called an atomic tactic and an LCF strategy is called a tactic, while tacticals or tactic expressions are still tacticals. These are fuzzy correspondences: for example, an LCF strategy might better correspond to a full-on Coq proof, which (CPDT advice aside) is almost always going to be at least several tactics long. Got it?