I would like to pass a tactic as a parameter to a separately-defined Ltac procedure. However, it seems whenever I include a “;” in that tactic I’m met with a syntax error. I’ve crafted a minimal example below. Perhaps I’ve made a silly mistake with parentheses or some such, but I can’t seem to get it working.
Ltac my_tac tac := tac.
Lemma foo : (1 = 1 /\ 2 = 2).
Proof.
split; [reflexivity | reflexivity]. (* Succeeds as expected *)
Undo.
my_tac (split; [reflexivity | reflexivity]). (* Syntax Error? *)
Qed.
Enclose the Ltac parameter in an ltac:() block (see below). Arguments to a tactic can be either terms or tactics, and are parsed as terms by default. See “ltac:(ltac_expr)” from the Coq documentation here. (Credit to Theo Zimmermann on the Coq Club for this suggestion).
Noteworthy “gotcha”: Coq will interpret an ltac:() block within parentheses itself as a “constr”, not a tactic.
i.e. my_tac (ltac:(...)) is not the same as my_tac ltac:(...), and would not work below. This is quite confusing to me–adding parentheses around a parameter seems a reasonable thing to do, and likely one of the first things one might try. Discussion on the mailing list suggests an update to the documentation is forthcoming to warn of this distinction. (Credit to Jason Gross on the Coq Club for this gotcha).
Lemma foo : (1 = 1 /\ 2 = 2).
Proof.
my_tac ltac:(split; [reflexivity | reflexivity]). (* Succeeds *)
Qed.
Another suggestion (I have yet to play around with this): Use Tactic Notations (Coq documentation)–gives you some control over tactic parsing precedence, may be able to avoid encolsiing a tactic parameter in ltac:(). (Credit to jonikelee@gmail.com from the Coq Club).