Diverging `iFrame` with predicate evar
This is a minimized version of a diverging iFrame
I found in Perennial:
Lemma test_iFrame_pred_evar (P Q : PROP) :
P -∗ ∃ (Φ : nat → PROP), ((∃ n, id (Φ n)) ∨ Q).
Proof. iIntros "HP". iExists _. iFrame "HP".
The goal at the time of framing is
"HP" : P
--------------------------------------∗
(∃ n : nat, id (?Goal n)) ∨ Q
All these components seem necessary: when I remove the disjunction, the exisential, or the id
, the divergence goes away.
In the trace, I can see that it is phantasizing a bigMS into existence, but I do not know why:
Debug: 1.1-1.1-1.1-1.1-1.12: simple apply @frame_instances.frame_big_sepMS_disj_union on
(Frame false P (id (?Goal a)) (?Ψ a)), 1 subgoal(s)
Debug:
1.1-1.1-1.1-1.1-1.12-1 : (Frame false P (([∗ mset] y ∈ ?X1, ?Φ y) ∗ ([∗ mset] y ∈ ?X2, ?Φ y)) (?Ψ a))
I think one part of the problem is that the extra id
means that (id (?Goal a))
does not start with an evar, so the !
is circumvented.