From 09782e1ccae26efe4350ca48b5cd5b1b868ab6ad Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Wed, 27 Sep 2023 13:10:26 +0200
Subject: [PATCH] =?UTF-8?q?Fixed=20iFrame=20under=20=E2=88=A7=20and=20?=
 =?UTF-8?q?=E2=88=A8=20taking=20forever=20to=20fail=20in=20the=20presence?=
 =?UTF-8?q?=20of=20evars,=20second=20option?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/proofmode/class_instances_frame.v | 20 ++++++++++++--------
 iris/proofmode/classes.v               |  4 ++--
 tests/proofmode.v                      | 24 ++++++++++++++++++++++++
 3 files changed, 38 insertions(+), 10 deletions(-)

diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index e3c78d51e..0af320b67 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -14,10 +14,14 @@ Implicit Types P Q R : PROP.
 goal. Otherwise we leave [emp] via [frame_here].
 Only if all those options fail, we start decomposing [R], via instances like
 [frame_exist]. To ensure that, all other instances must have cost > 1. *)
-Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
+Lemma frame_here_absorbing p R : Absorbing R → Frame p R R True.
 Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
-Global Instance frame_here p R : Frame p R R emp | 1.
+Lemma frame_here p R : Frame p R R emp.
 Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
+Global Instance frame_here_maybe_absorbing p R O :
+  TCIf (Absorbing R) (TCEq O True)%I (TCEq O emp)%I →
+  Frame p R R O | 0.
+Proof. case => [+->|->]; [apply frame_here_absorbing | apply frame_here]. Qed.
 Global Instance frame_affinely_here_absorbing p R :
   Absorbing R → Frame p (<affine> R) R True | 0.
 Proof.
@@ -59,20 +63,20 @@ Global Instance frame_pure_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
 Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
 
 Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
-  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → MakeSep Q1 Q2 Q' →
+  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → TCNoBackTrack (MakeSep Q1 Q2 Q') →
   Frame true R (P1 ∗ P2) Q' | 9.
 Proof.
-  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
+  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- [<-].
   rewrite {1}(intuitionistically_sep_dup R).
   by rewrite !assoc -(assoc _ _ _ Q1) -(comm _ Q1) assoc -(comm _ Q1).
 Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
-  Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
-Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
+  Frame false R P1 Q → TCNoBackTrack (MakeSep Q P2 Q') → Frame false R (P1 ∗ P2) Q' | 9.
+Proof. rewrite /Frame /MakeSep => <- [<-]. by rewrite assoc. Qed.
 Global Instance frame_sep_r p R P1 P2 Q Q' :
-  Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
+  Frame p R P2 Q → TCNoBackTrack (MakeSep P1 Q Q') → Frame p R (P1 ∗ P2) Q' | 10.
 Proof.
-  rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc.
+  rewrite /Frame /MakeSep => <- [<-]. by rewrite assoc -(comm _ P1) assoc.
 Qed.
 
 Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 94558ae4b..92b9b13a1 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -386,8 +386,8 @@ Global Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
   MaybeFrame true R P P false | 100.
 Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
 Global Instance maybe_frame_default {PROP : bi} (R P : PROP) :
-  TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
-Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
+  TCNoBackTrack (TCOr (Affine R) (Absorbing P)) → MaybeFrame false R P P false | 100.
+Proof. intros [?]. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
 
 Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
 Global Arguments IntoExcept0 {_} _%I _%I : simpl never.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e9f7005e0..05bb0d23a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -651,6 +651,21 @@ 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 2 iFrame.
+Abort.
+Lemma test_iFrame_disjunction_4_evars `(Φ : nat → nat → PROP) P :
+  Φ 0 1 ∗ Φ 1 0 ⊢ ∃ n m, (Φ n m ∗ Φ 0 1) ∨ (P ∗ Φ m n).
+Proof.
+  iIntros "(HΦ1 & HΦ2)". iExists _, _.
+  iFrame "HΦ1". by iLeft.
+Qed.
 
 Lemma test_iFrame_conjunction_1 P Q :
   P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q).
@@ -667,6 +682,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.
-- 
GitLab