Fixed iFrame under ∧ and ∨ taking forever to fail in the presence of evars

iris/proofmode/class_instances_frame.v

@@ -110,13 +110,13 @@ Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
 (unlike with [∗] where we can only frame it in one conjunct).
 We require at least one of those to make progress though. *)
 Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
-  MaybeFrame p R P1 Q1 progress1 →
-  MaybeFrame p R P2 Q2 progress2 →
+  TCNoBackTrack (MaybeFrame p R P1 Q1 progress1) →
+  TCNoBackTrack (MaybeFrame p R P2 Q2 progress2) →
   TCEq (progress1 || progress2) true →
   MakeAnd Q1 Q2 Q' →
   Frame p R (P1 ∧ P2) Q' | 9.
 Proof.
-  rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-.
+  rewrite /MaybeFrame /Frame /MakeAnd => [[<-]] [<-] _ <-.
   apply and_intro; [rewrite and_elim_l|rewrite and_elim_r]; done.
 Qed.
 
@@ -135,19 +135,21 @@ If Coq would memorize the results of type class resolution, the solution with
 multiple instances would be preferred (and more Prolog-like). *)
 
 Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
-  MaybeFrame false R P1 Q1 progress1 → MaybeFrame false R P2 Q2 progress2 →
+  TCNoBackTrack (MaybeFrame false R P1 Q1 progress1) →
+  TCNoBackTrack (MaybeFrame false R P2 Q2 progress2) →
   TCOr (TCEq (progress1 && progress2) true) (TCOr
     (TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
     (TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) →
   MakeOr Q1 Q2 Q →
   Frame false R (P1 ∨ P2) Q | 9.
-Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
+Proof. rewrite /Frame /MakeOr => [[<-]] [<-] _ <-. by rewrite -sep_or_l. Qed.
 
 Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
-  MaybeFrame true R P1 Q1 progress1 → MaybeFrame true R P2 Q2 progress2 →
+  TCNoBackTrack (MaybeFrame true R P1 Q1 progress1) →
+  TCNoBackTrack (MaybeFrame true R P2 Q2 progress2) →
   TCEq (progress1 || progress2) true →
   MakeOr Q1 Q2 Q → Frame true R (P1 ∨ P2) Q | 9.
-Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
+Proof. rewrite /Frame /MakeOr => [[<-]] [<-] _ <-. by rewrite -sep_or_l. Qed.
 
 Global Instance frame_wand p R P1 P2 Q2 :
   Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2) | 2.

tests/proofmode.v

@@ -651,6 +651,15 @@ Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
 Proof. intros ?. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
 Lemma test_iFrame_disjunction_2 P : P -∗ (True ∨ True) ∗ P.
 Proof. iIntros "HP". iFrame "HP". auto. Qed.
+Lemma test_iFrame_disjunction_3_evars `(Φ : nat → PROP) P1 P2 P3 P4 :
+  BiAffine PROP →
+  let n := 5 in
+  let R := fun a => Nat.iter n (fun P => (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a) ∨ P)%I (Φ a) in
+  P1 ⊢ ∃ a, R a.
+Proof.
+  intros ?. cbn. iIntros "HP1". iExists _.
+  Timeout 1 iFrame.
+Abort.
 
 Lemma test_iFrame_conjunction_1 P Q :
   P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q).
@@ -667,6 +676,15 @@ Proof.
   (* [iFrame] should simplify [False ∧ Q] to just [False]. *)
   Show.
 Abort.
+Lemma test_iFrame_conjunction_4_evars `(Φ : nat → PROP) P1 P2 P3 P4 P5 :
+  BiAffine PROP →
+  let n := 5 in
+  let R := fun a => Nat.iter n (fun P => (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a) ∧ P)%I (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a)%I in
+  P5 ⊢ ∃ a, R a.
+Proof.
+  intros ?. cbn. iIntros "HP1". iExists _.
+  Timeout 1 iFrame.
+Abort.
 
 Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.