iDestruct on a conjunction magically transforms hypothesis
The following proof script
Lemma test_True_conj :
(@bi_emp PROP ∧ True) -∗ True.
Proof.
iIntros "H". iDestruct "H" as "[_ H]".
results in the following goal:
"H" : <affine> True
--------------------------------------∗
True
Notice how an "affinely" modality showed up suddenly. When I first saw this happen, I spent some minutes following notations and definitions to figure out where I had typed that modality without noticing. However, it turns out I did not -- the proof mode actually magically transforms my assertions! I think this is a bug.
Mostly, this is a bug because it's not at all what the user would expect. If you ask someone what iDestruct "H" as "[_ H]".
does -- even someone familiar with the proof mode, even someone like me who thought about linear Iris quite a bit -- the answer would be "it applies and_elim_r
". End of story. This is what the tactic does in Coq, and it is also what it does in the "old" IPM.
It is never a good idea to defy user expectations like that.
Also, I felt we had a pretty strong sense when designing the original IPM that we wouldn't mess with the users assertions unless we're asked to do so. I think that's one of the reasons IPM works so well -- it does plenty of magic under the hood, but you don't see it doing magic -- the effect of the magic is that whatever you think should happen, happens. We ask the user to be explicit about moving things to the persistent context, we ask them to be explicit about maintaining the current modality (like \later or the updates) when doing iApply
. There was one exception around True
, where True -* P
behaves exactly like P
in some cases, and it was pretty confusing and AFAIK was entirely removed.
So, please, let's stick to that. We have have plenty of things that are surprising to people. We should keep that to an absolute minimum.
@robbertkrebbers argued that this is about information loss. I don't even get the argument: Of course not all tactics we apply are bidirectional! Information loss is even frequently the explicit purpose of a tactic, like clear
or destruct foo as [_ foo]
. In the above goal, the user can write iDestruct "H" as "#[_ H]"
if they want to remember that there are no resources here. I'm actually a little surprised this works, it seems to detect the emp /\
as "affinely" even though I did not spell it that way?
I just noticed one can also write iDestruct "H" as "[_ #H]"
. I'm pretty surprised that this works, because it seems to rely on the other conjunct that I already dropped -- but I'm not really offended by things "magically" working the way I told them to work. That's a totally different surprise than "I told it to do one thing and it did that and also painted my house blue".