Stream: Coq users

Topic: match goal with context succeeding with _ but failing with ?


view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 15:06):

You probably need to make the term second-order.

view this post on Zulip Fabian Kunze (Dec 03 2020 at 15:06):

i think if x is not closed (under a binder) that is expected behaviour?

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 15:06):

Goal matching in a context checks for binders.

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 15:07):

Ah yes of course, silly me. I had not seen the λ.

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 15:07):

Thanks!

view this post on Zulip Fabian Kunze (Dec 03 2020 at 15:08):

Well, it is still confusing behaviour ;)

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 15:09):

So can I still do it under a lambda?

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 15:10):

You need to use the second-order pattern syntax.

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 15:10):

That's @?x or ?@x, never remember which one.

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 15:11):

The term you capture with ?x must be closed in any case no?

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 15:11):

No, you'll get a term_under_context in Ltac parlance.

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 15:11):

Using them is hard though.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Dec 03 2020 at 15:13):

it dares to reject your gifts
so give it nothing

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 15:14):

Nothing is not good:

Syntax error: [Prim.identref] expected after [pattern_identref] (in [constr:operconstr]).

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 15:15):

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.

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 15:17):

y should be bound somewhere I guess.

view this post on Zulip 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).

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 15:21):

And since it's conversion and not equality it should work under binders.

view this post on Zulip Jakob Botsch Nielsen (Dec 03 2020 at 15:22):

Does change (f ?x ?y) with (g (x, y)) work?

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 15:23):

I feel even sillier now.

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 15:23):

Thanks it does.

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 15:25):

Yes, they are a different kind of metavariables

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 15:26):

(than existential variables in tactic mode or type inference/unification)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Dec 03 2020 at 15:30):

Given how it's implemented, it's conforting.

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC