From f9c04d5d4b859c59f8f7f760479fb2d638b827d2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Jun 2023 16:25:40 +0200
Subject: [PATCH] make sure CombineSepAs prefers AsFractional over own

---
 iris/base_logic/lib/own.v   | 3 ++-
 iris/base_logic/proofmode.v | 3 ++-
 iris/proofmode/classes.v    | 6 +++++-
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 2be0458d2..a3505b059 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -376,8 +376,9 @@ Section proofmode_instances.
   Proof. intros. by rewrite /FromSep -own_op -is_op. Qed.
   (* TODO: Improve this instance with generic own simplification machinery
   once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  (* Cost > 50 to give priority to [combine_sep_as_fractional. *)
   Global Instance combine_sep_as_own γ a b1 b2 :
-    IsOp a b1 b2 → CombineSepAs (own γ b1) (own γ b2) (own γ a).
+    IsOp a b1 b2 → CombineSepAs (own γ b1) (own γ b2) (own γ a) | 60.
   Proof. intros. by rewrite /CombineSepAs -own_op -is_op. Qed.
   (* TODO: Improve this instance with generic own validity simplification
   machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
diff --git a/iris/base_logic/proofmode.v b/iris/base_logic/proofmode.v
index 01cfda354..fd0b72159 100644
--- a/iris/base_logic/proofmode.v
+++ b/iris/base_logic/proofmode.v
@@ -26,9 +26,10 @@ Section class_instances.
   Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
   (* TODO: Improve this instance with generic own simplification machinery
   once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
+  (* Cost > 50 to give priority to [combine_sep_as_fractional. *)
   Global Instance combine_sep_as_ownM (a b1 b2 : M) :
     IsOp a b1 b2 →
-    CombineSepAs (uPred_ownM b1) (uPred_ownM b2) (uPred_ownM a).
+    CombineSepAs (uPred_ownM b1) (uPred_ownM b2) (uPred_ownM a) | 60.
   Proof. intros. by rewrite /CombineSepAs -ownM_op -is_op. Qed.
   (* TODO: Improve this instance with generic own validity simplification
   machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 6fdc67828..3ed21c2e9 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -273,7 +273,11 @@ Note that [FromSep] and [CombineSepAs] have nearly the same definition. However,
 they have different Hint Modes and are used for different tactics. [FromSep] is
 used to compute the two new goals obtained after applying [iSplitL]/[iSplitR],
 taking the current goal as input. [CombineSepAs] is used to combine two
-hypotheses into one. *)
+hypotheses into one.
+
+In terms of costs, note that the [AsFractional] instance for [CombineSepAs]
+has cost 50. If that instance should take priority over yours, make sure to use
+a higher cost. *)
 Class CombineSepAs {PROP : bi} (P Q R : PROP) := combine_sep_as : P ∗ Q ⊢ R.
 Global Arguments CombineSepAs {_} _%I _%I _%I : simpl never.
 Global Arguments combine_sep_as {_} _%I _%I _%I {_}.
-- 
GitLab