Stream: Coq users

Topic: How to solve `?Goal`?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 26 2021 at 15:27):

that's wrong though

view this post on Zulip Ignat Insarov (Mar 26 2021 at 15:28):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 _).

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Mar 26 2021 at 15:38):

How would that work?

view this post on Zulip Ignat Insarov (Mar 26 2021 at 15:39):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 26 2021 at 15:44):

you don't need parentheses around refine

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Meven Lennon-Bertrand (Mar 26 2021 at 15:52):

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

view this post on Zulip Ignat Insarov (Mar 26 2021 at 15:58):

I see. Thanks!

view this post on Zulip 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.

view this post on Zulip 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 *)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Meven Lennon-Bertrand (Mar 26 2021 at 16:07):

This works as well, indeed.

view this post on Zulip Ignat Insarov (Mar 26 2021 at 16:07):

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

view this post on Zulip 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

view this post on Zulip Ignat Insarov (Mar 26 2021 at 16:10):

A new hope! :smiley_cat:

view this post on Zulip Gaëtan Gilbert (Mar 26 2021 at 16:12):

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


Last updated: Feb 04 2023 at 21:02 UTC