I have an example where
lazymatch goal with | |- context [ f _ _ ] => idtac end.
succeeds but where
lazymatch goal with | |- context [ f ?x _ ] => idtac end.
fails saying that there is not matching clause for the match. I don't know how to minimise because it's the first time I have this problem.
You probably need to make the term second-order.
i think if x is not closed (under a binder) that is expected behaviour?
Goal matching in a context checks for binders.
Ah yes of course, silly me. I had not seen the λ.
Well, it is still confusing behaviour ;)
So can I still do it under a lambda?
You need to use the second-order pattern syntax.
That's @?x or ?@x, never remember which one.
The term you capture with ?x must be closed in any case no?
No, you'll get a term_under_context in Ltac parlance.
Using them is hard though.
lazymatch goal with | |- context [ f (@?x y) _ ] => idtac end.
It doesn't like the ident (
y) I give it.
it dares to reject your gifts
so give it nothing
Nothing is not good:
Syntax error: [Prim.identref] expected after [pattern_identref] (in [constr:operconstr]).
https://coq.inria.fr/refman/proof-engine/ltac.html doesn't have examples of this, if you have one I guess I should be able to mange.
y should be bound somewhere I guess.
I basically just wanted to write some tactic to fold all occurrences of
f x y to
And since it's conversion and not equality it should work under binders.
change (f ?x ?y) with (g (x, y)) work?
I feel even sillier now.
Thanks it does.
It's interesting because that means the evars there don't have the same status right?
Yes, they are a different kind of metavariables
I don't know, I had no idea that this was different from "normal" Ltac matching
(than existential variables in tactic mode or type inference/unification)
I have not found any place in the doc where this "change with ?foo with ?bar" behaviour is documented i think
Given how it's implemented, it's conforting.
even a "you can use patterns for subterms" that might be incorrect in some cases (under binders or somethign like that) would be nicer than just nothing. I'm opening an issue
(I only learned of this a few weeks ago to eta-reduce in my goal without copying all of it by using
change (fun x => ?f x) with f)
Last updated: Sep 26 2023 at 12:02 UTC