This is my code:

```
Definition g6 (x: ℤ): {y | f y = x}.
Proof.
unfold f. refine (exist _ _ _).
(* x : ℤ *)
(* ============================ *)
(* ?Goal + 1 = x *)
```

I do not understand what `?Goal`

is and how to work with it. For example, I can assert something similar:

```
assert (∃ pseudoGoal', pseudoGoal' + 1 = x) as ExistsSimilarThing.
* eexists ?[pseudoGoal]. instantiate (pseudoGoal := x - 1). ring.
* destruct ExistsSimilarThing as [z SimilarThing].
(* x, z : ℤ *)
(* SimilarThing : z + 1 = x *)
(* ============================ *)
(* ?Goal + 1 = x *)
exact SimilarThing.
(* Error: *)
(* In environment *)
(* x, z : ℤ *)
(* SimilarThing : z + 1 = x *)
(* The term "SimilarThing" has type "z + 1 = x" while it is expected to have type *)
(* "?Goal + 1 = x". *)
```

Not working! What am I doing wrong?

In your last script, the tactic `exact`

does not work because it is not authorized to instantiate existential variables. This is to avoid unwanted instantiations, however in your case you can use `eexact`

instead. This tactic allows instantiation of existential variables, like similar tactics prefixed by e such as `eexists`

, `eassumption`

, etc.

that's wrong though

Well, `eexact`

gives a different error, so that is some progress.

the problem is that ?goal is created before `z`

, so you can't use `z`

to fill it

Yes, this is what the new error says… Turns out there is a shelved goal №2 of type `ℤ`

and I think `?Goal`

refers to that one.

Yes, it is indeed the case. Here the easy solution would be to move your `assert`

before using `refine`

(that creates this existential variables to fill the `_`

).

In general, existential variables are used to handled "terms with holes". Those can appear either when you do not provide some parts of a term (as in your argument to `refine`

), or in a proof (which is represented internally as such a term with holes, with each goal corresponding to a hole).

Thanks, I get it! I did not know that `?Goal`

refers to the shelved goal №2 created by `refine`

. Knowing that, it sort of makes sense.

The tricky thing with existential variables is that to handle the fact that terms appear in a context, they need to keep track of the context they were created in, and trying to instantiate them with things outside of that context raises annoying errors like the one you encountered with `eexact`

.

And, also, I should mention that not all existential variables are presented by Coq as goals. If some can be deduced from later goals they are "shelved", with the hope that their value can be obtained indirectly.

How would that work?

This `?Goal`

is exactly a shelved goal, and I would like to obtain its value indirectly.

Exactly! Your `exists`

actually creates three existential variables, one per `_`

. The first one is instantiated right away because of the type constraint. The second one is shelved, and this is `?Goal`

. The third is presented to you as a goal, mentioning `?Goal`

. Now solving that goal should require you to provide a term that would allow deducing the value of `?Goal`

.

If you wish to avoid this shelving behaviour for any reason, you can either use the `Unshelve`

command that unshelves all currently shelved variables, or `unshelve tac`

that performs `tac`

and unshelves all variables it generates.

In your case, using `unshelve (refine (exist _ _ _)).`

would give you two goals, the first of which is of type Z, corresponding to `?Goal`

that normally gets shelved.

you don't need parentheses around refine

Yes, I just discovered what `unshelve`

does. So, there is no way to solve the goal corresponding to the third hole before the second one?

I was hoping that I could use `auto`

and let Coq find out that `x - 1`

is a suitable value for `?Goal`

, but for that to happen it needs to know that `?Goal + 1 = x`

, and this knowledge is not visible from the second hole.

Indeed, `auto`

is sadly not that smart… And I do not think there are tactics able to do this kind of things.

Things like `lia`

, `ring`

, `field`

are good at deciding whether a given goal is valid or not, but they are not smart enough to instantiate existential variables.

And I am not aware of solutions that would be able to do that.

I see. Thanks!

In your case, however, you can still get around a bit more manually if you are enclined to look for the right lemmas in the library, by letting Coq construct `?Goal`

by solving the goal it provides you with those lemmas.

```
Definition g6 (x: Z): {y | f y = x}.
Proof.
eexists.
unfold f.
eapply Z.sub_add.
Defined.
Eval compute in (proj1_sig (g6 4)). (* 3 *)
```

`eexists`

is exactly the same as your `refine (exist _ _ _)`

. Then I use lemma `Z.sub_add`

to solve the goal, and doing so provides a value for the shelved existential.

Or even:

```
Definition g6 (x: ℤ): {y | f y = x}.
Proof. unfold f. eexists. eauto using Z.sub_add. Qed.
```

This works as well, indeed.

So, in principle it is possible, I only need to provide the right elements.

If the expression is simple enough and you locate the right lemmas, it might work, yes

A new hope! :smiley_cat:

I think you don't need eexists there, eauto does it for you

Last updated: Jun 16 2024 at 01:42 UTC