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