Morning! I am going through the coq doc at the moment; I am pretty sure I get what shelve_unifiable does, but why would I ever want to use it given that any goals it applies to can be trivially resolved?

I am not sure why you think the goal you shelve with `shelve_unifiable`

should be trivially resolved? The general idea of `shelve_unifiable`

is to avoid having to instantiate by hand existential variables when their values can be deduced by the instance given to further variables. This is by default performed under the hood by most tactics generating existential variables. A typical example is tactic `eexists`

: to solve a goal of the form `exists x, P(x)`

, it generates two existential variables, the first one of which is shelved, and the second corresponding to a goal `P(?x)`

. Solving that goal might involve multiple steps, invocations of lemmatas, etc. But in the end along with proving `P(?x)`

it stepwise constructs a value for `?x`

without you ever needing to provide said value.

Maybe the manual is misleading here: `Goals that appear in the type of other goals can be solved by unification.`

means that those variables that are shelved with `shelve_unifiable`

can be solved *at some point* using unification, but not necessarily right away.

I would even dare say (almost) never right away, if they can already be solved by unification, they will be solved and thus not be goals I think.

Meven Lennon-Bertrand said:

Maybe the manual is misleading here:

`Goals that appear in the type of other goals can be solved by unification.`

means that those variables that are shelved with`shelve_unifiable`

can be solvedat some pointusing unification, but not necessarily right away.

But it's also `not necessarily at any time`

if it happens that the dependency disappears... So, `might be solved by unification in subsequent proof steps`

would be more accurate.

Last updated: Jun 18 2024 at 08:01 UTC