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.

Ignat Insarov (Mar 26 2021 at 15:58):

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.
  eapply Z.sub_add.
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: Apr 16 2024 at 13:01 UTC