Frame instance for multiset union can interact badly with instantiating existential quantifiers
This is problematic:
From iris.proofmode Require Import proofmode.
Section test.
Context {PROP : bi}.
Lemma multiset_problem (P : PROP) : P ⊢ ∃ (X : gmultiset nat), [∗ mset] y ∈ X, False.
Proof.
iIntros "HP".
Fail Timeout 2 iFrame "HP".
Abort.
End test.
This happens because there is the following frame instance for framing inside a multiset union:
Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
In our multiset_problem
example, this instance will instantiate the evar ?X
with a union ?X1 ⊎ ?X2
. After two more steps, we encounter almost the same goal, and Frame
instance search will loop.
The instances for [∗ list]
do not suffer from this problem, since they are guarded by an IsCons
or IsApp
typeclass with proper Hint Mode
s.
To fix this, we could use the same approach: guard frame_big_sepMS_disj_union
with a new class IsUnion
.