From 39fe55fe4e3a63e8431eb00bde96c733bcb5bc56 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 May 2016 13:11:56 +0200
Subject: [PATCH] Make iDestruct more powerful for destructing ghost ownership.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It is now able to destruct:
- [own γ (a1 ⋅ a1)] into [own γ a1] and [own γ a2]
- [own γ a] into [own γ a] and [own γ a] if [a] is persistent
- [own γ (a,b)] by proceeding recursively.
- [own γ (Some a)] by preceeding resursively.
---
 proofmode/coq_tactics.v     | 28 ++++++++++++++++++++++++----
 proofmode/ghost_ownership.v |  6 +++---
 2 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 7a308038c..72737d70d 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -717,14 +717,34 @@ Qed.
 Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
   sep_destruct : □?p P ⊢ □?p (Q1 ★ Q2).
 Arguments sep_destruct : clear implicits.
+Class OpDestruct {A : cmraT} (a b1 b2 : A) :=
+  op_destruct : a ≡ b1 ⋅ b2.
+Arguments op_destruct {_} _ _ _ {_}.
+
+Global Instance op_destruct_op {A : cmraT} (a b : A) : OpDestruct (a â‹… b) a b.
+Proof. by rewrite /OpDestruct. Qed.
+Global Instance op_destruct_persistent {A : cmraT} (a : A) :
+  Persistent a → OpDestruct a a a.
+Proof. intros; apply (persistent_dup a). Qed.
+Global Instance op_destruct_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  OpDestruct a b1 b2 → OpDestruct a' b1' b2' →
+  OpDestruct (a,a') (b1,b1') (b2,b2').
+Proof. by constructor. Qed.
+Global Instance op_destruct_Some {A : cmraT} (a : A) b1 b2 :
+  OpDestruct a b1 b2 → OpDestruct (Some a) (Some b1) (Some b2).
+Proof. by constructor. Qed.
+
 Lemma sep_destruct_spatial p P Q1 Q2 : P ⊢ (Q1 ★ Q2) → SepDestruct p P Q1 Q2.
 Proof. rewrite /SepDestruct=> ->. by rewrite always_if_sep. Qed.
 
 Global Instance sep_destruct_sep p P Q : SepDestruct p (P ★ Q) P Q.
-Proof. by apply sep_destruct_spatial. Qed.
-Global Instance sep_destruct_ownM p (a b : M) :
-  SepDestruct p (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b).
-Proof. apply sep_destruct_spatial. by rewrite ownM_op. Qed.
+Proof. rewrite /SepDestruct. by rewrite always_if_sep. Qed.
+Global Instance sep_destruct_ownM p (a b1 b2 : M) :
+  OpDestruct a b1 b2 →
+  SepDestruct p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  rewrite /OpDestruct /SepDestruct=> ->. by rewrite ownM_op always_if_sep.
+Qed.
 
 Global Instance sep_destruct_and P Q : SepDestruct true (P ∧ Q) P Q.
 Proof. by rewrite /SepDestruct /= always_and_sep. Qed.
diff --git a/proofmode/ghost_ownership.v b/proofmode/ghost_ownership.v
index 496b63049..87b8e0ef3 100644
--- a/proofmode/ghost_ownership.v
+++ b/proofmode/ghost_ownership.v
@@ -6,9 +6,9 @@ Section ghost.
 Context `{inG Λ Σ A}.
 Implicit Types a b : A.
 
-Global Instance sep_destruct_own p γ a b :
-  SepDestruct p (own γ (a ⋅ b)) (own γ a) (own γ b).
-Proof. apply sep_destruct_spatial. by rewrite own_op. Qed.
+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.
 Global Instance sep_split_own γ a b :
   SepSplit (own γ (a ⋅ b)) (own γ a) (own γ b) | 90.
 Proof. by rewrite /SepSplit own_op. Qed.
-- 
GitLab