"iFrame" sometimes fails to frame assertions piece-by-piece but succeeds to frame them all at once
A test says more than a thousand words:
Section tests.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Lemma test_iFrame_or `{!BiAffine PROP} P Q R : P -∗ Q -∗ R ∨ (P ∗ Q).
Proof.
iIntros "HP HQ". Fail iFrame "HP HQ".
iCombine "HP HQ" as "H". iFrame "H".
Qed.
The first iFrame
fails since it only makes progress under one arm of the disjunction, and our current heuristic is that we accept framing under ∨ only if
- it makes progress under both arms, or
- one arm is solved completely
But those heuristics violate the principle that you can frame things incrementally. We have never stated that principle, but we implement iFrame "H1 H2 H3"
as a loop framing things incrementally, so this is a reasonable principle to expect.
Now, IIRC we've arrived at these semantics since it used to be the case that iFrame
worked under ∨
in cases where that was not clearly desirable. So it's not clear that we have a good solution here. But it might be worth to experiment with the approach where we frame under ∨
if either arm makes progress, similar to what we do for ∧
?