(** * Ltac is an Imperative Metaprogramming Language *)
(** #
site/posts/LtacMetaprogramming.v
# *)
(** Coq is often depicted as an _interactive_ proof assistant, thanks to its
proof environment. Inside the proof environment, Coq presents the user a
goal, and said user solves said goal by means of tactics which describes a
logical reasoning. For instance, to reason by induction, one can use the
<> tactic, while a simple case analysis can rely on the
<> or <> tactics, etc. It is not uncommon for new Coq
users to be introduced to Ltac, the Coq default tactic language, using this
proof-centric approach. This is not surprising, since writing proofs remains
the main use-case for Ltac. In practice though, this discourse remains an
abstraction which hides away what actually happens under the hood when Coq
executes a proof scripts.
To really understand what Ltac is about, we need to recall ourselves that
Coq kernel is mostly a typechecker. A theorem statement is expressed as a
“type” (which lives in a dedicated sort called [Prop]), and a proof of this
theorem is a term of this type, just like the term [S (S O)] (##2##) is of type [nat]. Proving a theorem in Coq requires
to construct a term of the type encoding said theorem, and Ltac allows for
incrementally constructing this term, one step at a time.
Ltac generates terms, therefore it is a metaprogramming language. It does it
incrementally, by using primitives to modifying an implicit state, therefore
it is an imperative language. Henceforth, it is an imperative
metaprogramming language.
To summarize, a goal presented by Coq inside the environment proof is a hole
within the term being constructed. It is presented to users as:
- A list of “hypotheses,” which are nothing more than the variables
in the scope of the hole
- A type, which is the type of the term to construct to fill the hole
We illustrate what happens under the hood of Coq executes a simple proof
script. One can use the <> vernacular command to exhibit
this.
We illustrate how Ltac works with the following example. *)
Theorem add_n_O : forall (n : nat), n + O = n.
Proof.
(** The <> vernacular command starts the proof environment. Since no
tactic has been used, the term we are trying to construct consists solely in
a hole, while Coq presents us a goal with no hypothesis, and with the exact
type of our theorem, that is [forall (n : nat), n + O = n].
A typical Coq course will explain students the <> tactic allows for
turning the premise of an implication into an hypothesis within the context.
##C \vdash P \rightarrow Q#
#
becomes
##C,\ P \vdash Q#
#
This is a fundamental rule of deductive reasoning, and <> encodes it.
It achieves this by refining the current hole into an anymous function.
When we use *)
intro n.
(** it refines the term
<<
?Goal1
>>
into
<<
fun (n : nat) => ?Goal2
>>
The next step of this proof is to reason about induction on [n]. For [nat],
it means that to be able to prove
##\forall n, \mathrm{P}\ n#
#
we need to prove that
- ##\mathrm{P}\ 0#
#
- ##\forall n, \mathrm{P}\ n \rightarrow \mathrm{P}\ (S n)#
#
The <> tactic effectively turns our goal into two subgoals. But
why is that? Because, under the hood, Ltac is refining the current goal
using the [nat_ind] function automatically generated by Coq when [nat] was
defined. The type of [nat_ind] is
<<
forall (P : nat -> Prop),
P 0
-> (forall n : nat, P n -> P (S n))
-> forall n : nat, P n
>>
Interestingly enough, [nat_ind] is not an axiom. It is a regular Coq function, whose definition is
<<
fun (P : nat -> Prop) (f : P 0)
(f0 : forall n : nat, P n -> P (S n)) =>
fix F (n : nat) : P n :=
match n as n0 return (P n0) with
| 0 => f
| S n0 => f0 n0 (F n0)
end
>>
So, after executing *)
induction n.
(** The hidden term we are constructing becomes
<<
(fun n : nat =>
nat_ind
(fun n0 : nat => n0 + 0 = n0)
?Goal3
(fun (n0 : nat) (IHn : n0 + 0 = n0) => ?Goal4)
n)
>>
And Coq presents us two goals.
First, we need to prove ##\mathrm{P}\ 0##, i.e.,
##0 + 0 = 0##. Similarly to Coq presenting a goal
when what we are actually doing is constructing a term, the use of ##+## and ##+## (i.e., Coq
notations mechanism) hide much here. We can ask Coq to be more explicit by
using the vernacular command <> to learn that when Coq
presents us a goal of the form [0 + 0 = 0], it is actually looking for a
term of type [@eq nat (Nat.add O O) O].
[Nat.add] is a regular Coq (recursive) function.
<<
fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end
>>
Similarly, [eq] is _not_ an axiom. It is a regular inductive type, defined
as follows.
<<
Inductive eq (A : Type) (x : A) : A -> Prop :=
| eq_refl : eq A x x
>>
Coming back to our current goal, proving [@eq nat (Nat.add 0 0) 0] (i.e., [0
+ 0 = 0]) requires to construct a term of a type whose only constructor is
[eq_refl]. [eq_refl] accepts one argument, and encodes the proof that said
argument is equal to itself. In practice, Coq typechecker will accept the
term [@eq_refl _ x] when it expects a term of type [@eq _ x y] _if_ it can
reduce [x] and [y] to the same term.
Is it the case for [0 + 0 = 0]? It is, since by definition of [Nat.add], [0
+ x] is reduced to [x]. We can use the <> tactic to tell Coq to
fill the current hole with [eq_refl]. *)
+ reflexivity.
(** Suspicious readers may rely on <> to verify this assertion
assert:
<<
(fun n : nat =>
nat_ind
(fun n0 : nat => n0 + 0 = n0)
eq_refl
(fun (n0 : nat) (IHn : n0 + 0 = n0) => ?Goal4)
n)
>>
<> has indeed be replaced by [eq_refl].
One goal remains, as we need to prove that if [n + 0 = n], then [S n + 0 = S
n]. Coq can reduce [S n + 0] to [S (n + 0)] by definition of [Nat.add], but
it cannot reduce [S n] more than it already is. We can request it to do so
using tactics such as [cbn]. *)
+ cbn.
(** We cannot just use <> here (i.e., fill the hole with
[eq_refl]), since [S (n + 0)] and [S n] cannot be reduced to the same term.
However, at this point of the proof, we have the [IHn] hypothesis (i.e., the
[IHn] argument of the anonymous function whose body we are trying to
construct). The <> tactic allows for substituting in a type an
occurence of [x] by [y] as long as we have a proof of [x = y]. *)
rewrite IHn.
(** Similarly to <> using a dedicated function , <> refines
the current hole with the [eq_ind_r] function (not an axiom!). Replacing [n
+ 0] with [n] transforms the goal into [S n = S n]. Here, we can use
<> (i.e., [eq_refl]) to conclude. *)
reflexivity.
(** After this last tactic, the work is done. There is no more goal to fill
inside the proof term that we have carefully constructed.
<<
(fun n : nat =>
nat_ind
(fun n0 : nat => n0 + 0 = n0)
eq_refl
(fun (n0 : nat) (IHn : n0 + 0 = n0) =>
eq_ind_r (fun n1 : nat => S n1 = S n0) eq_refl IHn)
n)
>>
We can finally use [Qed] or [Defined] to tell Coq to typecheck this
term. That is, Coq does not trust Ltac, but rather typecheck the term to
verify it is correct. This way, in case Ltac has a bug which makes it
construct ill-formed type, at the very least Coq can reject it. *)
Qed.
(** In conclusion, tactics are used to incrementally refine hole inside a term
until the latter is complete. They do it in a very specific manner, to
encode certain reasoning rule.
On the other hand, the <> tactic provides a generic, low-level way
to do the same thing. Knowing how a given tactic works allows for mimicking
its behavior using the <> tactic.
If we take the previous theorem as an example, we can prove it using this
alternative proof script. *)
Theorem add_n_O' : forall (n : nat), n + O = n.
Proof.
refine (fun n => _).
refine (nat_ind (fun n => n + 0 = n) _ _ n).
+ refine eq_refl.
+ refine (fun m IHm => _).
refine (eq_ind_r (fun n => S n = S m) _ IHm).
refine eq_refl.
Qed.
(** ** Conclusion *)
(** This concludes our introduction to Ltac as an imperative metaprogramming
language. In the ##next part of this series##, we
present Ltac powerful pattern matching capabilities. *)