Karolin Varner (Mar 29 2021 at 07:25): Karolin Varner (Mar 29 2021 at 07:25):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?
Meven Lennon-Bertrand (Mar 29 2021 at 09:03):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.
Meven Lennon-Bertrand (Mar 29 2021 at 09:05):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.
Théo Winterhalter (Mar 29 2021 at 09:07):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.
Matthieu Sozeau (Mar 29 2021 at 21:36):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 withshelve_unifiablecan be solved at some point using 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: Sep 23 2023 at 14:01 UTC