## Stream: Coq users

### Topic: How to solve `?Goal`?

#### Ignat Insarov (Mar 26 2021 at 15:01):

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?

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:25):

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.

#### Gaëtan Gilbert (Mar 26 2021 at 15:27):

that's wrong though

#### Ignat Insarov (Mar 26 2021 at 15:28):

Well, `eexact` gives a different error, so that is some progress.

#### Gaëtan Gilbert (Mar 26 2021 at 15:28):

the problem is that ?goal is created before `z`, so you can't use `z` to fill it

#### Ignat Insarov (Mar 26 2021 at 15:30):

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.

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:31):

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 `_`).

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:33):

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).

#### Ignat Insarov (Mar 26 2021 at 15:36):

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.

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:37):

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`.

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:38):

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.

#### Ignat Insarov (Mar 26 2021 at 15:38):

How would that work?

#### Ignat Insarov (Mar 26 2021 at 15:39):

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

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:40):

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`.

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:42):

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.

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:44):

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.

#### Gaëtan Gilbert (Mar 26 2021 at 15:44):

you don't need parentheses around refine

#### Ignat Insarov (Mar 26 2021 at 15:46):

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?

#### Ignat Insarov (Mar 26 2021 at 15:47):

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.

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:50):

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

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:51):

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.

#### Meven Lennon-Bertrand (Mar 26 2021 at 15:52):

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

I see. Thanks!

#### Meven Lennon-Bertrand (Mar 26 2021 at 16:04):

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.

#### Meven Lennon-Bertrand (Mar 26 2021 at 16:04):

``````Definition g6 (x: Z): {y | f y = x}.
Proof.
eexists.
unfold f.
Defined.

Eval compute in (proj1_sig (g6 4)). (* 3 *)
``````

#### Meven Lennon-Bertrand (Mar 26 2021 at 16:06):

`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.

#### Ignat Insarov (Mar 26 2021 at 16:07):

Or even:

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

#### Meven Lennon-Bertrand (Mar 26 2021 at 16:07):

This works as well, indeed.

#### Ignat Insarov (Mar 26 2021 at 16:07):

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

#### Meven Lennon-Bertrand (Mar 26 2021 at 16:07):

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

#### Ignat Insarov (Mar 26 2021 at 16:10):

A new hope! :smiley_cat:

#### Gaëtan Gilbert (Mar 26 2021 at 16:12):

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

Last updated: Jun 16 2024 at 01:42 UTC