One of the most misleading introduction to Coq is to say that “Gallina is
for programs, while tactics are for proofs.” Indeed, in Coq we construct
terms of given types, always. Terms encodes both programs and proofs about
these programs. Gallina is the preferred way to construct programs, and
tactics are the preferred way to construct proofs.
The key word here is “preferred.” We do not always need to use tactics to
construct a proof term. Conversly, there are some occasions where
constructing a program with tactics become handy. Furthermore, Coq actually
allows for mixing together Ltac and Gallina.
Constructing terms proofs directly in Gallina often happens when one is
writing dependently-typed definition. For instance, we can write a type safe
from_option function (inspired by this very
nice write-up) such that the option to unwrap shall be accompagnied by
a proof that said option contains something. This extra argument is used in
the None case to derive a proof of False, from which we can derive
When Coq encounters ltac:(), it treats it as a hole. It sets up a
corresponding goal, and tries to solve it with the supplied tactic.
Conversly, there exists ways to construct terms in Gallina when writing a
proof script. Certains tactics takes such terms as arguments. Besides, Ltac
provides constr:() and uconstr:() which work similarly to ltac:().
The difference between constr:() and uconstr:() is that Coq will try to
assign a type to the argument of constr:(), but will leave the argument of
For instance, consider the following tactic definition.
Both x the argument of wrap_id and f the anonymous identity function
are not typed. It is only when they are composed together as an argument of
exact (which expects a typed argument, more precisely of the type of the
goal) that Coq actually tries to typecheck it.
As a consequence, wrap_id generates a specialized identity function for
each specific context.
The generated anonymous identity function is funx:listα=>x. Besides,
we do not need to give more type information about nil. If wrap_id were
to be expecting a typed term, we would have to replace nil by (@nilα).
Proofs and computational programs are encoded in Coq as terms, but there is
a fundamental difference between them, and it is highlighted by one of the
axiom provided by the Coq standard library: proof irrelevance.
Proof irrelevance states that two proofs of the same theorem (i.e., two
proof terms which share the same type) are essentially equivalent, and can
be substituted without threatening the trustworthiness of the system. From a
formal methods point of view, it makes sense. Even if we value “beautiful
proofs,” we mostly want correct proofs.
The same reasoning does not apply to computational programs. Two functions
of type nat->nat->nat are unlikely to be equivalent. For instance,
add, mul or sub share the same type, but computes totally different
Using tactics such as auto to generate terms which do not live inside
Prop is risky, to say the least. For instance,
This works, but it is certainly not what you would expect:
add = fun _ y : nat => y
: nat -> nat -> nat
That being said, if we keep that in mind, and assert the correctness of the
generated programs (either by providing a proof, or by extensively testing
it), there is no particular reason not to use Ltac to generate terms when it
Dependently-typed programming can help here. If we decorate the return type
of a function with the expected properties of the result wrt. the function’s
arguments, we can ensure the function is correct, and conversly prevent
tactics such as auto to generate “incorrect” terms. Interested readers may
refer to the dedicated
series on this very website.