instantiating existentials

Using Coq
#1

Hi,

I'm having difficulty using the tactic

  Variant instantiate (num := term)

because I get

lja_dd_ImpL_p < instantiate (0 := l).
Toplevel input, characters 1-21:
> instantiate (0 := l).
> ^^^^^^^^^^^^^^^^^^^^
Error:
Ltac call to "instantiate ( (int) := (lglob) ) (hloc)" failed.
Incorrect existential variable index.

lja_dd_ImpL_p < instantiate (1 := l).
Toplevel input, characters 0-20:
> instantiate (1 := l).
> ^^^^^^^^^^^^^^^^^^^^
Error:
Ltac call to "instantiate ( (int) := (lglob) ) (hloc)" failed.
Not enough uninstantiated existential variables.

Are existential variables numbered from 0 or from 1?

And what am I doing wrong?

Thanks

Jeremy

#2

Hi Jeremy,

The documentation says that the index is relative to the position of the existential variable in the goal. It starts at 1. Can you show your goal or ideally even provide a minimal example to be able to reproduce your situation?

BTW, if you can use named existentials, e.g. by using the ?[x] syntax when creating them, then you will benefit from the ability to use named goal selectors to instantiate your existential variables, which should lead to more robust proof scripts.

#3

Hi Theo,

I may have misunderstood the terminology since the existential variable
does not appear in the conclusion of the goal but in a hypothesis
(called n). After I do revert n. it seems to work OK.

Does “goal” here mean just the conclusion?

When such a variable is instantiated, I had assumed that it is
instantiated everywhere it appears, is that correct?

Cheers,

Jeremy

#4

Indeed, “goal” can be confusing since in this case it means only the conclusion (I have opened a PR clarifying the doc). If you want to instantiate an existential variable appearing in a hypothesis, you can use the variant instantiate (1 := l) in n.