Stream: Coq users

Topic: what is unshelving ?

walker (Mar 14 2022 at 16:39):

I am getting strange warning in coq:

There are shelved goals. Try using `Unshelve`.

But when I tried Unshelve it gives me two goals to prove both are nat which I am not sure how to deal with maybe zero is proof of nat ? but I don't know how to deal with that and why would that warning appear to start with:

The theroem I am trying to prove might not be helpful in figuring out what is the issue:

Lemma value_not_same_as_normal_form :
  exists v, value v /\ ~ normal_form step v.
Proof.
  eexists.
  split.
  - eapply v_funny.
  - unfold normal_form. intros H. apply H.
    eexists. apply ST_PlusConstConst. (* hear coq tells me I need to unshelve some goals which I don't understand*)

This is from PLF Small step chapter here: https://softwarefoundations.cis.upenn.edu/plf-current/Smallstep.html

Edit: after some fiddling apply O worked, but I would care to understand why did that happen.

Andrew Hirsch (Mar 14 2022 at 16:48):

When you use eexists (or perhaps eapply), Coq is generating some _unification variables_ for you. These essentially represent some term (in this case, a Nat), that Coq doesn't know anything about. Essentially, it says "I'll try to figure out what to put here later." However, figuring out the proof didn't tell it (enough) about the terms to actually come up with something concrete, so it's asking you to.

The best way to fix this is probably to change eexists into exists 0. Then, the apply ST_PlusConstConst will work on the concrete term 0 instead of some unknown term, so you won't have to figure out the term later.

Andrew Hirsch (Mar 14 2022 at 16:54):

Looking at the page you linked, this is probably happening when you use eapply v_funny.. At that point, it needs to figure out the value of n2. Since any number will work, it can't figure it out.

To be clear, what's happening with Unshelve is that Coq is happily turning any unification variables in the proof (like the unknown natural number) into goals and asking you to solve them. So when you use eapply v_funny above, it creates an unification variable for n2, and can't figure it out. Since you can't save any terms with unification variables, it asks you to fill in some concrete term there. Using Unshelve creates a goal for that concrete term, which you can then solve with apply 0, like you noticed.

walker (Mar 14 2022 at 16:56):

understood thanks!

Last updated: Sep 25 2023 at 12:01 UTC