Stream: Coq users

Topic: Ltac2 pass pattern / term with holes to tactic


view this post on Zulip Arnoud van der Leer (Mar 15 2024 at 16:18):

Is it possible to create a tactic like the following?

Ltac2 match_n_refine (p : pattern) (c : constr) := match! goal with
| [ |- p = _ ] => refine c
end.

That checks whether the left hand side of the goal matches some pattern, (and if so, refines using some term). The latter is optional, because I am mainly interested in passing a pattern to match against to an Ltac2 tactic.

view this post on Zulip Gaëtan Gilbert (Mar 15 2024 at 16:32):

Ltac2 match_n_refine (p : pattern) (c : constr) := match! goal with
| [ |- $pattern:p = _ ] => refine c
end.

view this post on Zulip Arnoud van der Leer (Mar 15 2024 at 16:33):

Ooh, right. Thanks!

view this post on Zulip Arnoud van der Leer (Mar 15 2024 at 16:34):

Is there a canonical way to learn this stuff? Is there accessible documentation, or should I just ask these questions now and then?

view this post on Zulip Julin Shaji (Mar 15 2024 at 16:35):

I guess the later option is more feasible at the moment. :sweat_smile:
Since there is no extensive docs yet.

view this post on Zulip Gaëtan Gilbert (Mar 15 2024 at 16:36):

It's mentioned in https://coq.github.io/doc/master/refman/proof-engine/ltac2.html "Trivial Term Antiquotations"
but IDK if that's a great way to learn

view this post on Zulip Arnoud van der Leer (Mar 15 2024 at 16:36):

Thanks ^^

view this post on Zulip Arnoud van der Leer (Mar 15 2024 at 17:10):

I get an error "Error: Unknown Ltac2 variable quotation kind pattern" at $pattern in

Ltac2 build_refine (p : pattern) := traverse
  (fun s => match! goal with
  | [ |- $pattern:p = _ ] => print_refine s "[replace]"
  end)
  ().

view this post on Zulip Gaëtan Gilbert (Mar 15 2024 at 17:12):

sounds like too old coq version

view this post on Zulip Arnoud van der Leer (Mar 15 2024 at 17:16):

Oooh, that sounds possible. Thanks!

view this post on Zulip Gaëtan Gilbert (Mar 15 2024 at 17:19):

(you need 8.19 for $pattern:)

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 08:04):

My next problem: how do I supply this pattern argument? Because when trying
build_refine (_ ∘ _). I get Error: Syntax error: ')' or [ltac2_expr] expected after '(' (in [ltac2_expr]).

view this post on Zulip Gaëtan Gilbert (Mar 16 2024 at 08:11):

what's build_refine? Is ° some ltac2 notation?

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 08:13):

It is the tactic I'm working on. Basically, it traverses a syntax tree / term, tries to match every subterm to a pattern, and spits out a "refine" statement for every matching subterm

Ltac2 build_refine (p : pattern) := traverse
  (fun s => match! goal with
  | [ |- $pattern:p = _ ] => print_refine s "[replace]"
  end).

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 08:15):

I want to use this to more easily construct refine statements if I want to rewrite (which is costly) a very nested part of a term

view this post on Zulip Gaëtan Gilbert (Mar 16 2024 at 08:16):

then you need to say build_refine pattern:(_ ° _)

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 08:16):

Oooh, right.

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 08:18):

Ah, progress. We now have a different error (on the :)
Error: Syntax error: [ltac2_use_default] expected after [ltac2_expr] (in [ltac2_command]). though.

view this post on Zulip Gaëtan Gilbert (Mar 16 2024 at 08:37):

oh there's no default syntax for patterns
you can either define your own like

Ltac2 Notation "pattern:(" p(pattern) ")" : 0 := p.

(the : 0 means it doesn't need extra parentheses so you can do pattern:(foo) instead of (pattern:(foo)))

or define a notation just for your tactic like

Ltac2 Notation "build_refine_nota" p(pattern) := build_refine p.

Ltac2 Eval build_refine_nota (_ ° _).

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 08:38):

Ah, right. Thanks!

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 08:38):

The nonexistence of a default syntax sounds somewhat inconvenient, right?

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 10:44):

Hm, I am getting another error: Error: Syntax error: ')' expected after [constr] (in [ltac2_expr]). at

Ltac2 Notation "pattern:(" p(pattern) ")" : 0 := p.
Ltac2 traversals : pattern list := [pattern:(_  _)].

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 10:45):

(Btw, thank you for all the support. It seems nigh impossible to work with Ltac2 without knowledgeable people like you helping out)

view this post on Zulip Gaëtan Gilbert (Mar 16 2024 at 12:16):

seems to be a bug, please report on github

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 12:33):

Okay, thanks :-)

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 12:54):

Ah, it seems that needed some more parentheses

view this post on Zulip Gaëtan Gilbert (Mar 16 2024 at 13:08):

https://github.com/coq/coq/issues/18812

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 14:02):

And now I am trying to use a variable from a pattern in a constr, like so:

Ltac2 Notation "(traversal"
  p(pattern)
  c(constr)
")" := fun () =>
  match! goal with
  | [ |- $pattern:p = _ ] => refine c
  end.

Ltac2 t : unit -> unit := (traversal
  (app ?a ?b)
  (maponpaths  x, app x _) $b)
).

This gives Error: Unbound value b. Is there a way to pass a pattern and something that uses the results of pattern matching to a tactic?

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 14:09):

If not, that is fine, I can work around it. But was wondering whether it could be done, or whether variables in patterns just "disappear".

view this post on Zulip Gaëtan Gilbert (Mar 16 2024 at 14:26):

you would need to use the low level primitives
ltac2 notations don't bind variables in their arguments

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 14:26):

Ah, right. I am not entirely sure what the 'low level primitives' would be, though.

view this post on Zulip Gaëtan Gilbert (Mar 16 2024 at 14:35):

the stuff in Pattern.v
you can see how they're used by doing eg

Ltac2 foo f :=
  match! goal with
  | [ |- ?p = _ ] => f p
  end.
Print foo.

view this post on Zulip Arnoud van der Leer (Mar 16 2024 at 14:40):

Ah, right. Thanks!


Last updated: Jun 23 2024 at 05:02 UTC