Théo Winterhalter (Dec 03 2020 at 15:05): Théo Winterhalter (Dec 03 2020 at 15:05):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.
Pierre-Marie Pédrot (Dec 03 2020 at 15:06):You probably need to make the term second-order.
Fabian Kunze (Dec 03 2020 at 15:06):i think if x is not closed (under a binder) that is expected behaviour?
Pierre-Marie Pédrot (Dec 03 2020 at 15:06):Goal matching in a context checks for binders.
Théo Winterhalter (Dec 03 2020 at 15:07):Ah yes of course, silly me. I had not seen the λ.
Théo Winterhalter (Dec 03 2020 at 15:07):Thanks!
Fabian Kunze (Dec 03 2020 at 15:08):Well, it is still confusing behaviour ;)
Théo Winterhalter (Dec 03 2020 at 15:09):So can I still do it under a lambda?
Pierre-Marie Pédrot (Dec 03 2020 at 15:10):You need to use the second-order pattern syntax.
Pierre-Marie Pédrot (Dec 03 2020 at 15:10):That's @?x or ?@x, never remember which one.
Matthieu Sozeau (Dec 03 2020 at 15:11):The term you capture with ?x must be closed in any case no?
Pierre-Marie Pédrot (Dec 03 2020 at 15:11):No, you'll get a term_under_context in Ltac parlance.
Pierre-Marie Pédrot (Dec 03 2020 at 15:11):Using them is hard though.
Théo Winterhalter (Dec 03 2020 at 15:12):Like
lazymatch goal with
| |- context [ f (@?x y) _ ] => idtac
end.
?
It doesn't like the ident (y) I give it.
Gaëtan Gilbert (Dec 03 2020 at 15:13):it dares to reject your gifts
so give it nothing
Théo Winterhalter (Dec 03 2020 at 15:14):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.
Matthieu Sozeau (Dec 03 2020 at 15:17):y should be bound somewhere I guess.
Théo Winterhalter (Dec 03 2020 at 15:19):I basically just wanted to write some tactic to fold all occurrences of f x y to g (x,y).
Théo Winterhalter (Dec 03 2020 at 15:21):And since it's conversion and not equality it should work under binders.
Jakob Botsch Nielsen (Dec 03 2020 at 15:22):Does change (f ?x ?y) with (g (x, y)) work?
Théo Winterhalter (Dec 03 2020 at 15:23):I feel even sillier now.
Théo Winterhalter (Dec 03 2020 at 15:23):Thanks it does.
Théo Winterhalter (Dec 03 2020 at 15:24):It's interesting because that means the evars there don't have the same status right?
Matthieu Sozeau (Dec 03 2020 at 15:25):Yes, they are a different kind of metavariables
Jakob Botsch Nielsen (Dec 03 2020 at 15:25):I don't know, I had no idea that this was different from "normal" Ltac matching
Matthieu Sozeau (Dec 03 2020 at 15:26):(than existential variables in tactic mode or type inference/unification)
Fabian Kunze (Dec 03 2020 at 15:29):I have not found any place in the doc where this "change with ?foo with ?bar" behaviour is documented i think
Pierre-Marie Pédrot (Dec 03 2020 at 15:30):Given how it's implemented, it's conforting.
Fabian Kunze (Dec 03 2020 at 15:31):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
Fabian Kunze (Dec 03 2020 at 15:33):(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