Stream: Coq users

Topic: Use disjunction with `match goal ` in Ltac


view this post on Zulip Ayhon (Apr 13 2024 at 21:47):

For a proof I'm trying to write my own tactic which performs the following:

Ltac my_tactic :=
   match goal with
   | [ A : ?x + ?y <=? ?d ]
   | [ A : ?y + ?x <=? ?d ] => (* continue with the tactic *)
   end.

however I'm getting an error saying Syntax error: ']' '=>' expected after [match_pattern] (in [match_context_rule]).. Is there no way to achieve this concept of looking for a goal which matches any of two patterns? The same information I want can be obtained from both.

view this post on Zulip Théo Winterhalter (Apr 14 2024 at 08:34):

In match goal you must always have the |- symbol. So x : nat, b : bool |- nat is one such goal to match.

view this post on Zulip Ayhon (Apr 14 2024 at 09:48):

You're correct, I missed that initially. However, even when adding a |- _ it doesn't seem to work, it complains with the message I quoted above

view this post on Zulip Li-yao (Apr 14 2024 at 10:22):

there are no or-patterns in match-goal:

Ltac my_tactic :=
   match goal with
   | [ A : ?x + ?y <= ?d |- _ ] => idtac x y d
   | [ A : ?y + ?x <= ?d |- _ ] => idtac x y d
   end.

view this post on Zulip Ayhon (Apr 14 2024 at 11:44):

That's unfortunate, since I needed to nest a couple of match goals to prove something like

h: ?x + ?y <=? ?d
h': - ?y + ?z <=? ?d'
|- ?x + ?z <=? ?d + ?d'

is there no other way of handling this than dealing with a lot of repetition? I was trying to create a tactic that would help with the different ways in which ?x + ?y can be commuted.

view this post on Zulip Théo Winterhalter (Apr 14 2024 at 11:45):

You could always create a tactic that you call in all branches?

view this post on Zulip Ayhon (Apr 14 2024 at 11:57):

Can I pass the valules of ?x, ?y and ?z to the tactic as arguments? I was under the impression that arguments to Ltac needed to be hypothesis, but that may have been my own assumption. I'll try it out

view this post on Zulip Kenji Maillard (Apr 14 2024 at 12:53):

I'm empirically convinced that you can bind terms in an Ltac definition, but your question triggered me to have a look at the documentation. Looking at Ltac and ltac functions is not very insightful, but it does say that ltac functions arguments have to be evaluated before the application happen, so the best guess I can formulate is that an Ltac function is supposed to bind any tactic_value, which are supposed to contain both untyped gallina terms (through uconstr:(...)) and typed gallina terms (through constr:(...)). The paragraph on substitution also contains an indication that names can disambiguated between ltac names and gallina names.

view this post on Zulip Pierre-Marie Pédrot (Apr 14 2024 at 14:00):

Short answer: the ?x notation in match goal works as you intend it to do


Last updated: Jun 23 2024 at 04:03 UTC