Library iris.proofmode.ghost_ownership

From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export ghost_ownership.

Section ghost.
Context `{inG Λ Σ (gmapUR gname A)}.
Implicit Types a b : A.

Global Instance into_sep_own p γ a b1 b2 :
  IntoOp a b1 b2 → IntoSep p (own γ a) (own γ b1) (own γ b2).
Proof.
  rewrite /IntoOp /IntoSep. destruct p; rewrite //=; intros ->; rewrite own_op; auto.
  rewrite -(uPred.affine_affine (own _ b1)).
  rewrite -(uPred.affine_affine (own _ b2)).
    by rewrite uPred.relevant_affine_sep.
Qed.
Global Instance from_sep_own γ a b :
  FromSep (own γ (a ⋅ b)) (own γ a) (own γ b) | 90.
Proof. by rewrite /FromSep own_op. Qed.
End ghost.