[Coq-Club] how to instantiate existential variables

[Jeremy Dawson]

Hi,

thanks for all the answers to my previous question.

FWIW, actually simpl seems to rewrite a goal without instantiating evars

Another question about evars:
given a goal

Γ1 ++ l ++ A :: Γ2 ++ B :: Γ3 = ?Γ1 ++ ?A :: ?Γ2 ++ ?B :: ?Γ3

how do I instantiate ?A to A and ?B to B?

I've tried
instantiate (?A := A).
and
instantiate (A := A).
but both those produce error mes

[Jason Gross]

You can instantiate them by number

instantiate (4 := B). instantiate (2 := A). This is not very satisfying,
but it works.

Post by Jeremy Dawson
Hi,
thanks for all the answers to my previous question.
FWIW, actually simpl seems to rewrite a goal without instantiating evars
given a goal
Γ1 ++ l ++ A :: Γ2 ++ B :: Γ3 = ?Γ1 ++ ?A :: ?Γ2 ++ ?B :: ?Γ3
how do I instantiate ?A to A and ?B to B?
I've tried
instantiate (?A := A).
and
instantiate (A := A).
but both those produce error messages.
thanks
Jeremy

[Théo Zimmermann]

You need to explicitly name existential variables (with the `?[x]`
syntax, e.g. `refine (?[A] ?[B])` if you want to be able to refer to
them by name later on, with instantiate, or with the named goal selector
`[x]: ` (see
https://coq.inria.fr/refman/proof-engine/ltac.html#goal-selectors and,
in 8.9,
https://coq.inria.fr/distrib/V8.9+beta1/refman/proof-engine/proof-handling.html#navigation-in-the-proof-tree).

Théo

Post by Jason Gross
You can instantiate them by number
instantiate (4 := B).  instantiate (2 := A).  This is not very
satisfying, but it works.
Hi,
thanks for all the answers to my previous question.
FWIW, actually simpl seems to rewrite a goal without instantiating evars
given a goal
  Γ1 ++ l ++ A :: Γ2 ++ B :: Γ3 = ?Γ1 ++ ?A :: ?Γ2 ++ ?B :: ?Γ3
how do I instantiate ?A to A and ?B to B?
I've tried
instantiate (?A := A).
and
instantiate (A := A).
but both those produce error messages.
thanks
Jeremy

[Jean-Christophe Léchenet]

Note that there is an open issue on Github about the unclear error
message when you try to manipulate an evar whose name was not manually
set: https://github.com/coq/coq/issues/4633.

Jean-Christophe

Post by Jeremy Dawson
Hi,
thanks for all the answers to my previous question.
FWIW, actually simpl seems to rewrite a goal without instantiating evars
given a goal
Γ1 ++ l ++ A :: Γ2 ++ B :: Γ3 = ?Γ1 ++ ?A :: ?Γ2 ++ ?B :: ?Γ3
how do I instantiate ?A to A and ?B to B?
I've tried
instantiate (?A := A).
and
instantiate (A := A).
but both those produce error messages.
thanks
Jeremy