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.
Why would you expect it to work without introducing y
? I would find that very surprising if it did.
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
:)
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
.
I think I understand now what coq does now! Thanks you
Davide F has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC