## How to quantify quantifiers: an Ltac puzzle

- April 5, 2018

In some occasions, using the Coq proof assistant stops resembling a normal software development activity, and becomes more similar to puzzle solving.

Similarly to the excellent video games of the Zachtronics studio (TIS-100, SpaceChem, …), the system provides you with puzzles where obstacles have to be side-stepped using a fair amount of tricks and ingenuity, and finally solving the problem has often no other utility than the satisfaction of having completed it.

In this blog-post, I would like to present what I think is one such situation. What the puzzle is, how we solved it, and why you shouldn’t probably do that if you like spending your time in a useful manner.

# Prelude

A few months ago, I was wondering if it was possible to count the number of `exists`

in front of the goal, using `Ltac`

(the tactic language of Coq). That is, write a tactic that would for example produce `3`

on the following goal:

```
====================================
exists x y z : nat, x + y = z
```

“That’s easy”, I thought. “I will just write a recursive function in Ltac”. First, we check that we can get the body of the `exists`

by matching on the goal – this seems to work as expected:

```
Goal exists x y z : nat, x + y = z.
match goal with |- exists x, ?G' => idtac G' end.
(* Prints (exists y z : nat, x + y = z) *)
```

Then, we write a tactic to do this recursively, walking down the type of the goal until there is no `exists`

in front of it.

```
Ltac count_exists_naive_aux G n :=
lazymatch G with
| exists x, ?G' => count_exists_naive_aux G' (S n)
| _ => constr:(n)
end.
Ltac count_exists_naive :=
match goal with |- ?G =>
let x := count_exists_naive_aux G 0 in
pose x
end.
```

But this does not work, and fails with the error below. It seems Ltac does not handle terms with free variables.

```
Error: Must evaluate to a closed term
offending expression:
G
this is an object of type constr_under_binders
```

At this point, the reasonable choice would be to give up, write specialized versions of the tactic for 0 to 7 exists (who has goals with more than 7 exists anyway?), and wait for one of the successors of Ltac (Ltac2 maybe?) to come up without these limitations. Unreasonably, I sought the help of Cyprien Mangin, my local puzzle game and Coq expert, and we came up with the following solution.

# A first idea: “destruct”ing the goal

A first idea: one thing that we can do iteratively on a `exists x y z ...`

term is splitting it using `destruct`

– *if we have it as an hypothesis*. For example:

```
(* Goal:
H : exists x y z : nat, x + y = z
====================================
True
*)
Ltac count_in_hyp H acc kont :=
lazymatch type of H with
| exists _, _ => destruct H as [? H]; count_in_hyp H (S acc) kont
| _ => kont acc
end.
count_in_hyp H 0 ltac:(fun n => pose n).
(* Goal:
x, x0, x1 : nat
H : x + x0 = x1
n := 3 : nat
====================================
True
*)
```

Notice we had to do the “standard trick” of writing the tactic in continuation passing style (using `kont`

here as a continuation to return the number of `exists`

). This is required since a Ltac tactic cannot do side-effects on the goal (here, `destruct`

) and at the same time return a term.

Now, we want to count the number of exists *in the goal*, not in an hypothesis. How could we turn the goal into an hypothesis – after all, these exists are something we need to provide, not something we get. In fact, it is possible to get a sub-goal with an hypothesis of the same type as the goal – simply, this sub-goal won’t be much relevant for proving the goal. We define the following helper lemma:

```
Definition helper_lemma : forall P Q, (P -> True) -> Q -> Q :=
fun P Q _ Q_proof => Q_proof.
```

Applying this lemma produces an extra sub-goal with an hypothesis of type `P`

. Notice how the proof term corresponding to this sub-goal is completely discarded in the definition of `helper_lemma`

: this sub-goal is only relevant for our Ltac tricks. To get a sub-goal which allows destructing the exists in front of the goal, we do:

```
(* Goal:
====================================
exists x y z : nat, x + y = z
*)
match goal with |- ?G => apply (helper_lemma G) end;
[ intro H | ].
(* Goal 1:
H : exists x y z : nat, x + y = z
====================================
True
Goal 2:
====================================
exists x y z : nat, x + y = z
*)
count_in_hyp H 0 ltac:(fun n => pose n).
(* Goal 1:
x, x0, x1 : nat
H : x + x0 = x1
n := 3 : nat
====================================
True
Goal 2:
====================================
exists x y z : nat, x + y = z
*)
```

# Second idea: communicating through evars

We are not done yet: we can count the number of exists in the first – dummy – sub-goal, but we need to transmit this information to the main sub-goal.

