Define FromOp type class and use it in the proof mode.

proofmode/class_instances.v

@@ -132,6 +132,10 @@ Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
 (* FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ★ P2) P1 P2 | 100.
 Proof. done. Qed.
+Global Instance from_sep_ownM (a b1 b2 : M) :
+  FromOp a b1 b2 →
+  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /FromSep -ownM_op from_op. Qed.
 Global Instance from_sep_always P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
 Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
@@ -142,9 +146,6 @@ Global Instance from_sep_rvs P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|=r=> P) (|=r=> Q1) (|=r=> Q2).
 Proof. rewrite /FromSep=><-. apply rvs_sep. Qed.
 
-Global Instance from_sep_ownM (a b : M) :
-  FromSep (uPred_ownM (a ⋅ b)) (uPred_ownM a) (uPred_ownM b) | 99.
-Proof. by rewrite /FromSep ownM_op. Qed.
 Global Instance from_sep_big_sepM
     `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
   (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
@@ -160,6 +161,20 @@ Proof.
   rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
 Qed.
 
+(* FromOp *)
+Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a ⋅ b) a b.
+Proof. by rewrite /FromOp. Qed.
+Global Instance from_op_persistent {A : cmraT} (a : A) :
+  Persistent a → FromOp a a a.
+Proof. intros. by rewrite /FromOp -(persistent_dup a). Qed.
+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_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.

proofmode/classes.v

@@ -39,6 +39,9 @@ Global Arguments into_and : clear implicits.
 Lemma mk_into_and_sep p P Q1 Q2 : (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.
+Global Arguments from_op {_} _ _ _ {_}.
+
 Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2.
 Global Arguments into_op {_} _ _ _ {_}.
 

proofmode/ghost_ownership.v

@@ -9,7 +9,7 @@ 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.
-Global Instance from_sep_own γ a b :
-  FromSep (own γ (a ⋅ b)) (own γ a) (own γ b) | 90.
-Proof. by rewrite /FromSep own_op. Qed.
+Global Instance from_sep_own γ a b1 b2 :
+  FromOp a b1 b2 → FromSep (own γ a) (own γ b1) (own γ b2).
+Proof. intros. by rewrite /FromSep -own_op from_op. Qed.
 End ghost.