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

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.

understood thanks!

Last updated: Jun 24 2024 at 00:02 UTC