The second idea is to propagate this information using an “evar”. An evar is a Coq term representing a “hole”: its definition is not known yet, and will be given later in the proof. This discipline only exists when constructing the proof: evars do not appear in the proof term, where everything happens in order.

The idea here is to introduce an evar before applying our auxiliary `helper_lemma`

. This evar will appear in the context of both sub-goals introduced by the lemma: in the first one, we can “instantiate” it (ie. set its definition) with the number of exists computed, and use it in the second sub-goal.

This gives us:

```
evar (n : nat).
(* Goal:
n := ?n : nat
====================================
exists x y z : nat, x + y = z
*)
match goal with |- ?G => apply (helper_lemma G) end;
[ intro H;
let x := count_in_hyp H 0 in
instantiate (n := x);
exact I
| ].
(* Goal:
n := 3 : nat
====================================
exists x y z : nat, x + y = z
*)
```

Hurray! It works. We can wrap this in a reusable tactic:

```
Ltac count_in_ty G kont :=
let n := fresh "n" in
evar (n : nat);
apply (helper_lemma G); [
let H := fresh in
intro H; count_in_hyp H 0 ltac:(fun x => instantiate (n := x));
exact I
| kont n ].
```

# Third idea: cleaning up

The tactic above indeed works, and successfully counts the number of exists in the goal. However, it is still a bit messy. In particular, the trick of using a helper lemma shows up in the proof term. Using `Show Proof`

after running `count_in_ty`

on the goal yields:

```
(let n := 3 in
helper_lemma (exists x y z : nat, x + y = z) (exists x y z : nat, x + y = z)
(fun H : exists x y z : nat, x + y = z =>
match H with
| ex_intro _ x (ex_intro _ x0 (ex_intro _ _ _)) => I
end) ?Goal)
```

This is mostly noise! Indeed, `helper_lemma P Q H1 H2`

is equivalent to simply `H2`

– we only use the lemma for our Ltac tricks, and ideally, this should not appear in the final proof term. We can do better. The third idea is to isolate the messy proof term containing `helper_lemma`

, and simplify it after it has been produced by counting the exists. Isolating the proof term can be achieved with the following pattern:

```
let n := constr:(ltac:(mytactic) : nat) in
...
```

`constr:()`

and `ltac:()`

are both quotations: the first one indicates that its contents must be parsed as a Coq term, and the second one that it must be parsed as a tactic. Their combination above indicates that we want to produce a term (of type `nat`

), and to run the tactic `mytactic`

to produce it.

`mytactic`

will run on a goal of type `nat`

, and the proof term it produces by proving this goal will become the definition of `n`

. Let us replace `mytactic`

by our counting tactic (its continuation being simply `exact`

to prove the `nat`

goal using the result of the count):

```
(* Goal:
====================================
exists x y z : nat, x + y = z
*)
match goal with |- ?G =>
let n := constr:(ltac:(count_in_ty G ltac:(fun n => exact n)) : nat) in
pose n
end.
(* Goal:
n := ((let n := 3 in
helper_lemma (exists x y z : nat, x + y = z) nat
(fun H : exists x y z : nat, x + y = z =>
match H with
| ex_intro _ x (ex_intro _ x0 (ex_intro _ _ _)) => I
end) n)
:
nat) : nat
============================
exists x y z : nat, x + y = z
*)
```

The messy proof-term is now part of the definition. We now just have to simplify it, e.g. using `eval cbv in n`

:

```
match goal with |- ?G =>
let n := constr:(ltac:(count_in_ty G ltac:(fun n => exact n)) : nat) in
let n := (eval cbv in n) in
pose n
end.
(* Goal:
n := 3 : nat
============================
exists x y z : nat, x + y = z
*)
Show Proof.
(* Prints: (let n := 3 in ?Goal) *)
```

And there you have it! Here is the whole implementation of `count_exists`

:

```
Ltac count_in_hyp H acc kont :=
lazymatch type of H with
| exists _, _ => destruct H as [? H]; count_in_hyp H (S acc) kont
| _ => kont acc
end.
Definition helper_lemma : forall P Q, (P -> True) -> Q -> Q :=
fun P Q _ Q_proof => Q_proof.
Ltac count_in_ty G kont :=
let n := fresh "n" in
evar (n : nat);
apply (helper_lemma G); [
let H := fresh in
intro H; count_in_hyp H 0 ltac:(fun x => instantiate (n := x));
exact I
| kont n ].
Ltac count_exists kont :=
match goal with |- ?G =>
let n := constr:(ltac:(count_in_ty G ltac:(fun n => exact n)) : nat) in
let n := (eval cbv in n) in
kont n
end.
```