ghost_ownership.v 556 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8
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 Λ Σ A}.
Implicit Types a b : A.

9 10 11
Global Instance sep_destruct_own p γ a b1 b2 :
  OpDestruct a b1 b2  SepDestruct p (own γ a) (own γ b1) (own γ b2).
Proof. rewrite /OpDestruct /SepDestruct => ->. by rewrite own_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14 15
Global Instance sep_split_own γ a b :
  SepSplit (own γ (a  b)) (own γ a) (own γ b) | 90.
Proof. by rewrite /SepSplit own_op. Qed.
End ghost.