Merge FromOp and IntoOp into IsOp and perform some tweak the modes.

theories/algebra/auth.v

@@ -248,11 +248,8 @@ Arguments authR : clear implicits.
 Arguments authUR : clear implicits.
 
 (* Proof mode class instances *)
-Instance from_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
-  FromOp a b1 b2 → FromOp (◯ a) (◯ b1) (◯ b2).
-Proof. done. Qed.
-Instance into_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
-  IntoOp a b1 b2 → IntoOp (◯ a) (◯ b1) (◯ b2).
+Instance is_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
+  IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
 Proof. done. Qed.
 
 (* Functor *)

theories/algebra/frac.v

@@ -50,7 +50,5 @@ Proof. done. Qed.
 Lemma frac_valid' (p : Qp) : ✓ p ↔ (p ≤ 1%Qp)%Qc.
 Proof. done. Qed.
 
-Global Instance frac_into_op q : IntoOp q (q/2)%Qp (q/2)%Qp.
-Proof. by rewrite /IntoOp frac_op' Qp_div_2. Qed.
-Global Instance frac_from_op q : FromOp q (q/2)%Qp (q/2)%Qp.
-Proof. by rewrite /FromOp frac_op' Qp_div_2. Qed.
\ No newline at end of file
+Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
+Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.

theories/algebra/frac_auth.v

@@ -89,23 +89,14 @@ Section frac_auth.
   Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯!{1} a ⋅ ◯!{q} b) → False.
   Proof. rewrite -frag_auth_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
 
-  Global Instance into_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
-    IntoOp q q1 q2 → IntoOp a a1 a2 → IntoOp (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
-  Proof. by rewrite /IntoOp=> /leibniz_equiv_iff -> ->. Qed.
-  Global Instance from_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
-    FromOp q q1 q2 → FromOp a a1 a2 → FromOp (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
-  Proof. by rewrite /FromOp=> /leibniz_equiv_iff <- <-. Qed.
-
-  Global Instance into_op_frac_auth_persistent (q q1 q2 : frac) (a  : A) :
-    Persistent a → IntoOp q q1 q2 → IntoOp (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
-  Proof.
-    rewrite /IntoOp=> ? /leibniz_equiv_iff ->.
-    by rewrite -frag_auth_op -persistent_dup.
-  Qed.
-  Global Instance from_op_frac_auth_persistent (q q1 q2 : frac) (a : A) :
-    Persistent a → FromOp q q1 q2 → FromOp (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
+  Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
+    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
+  Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
+
+  Global Instance is_op_frac_auth_persistent (q q1 q2 : frac) (a  : A) :
+    Persistent a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
   Proof.
-    rewrite /FromOp=> ? /leibniz_equiv_iff <-.
+    rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
     by rewrite -frag_auth_op -persistent_dup.
   Qed.
 

theories/base_logic/lib/auth.v

@@ -74,21 +74,21 @@ Section auth.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
 
   Global Instance from_and_auth_own γ a b1 b2 :
-    FromOp a b1 b2 →
+    IsOp a b1 b2 →
     FromAnd false (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
-  Proof. rewrite /FromOp /FromAnd=> <-. by rewrite auth_own_op. Qed.
+  Proof. rewrite /IsOp /FromAnd=> ->. by rewrite auth_own_op. Qed.
   Global Instance from_and_auth_own_persistent γ a b1 b2 :
-    FromOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+    IsOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
     FromAnd true (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 91.
   Proof.
     intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
-    by rewrite -auth_own_op from_op.
+    by rewrite -auth_own_op -is_op.
   Qed.
 
   Global Instance into_and_auth_own p γ a b1 b2 :
-    IntoOp a b1 b2 →
+    IsOp a b1 b2 →
     IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
-  Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) auth_own_op. Qed.
+  Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) auth_own_op. Qed.
 
   Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
   Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.

theories/base_logic/lib/own.v

@@ -187,16 +187,16 @@ Section proofmode_classes.
   Implicit Types a b : A.
 
   Global Instance into_and_own p γ a b1 b2 :
-    IntoOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
-  Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) own_op. Qed.
+    IsOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) own_op. Qed.
   Global Instance from_and_own γ a b1 b2 :
-    FromOp a b1 b2 → FromAnd false (own γ a) (own γ b1) (own γ b2).
-  Proof. intros. by rewrite /FromAnd -own_op from_op. Qed.
+    IsOp a b1 b2 → FromAnd false (own γ a) (own γ b1) (own γ b2).
+  Proof. intros. by rewrite /FromAnd -own_op -is_op. Qed.
   Global Instance from_and_own_persistent γ a b1 b2 :
-    FromOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+    IsOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
     FromAnd true (own γ a) (own γ b1) (own γ b2).
   Proof.
     intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
-    by rewrite -own_op from_op.
+    by rewrite -own_op -is_op.
   Qed.
 End proofmode_classes.

theories/proofmode/class_instances.v

@@ -355,15 +355,15 @@ Proof.
 Qed.
 
 Global Instance from_sep_ownM (a b1 b2 : M) :
-  FromOp a b1 b2 →
+  IsOp a b1 b2 →
   FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /FromAnd -ownM_op from_op. Qed.
+Proof. intros. by rewrite /FromAnd -ownM_op -is_op. Qed.
 Global Instance from_sep_ownM_persistent (a b1 b2 : M) :
-  FromOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+  IsOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
   FromAnd true (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof.
   intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
-  by rewrite -ownM_op from_op.
+  by rewrite -ownM_op -is_op.
 Qed.
 
 Global Instance from_sep_bupd P Q1 Q2 :
@@ -389,51 +389,28 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M
 Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
 
 (* FromOp *)
-Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a ⋅ b) a b | 100.
-Proof. by rewrite /FromOp. Qed.
-
 (* TODO: Worst case there could be a lot of backtracking on these instances,
 try to refactor. *)
-Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
-  FromOp a b1 b2 → FromOp a' b1' b2' → FromOp (a,a') (b1,b1') (b2,b2').
-Proof. by constructor. Qed.
-Global Instance from_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
-  Persistent a → FromOp a' b1' b2' → FromOp (a,a') (a,b1') (a,b2').
-Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
-Global Instance from_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
-  Persistent a' → FromOp a b1 b2 → FromOp (a,a') (b1,a') (b2,a').
-Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
-
-Global Instance from_op_Some {A : cmraT} (a : A) b1 b2 :
-  FromOp a b1 b2 → FromOp (Some a) (Some b1) (Some b2).
-Proof. by constructor. Qed.
-
-(* IntoOp *)
-Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a ⋅ b) a b.
-Proof. by rewrite /IntoOp. Qed.
-
-Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
-  IntoOp a b1 b2 → IntoOp a' b1' b2' →
-  IntoOp (a,a') (b1,b1') (b2,b2').
+Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  IsOp' a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
 Proof. by constructor. Qed.
-Global Instance into_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
-  Persistent a → IntoOp a' b1' b2' → IntoOp (a,a') (a,b1') (a,b2').
+Global Instance is_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
+  Persistent a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
 Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
