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.
20200828  Heavy reworking of the Ltac series  a7e4531 
 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
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 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 anymous function.
When we use
intro n.
it refines the term
?Goal1into
fun (n : nat) => ?Goal2The 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)$
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) endSo, 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 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) endSimilarly, 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 xComing 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 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
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. 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
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.
(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 illformed 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
refine
tactic provides a generic, lowlevel 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.