8

While trying to create an Ltac definition that loops over a variable-length argument list, I encountered the following unexpected behavior on Coq 8.4pl2. Can anyone explain it to me?

Ltac ltac_loop X :=
  match X with
  | 0 => idtac "done"
  | _ => (fun Y => idtac "hello"; ltac_loop Y)
  end.

Goal True.
  ltac_loop 0.  (* prints "done" as expected *)
  ltac_loop 1 0.  (* prints "hello" then "done" as expected *)
  ltac_loop 1 1 0.  (* unexpectedly yields "Error: Illegal tactic application." *)
Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
Kevin Hamlen
  • 185
  • 3

1 Answers1

6

Let's expand the last invocation of ltac_loop to see what's happening:

ltac_loop 1 1 0
-> (fun Y => idtac "hello"; ltac_loop Y) 1 0
-> (idtac "hello"; ltac_loop 1) 0

There you can see the problem: you are trying to apply something that is not a function to an argument, which results in the error you saw. The solution is to rewrite the tactic in continuation-passing style:

Ltac ltac_loop_aux k X :=
  match X with
  | 0 => k
  | _ => (fun Y => ltac_loop_aux ltac:(idtac "hello"; k) Y)
  end.

Ltac ltac_loop X := ltac_loop_aux ltac:(idtac "done") X.
Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • 1
    In `ltac_loop_aux`, you could replace `(fun Y => ltac_loop_aux ltac:(idtac "hello"; k) Y)` with `ltac_loop_aux ltac:(idtac "hello"; k)`. – Zimm i48 Oct 19 '16 at 08:27