-Global Instance into_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
-  Persistent a' → IntoOp a b1 b2 → IntoOp (a,a') (b1,a') (b2,a').
+Global Instance is_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
+  Persistent a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
 Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
 
-Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
-  IntoOp a b1 b2 → IntoOp (Some a) (Some b1) (Some b2).
+Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
+  IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
 Proof. by constructor. Qed.
 
 (* IntoAnd *)
 Global Instance into_and_sep p P Q : IntoAnd p (P ∗ Q) P Q.
 Proof. by apply mk_into_and_sep. Qed.
 Global Instance into_and_ownM p (a b1 b2 : M) :
-  IntoOp a b1 b2 →
-  IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) ownM_op. Qed.
+  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) ownM_op. Qed.
 
 Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q.
 Proof. done. Qed.

theories/proofmode/classes.v

@@ -108,15 +108,36 @@ Lemma mk_into_and_sep {M} p (P Q1 Q2 : uPred M) :
   (P ⊢ Q1 ∗ Q2) → IntoAnd p P Q1 Q2.
 Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
 
-Class FromOp {A : cmraT} (a b1 b2 : A) := from_op : b1 ⋅ b2 ≡ a.
-Arguments from_op {_} _ _ _ {_}.
-Hint Mode FromOp + ! - - : typeclass_instances.
-Hint Mode FromOp + - ! ! : typeclass_instances. (* For iCombine *)
-
-Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2.
-Arguments into_op {_} _ _ _ {_}.
-(* No [Hint Mode] since we want to turn [?x] into [?x1 ⋅ ?x2], for example
-when having [H : own ?x]. *)
+(* There are various versions of [IsOp] with different modes:
+
+- [IsOp a b1 b2]: this one has no mode, it can be used regardless of whether
+  any of the arguments is an evar. This class has only one direct instance:
+  [IsOp (a ⋅ b) a b].
+- [IsOp' a b1 b2]: requires either [a] to start with a constructor, OR [b1] and
+  [b2] to start with a constructor. All usual instances should be of this
+  class to avoid loops.
+- [IsOp'LR a b1 b2]: requires either [a] to start with a constructor. This one
+  has just one instance: [IsOp'LR (a ⋅ b) a b] with a very low precendence.
+  This is important so that when performing, for example, an [iDestruct] on
+  [own γ (q1 + q2)] where [q1] and [q2] are fractions, we actually get
+  [own γ q1] and [own γ q2] instead of [own γ ((q1 + q2)/2)] twice.
+*)
+Class IsOp {A : cmraT} (a b1 b2 : A) := is_op : a ≡ b1 ⋅ b2.
+Arguments is_op {_} _ _ _ {_}.
+Hint Mode IsOp + - - - : typeclass_instances.
+
+Instance is_op_op {A : cmraT} (a b : A) : IsOp (a ⋅ b) a b | 100.
+Proof. by rewrite /IsOp. Qed.
+
+Class IsOp' {A : cmraT} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
+Hint Mode IsOp' + ! - - : typeclass_instances.
+Hint Mode IsOp' + - ! ! : typeclass_instances.
+
+Class IsOp'LR {A : cmraT} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
+Existing Instance is_op_lr | 0.
+Hint Mode IsOp'LR + ! - - : typeclass_instances.
+Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a ⋅ b) a b | 0.
+Proof. by rewrite /IsOp'LR /IsOp. Qed.
 
 Class Frame {M} (p : bool) (R P Q : uPred M) := frame : □?p R ∗ Q ⊢ P.
 Arguments frame {_ _} _ _ _ {_}.