Make MaybeFrame shorthand notation for TCNoBackTrack MaybeFrame'

iris/proofmode/class_instances_frame.v

@@ -59,14 +59,11 @@ 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' :
-  (* This [MaybeFrame] does not really have to be guarded by [TCNoBacktrack]:
-    if the first [Frame] instance can be satisfied, this instance will
-    be successfully constructed, regardless of the [progress]. *)
-  Frame true R P1 Q1 → TCNoBackTrack (MaybeFrame true R P2 Q2 progress) →
+  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress →
   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.
@@ -122,18 +119,19 @@ _fail_ to construct a [Frame] instance. This happens especially when the
 resource we are framing in contains evars, since Coq's typeclass search
 does more backtracking in this case.
 
-To combat this, the [∧] and [∨] instances use [MaybeFrame] classes guarded
-by a [TCNoBackTrack]. The [MaybeFrame] clauses for the subterms output a
-boolean [progress] indicator, on which some condition is posed. The
-[TCNoBackTrack] ensures that when this condition is not met, Coq will not
-backtrack on the [MaybeFrame] clauses to consider different [progress]es. *)
+To combat this, the [∧] and [∨] instances use [MaybeFrame] classes---
+a notation for [MaybeFrame'] guarded by a [TCNoBackTrack]. The [MaybeFrame]
+clauses for the subterms output a boolean [progress] indicator, on which some
+condition is posed. The [TCNoBackTrack] ensures that when this condition is not
+met, Coq will not backtrack on the [MaybeFrame] clauses to consider different
+[progress]es. *)
 
 (* For framing below [∧], we can frame [R] away in *both* conjuncts
 (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' :
-  TCNoBackTrack (MaybeFrame p R P1 Q1 progress1) →
-  TCNoBackTrack (MaybeFrame p R P2 Q2 progress2) →
+  MaybeFrame p R P1 Q1 progress1 →
+  MaybeFrame p R P2 Q2 progress2 →
   (* If below [TCEq] fails, the [frame_and] instance is immediately abandoned:
     the [TCNoBackTrack]s above prevent Coq from considering other ways to
     construct [MaybeFrame] instances. *)
@@ -141,7 +139,7 @@ Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
   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.
 
@@ -165,12 +163,13 @@ multiple instances would be preferred (and more Prolog-like). *)
 This instance does _not_ framing spatial resources when they can be framed in
 exactly one side, since that can make your goal unprovable. *)
 Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
-  TCNoBackTrack (MaybeFrame false R P1 Q1 progress1) →
-  TCNoBackTrack (MaybeFrame false R P2 Q2 progress2) →
+  MaybeFrame false R P1 Q1 progress1 →
+  MaybeFrame false R P2 Q2 progress2 →
   (* Below [TCOr] encodes the condition described above. If this condition
     cannot be satisfied, the [frame_or_spatial] instance is immediately
-    abandoned: the [TCNoBackTrack]s above prevent Coq from considering other
-    ways to construct [MaybeFrame] instances. *)
+    abandoned: the [TCNoBackTrack]s present in the [MaybeFrame] notation
+    prevent Coq from considering other ways to construct [MaybeFrame']
+    instances. *)
   TCOr (TCEq (progress1 && progress2) true) (TCOr
     (TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
     (TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) →
@@ -182,11 +181,12 @@ Proof. rewrite /Frame /MakeOr => [[<-]] [<-] _ <-. by rewrite -sep_or_l. Qed.
 on _at least_ one side. This does not affect provability of your goal,
 since you can keep the resource after framing. *)
 Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
-  TCNoBackTrack (MaybeFrame true R P1 Q1 progress1) →
-  TCNoBackTrack (MaybeFrame true R P2 Q2 progress2) →
-  (* If below [TCEq] fails, the [frame_and] instance is immediately abandoned:
-    the [TCNoBackTrack]s above prevent Coq from considering other ways to
-    construct [MaybeFrame] instances. *)
+  MaybeFrame true R P1 Q1 progress1 →
+  MaybeFrame true R P2 Q2 progress2 →
+  (* If below [TCEq] fails, the [frame_or_persistent] instance is immediately
+    abandoned: the [TCNoBackTrack]s present in the [MaybeFrame] notation
+    prevent Coq from considering other ways to construct [MaybeFrame']
+    instances. *)
   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.

iris/proofmode/classes.v

@@ -372,22 +372,28 @@ Global Hint Mode Frame + + ! ! - : typeclass_instances.
 (* The boolean [progress] indicates whether actual framing has been performed.
 If it is [false], then the default instance [maybe_frame_default] below has been
 used. *)
-Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
+Class MaybeFrame' {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
   maybe_frame : □?p R ∗ Q ⊢ P.
-Global Arguments MaybeFrame {_} _ _%I _%I _%I _.
+Global Arguments MaybeFrame' {_} _ _%I _%I _%I _.
 Global Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
-Global Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
+Global Hint Mode MaybeFrame' + + ! - - - : typeclass_instances.
 
 Global Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
-  Frame p R P Q → MaybeFrame p R P Q true.
+  Frame p R P Q → MaybeFrame' p R P Q true.
 Proof. done. Qed.
 
 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.
+  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.
+  TCOr (Affine R) (Absorbing P) → MaybeFrame' false R P P false | 100.
+Proof. intros. rewrite /MaybeFrame' /=. apply: sep_elim_r. Qed.
+
+(* We never want to backtrack on instances of [MaybeFrame']. We provide
+a notation for [MaybeFrame'] wrapped in the [TCNoBackTrack] construct.
+For more details, see also iris!989 and the [frame_and] and [frame_or_spatial]
+instances in [class_instances_frame.v] *)
+Notation MaybeFrame p R P Q progress := (TCNoBackTrack (MaybeFrame' p R P Q progress)).
 
 Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
 Global Arguments IntoExcept0 {_} _%I _%I : simpl never.