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.

In `match goal`

you must always have the `|-`

symbol. So `x : nat, b : bool |- nat`

is one such goal to match.

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

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

That's unfortunate, since I needed to nest a couple of `match goal`

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

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

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

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.

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

Last updated: Jun 23 2024 at 04:03 UTC