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.