Stream: Coq devs & plugin devs

Topic: ✔ eexists without intro causes scoping errors


view this post on Zulip Davide F (Aug 02 2024 at 07:16):

Given the following goal:

Goal forall (y: Prop), exists (F: Prop -> Prop), (fun x => F x) = (fun x => y).

I can intro y, eexists ?[F'] and call reflexivity, so that the two sides
of the equality are unified. This unification succeeds since F' has y in its
scope.

Another possibility to introduce the unification variable F' is to call
eexists ?[F'] without introing y. This produces the new goal where y is
in the context and the occurrences of F are replaced with the fresh
unification variable F'. What I do not understand is why in this second
approach, F' has not y in its scope. I imagine it is because the tactic
quantifies F' before y, but is it not misleading?

Below the full example

Goal forall (y: Prop), exists (F: Prop -> Prop), (fun x => F x) = (fun x => y).
  intro y. (* comment this line to see the different behaviour *)
  eexists ?[F'].
  Set Printing Existential Instances.
  reflexivity.
Abort.

view this post on Zulip Théo Winterhalter (Aug 02 2024 at 07:41):

Why would you expect it to work without introducing y? I would find that very surprising if it did.

view this post on Zulip Davide F (Aug 02 2024 at 07:47):

It seems that coq does some intro for me, so I was thinking that eexists ?[X'] is the same as intros; eexists ?[X'].
In this case, X' should have the intro variables in scope.

Maybe I'm misunderstanding the tactic eexists:)

view this post on Zulip Guillaume Melquiond (Aug 02 2024 at 07:47):

The important point is that eexists ?[F'] is actually the composition of two more primitive operations: evar (F' : ...) and exists F'. The former will take only the current context into consideration (it cannot do otherwise), while the latter will actually introduce y.

view this post on Zulip Davide F (Aug 02 2024 at 07:51):

I think I understand now what coq does now! Thanks you

view this post on Zulip Notification Bot (Aug 02 2024 at 07:51):

Davide F has marked this topic as resolved.


Last updated: Oct 13 2024 at 01:02 UTC