## Stream: Coq users

### Topic: Tactic Notation for in clause

#### Yannick Zakowski (May 18 2020 at 16:12):

Is there a way to give to a Tactic the kind of pattern that one gives to rewrite for instance after a "in", i.e. in particular so that I can pass to the same tactic either an hyp, or `|- *` to rewrite in the goal?
A silly self example for concreteness would be:

``````  Axiom f: 1 = 2.
Ltac foo := rewrite f.
Ltac foo_hyp h := rewrite f in h.
Ltac Notation "foo" "in" hyp(h) := foo h.
``````

And the point would be to not need to define `foo` that is basically a duplicate of `foo_hyp`, but instead do something like:

``````  Axiom f: 1 = 2.
Ltac foo_hyp h := rewrite f in h.
Ltac Notation "foo" "in" hyp(h) := foo h.
Ltac Notation "foo"  := foo |-*. (* or "foo goal" or something like that *)
``````

#### Hugo Herbelin (Jun 03 2020 at 18:59):

@Yannick Zakowski: the grammar entry to parse `in` clauses (the one with `|-`) is currently not exported for the purpose of `Tactic Notation`. This could be done, like it is done e.g. for `intro_patterns` by defining what is called a `genarg` and doing mechanically a couple of appropriate changes. The grammar entry is called `in_clause` in `plugins/ltac/g_tactic.mlg`.

Maybe Ltac2 has a ready solution for that otherwise. You should ask @ppedrot.

#### Théo Zimmermann (Jun 03 2020 at 19:04):

(edited the topic to keep the answer closer to the question)

#### Yannick Zakowski (Jun 03 2020 at 20:37):

Thank you for the answer Hugo!
I will have a look on Ltac2's side, and will alternatively consider opening an issue or a PR as soon as I can, that would be a quite useful feature to have access to.

#### Paolo Giarrusso (Jun 04 2020 at 13:19):

Let me just mention that Ltac(2) support for this and other "variadic" notations would be a godsend. Quite a few people resort to writing N variants of a tactic — sometimes in a combinatorial explosion.

#### Pierre-Marie Pédrot (Jun 04 2020 at 13:23):

There is a dedicated type of clauses in Ltac2, as well as its corresponding (primitive) scope.

#### Pierre-Marie Pédrot (Jun 04 2020 at 13:24):

See for instance the definition of the `set` tactic in Ltac2.Notation

#### Pierre-Marie Pédrot (Jun 04 2020 at 13:24):

``````Ltac2 Notation "set" p(thunk(pose)) cl(opt(clause)) :=
Std.set false p (default_on_concl cl).
``````

#### Pierre-Marie Pédrot (Jun 04 2020 at 13:25):

For true "variadic" tactics, just parse a list instead, and thanks to the magic of datastructures, you should be happy.

Last updated: Jun 18 2024 at 21:01 UTC