# Ltac is an Imperative Metaprogramming Language

## Revisions

This revisions table has been automatically generated
from the
`git`

history of this website repository, and the
change descriptions may not always be as useful as they should.

You can consult the source of this file in its current version here.

2021-03-28 | 2021 Spring redesign | 495f9db |

2020-08-28 | Heavy reworking of the Ltac series | a7e4531 |

*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 scripts.
- 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

`Show Proof`

vernacular command to exhibit
this.
The
A typical Coq course will explain students the
becomes
This is a fundamental rule of deductive reasoning, and

`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.
`intro`

tactic allows for
turning the premise of an implication into an hypothesis within the context.
$C \vdash P \rightarrow Q$

$C,\ P \vdash Q$

`intro`

encodes it.
It achieves this by refining the current hole into an anymous function.
When we use
intro n.

it refines the term
into
The next step of this proof is to reason about induction on n. For nat,
it means that to be able to prove
we need to prove that
The
So, after executing

?Goal1

fun (n : nat) => ?Goal2

$\forall n, \mathrm{P}\ n$

- $\mathrm{P}\ 0$
- $\forall n, \mathrm{P}\ n \rightarrow \mathrm{P}\ (S n)$

`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 nInterestingly 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

induction n.

The hidden term we are constructing becomes
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
Nat.add is a regular Coq (recursive) function.
Similarly, eq is
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
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

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

`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.
fix add (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (add p m) end

*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

*if*it can reduce x and y to the same term.`reflexivity`

tactic to tell Coq to
fill the current hole with eq_refl.
+ reflexivity.

Suspicious readers may rely on
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.

`Show Proof`

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)

`?Goal3`

has indeed be replaced by eq_refl.
+ 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
occurence 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 function (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.
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.

(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)

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
If we take the previous theorem as an example, we can prove it using this
alternative proof script.

`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.
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.