- MEMOCODE Paper Accepted
- NFM '21 (Virtual) Conference Presentation
- Paper Accepted to NFM '21
- Ltac Bug or Ltac Feature?
- Deep Field by Eric Whitacre
- Higher-Order Automation
- HotSoS 2020 Poster Presentation
- Dissertation Proposal Defense

Index

Blog

Blog Categories

Announcements

Coq

Music

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