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: Oct 03 2023 at 04:02 UTC