As I mentioned in #62 (closed), I would like to get rid of the specialization pattern * and instead instantiate all universal quantifiers automatically when applying or destructing. This merge request implements that.
There is however one open issue: when destructing a persistent hypothesis we have to decide when to keep the original and when to remove it. To illustrate why, consider having the following hypothesis in the persistent context:
H : ∀ x, P x ∨ Q xClearly, when doing an iDestruct we would like to keep the original. After all, we may want to instantiate it with different values for x. However, when having a disjunction that is not universally quantified, it is safe to remove the original because it does not lead to loss of information.
The current heuristic for determining whether to keep a hypothesis is rather stupid: it only copies when variables are explicitly instantiated, i.e. when having a non-empty list x1 ... xn in the below.
iDestruct ("H" $! x1 ... xn)Now that we automatically instantiate universal quantifiers, this heuristic may not be the best idea anymore.
Any ideas for a better heuristic?