iFrame sometimes needs to be called twice
Consider the following proof (written in the context of
Program Definition monPred_id (R : monPred) : monPred := MonPred (λ V, R V) _. Next Obligation. intros ? ???. eauto. Qed. Lemma test_iFrame_monPred_id (P Q R : monPred) i : (P i) ∗ (Q i) ∗ (R i) -∗ (P ∗ Q ∗ monPred_id R) i. Proof. iIntros "(? & ? & ?)". iFrame. iFrame. Qed.
Notice that I need to call
iFrame twice. That should not be necessary.
This lead to a bunch of additional rewrites being introduced when fixing the fallout from https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/154 because the
[$] specialization pattern stopped working (it does
iFrame just once, it seems).