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.
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
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.
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.
Last updated: Feb 06 2023 at 12:04 UTC