Coq: Ltac определений над списками переменных аргументов?

Question

При попытке создать определение Ltac, которое зацикливается на списке аргументов переменной длины, я столкнулся со следующим неожиданным поведением на Coq 8.4pl2. Кто-нибудь может мне это объяснить?

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." *)

Answer 1

Давайте расширим последний вызов ltac_loop чтобы увидеть, что происходит:

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

Здесь вы можете увидеть проблему: вы пытаетесь применить что-то, что не является функцией, к аргументу, что приводит к появившейся ошибке. Решение состоит в том, чтобы переписать тактику в стиле продолжения:

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.