diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v index 2be0458d2b628c0a3d47e2d5523c6099eec15e98..a3505b059e72ff158ae06328208f500d26e74d4b 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 01cfda35479376f2726f5df5b16b351fb188c53a..fd0b7215933b6ea5f45c3bfe7099522a30955f69 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 6fdc67828687d48a4192416d8061caa820dda72e..3ed21c2e9eea0e4f3530c9bf1a8cac639ef7d609 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 {_}.