Ltac is an Imperative Metaprogramming Language

coq

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 induction tactic, while a simple case analysis can rely on the destruct or case_eq 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 script.

To really understand what Ltac is about, we need to recall ourselves that Coq kernel is mostly a type checker. 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 Show Proof 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 Proof 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 to students the intro 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 intro encodes it. It achieves this by refining the current hole into an anonymous 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 induction 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., the Coq notations mechanism) hides much here. We can ask Coq to be more explicit by using the vernacular command Set Printing All 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) 0That is, 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 type checker 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 @eq nat (Nat.add 0 0) 0? It is, since by definition of Nat.add, Nat.add 0 x is reduced to x. We can use the reflexivity tactic to tell Coq to fill the current hole with eq_refl.

  + reflexivity.

Suspicious readers may rely on Show Proof to verify this assertion.

  (fun n : nat =>
     nat_ind
       (fun n0 : nat => n0 + 0 = n0)
       eq_refl
       (fun (n0 : nat) (IHn : n0 + 0 = n0) => ?Goal4)
       n)

?Goal3 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.

  + cbn.

We cannot just use reflexivity 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 rewrite tactic allows for substituting in a type an occurrence of x by y as long as we have a proof of x = y. *)

    rewrite IHn.

Similarly to induction using a dedicated function, rewrite refines the current hole with the eq_ind_r functionAgain, not an axiom. . Replacing n + 0 with n transforms the goal into S n = S n. Here, we can use reflexivity (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 type check this term. That is, Coq does not trust Ltac, but rather type check the term to verify it is correct. This way, in case Ltac has a bug which makes it construct an 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 rules.

On the other hand, the refine 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 refine 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.