From 383fee403e974515df84264f56c353da6bc54e16 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Mar 2017 00:16:13 +0100
Subject: [PATCH] No longer allow ownership of persistent elements to be split.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This could lead to awkward loops, for example, when having:

- As goal `own γ c` with `c` persistent, one could keep on
  `iSplit`ting the goal. Especially in (semi-)automated proof
  scripts this is annoying as it easily leads to loops.
- When having a hypothesis `own γ c` with `c` persistent, one
  could keep on `iDestruct`ing it.

To that end, this commit removes the `IntoOp` and `FromOp` instances
for persistent CMRA elements. Instead, we changed the instances for
pairs, so that one, for example, can still split `(a â‹… b, c)` with
`c` persistent.
---
 theories/proofmode/class_instances.v | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 1951230ad..467aa4387 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -354,12 +354,19 @@ Proof. by rewrite /FromSep big_sepL_app. 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.
+
+(* 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.
@@ -367,13 +374,18 @@ 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_persistent {A : cmraT} (a : A) :
-  Persistent a → IntoOp a a a.
-Proof. intros; apply (persistent_dup a). 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').
 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').
+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').
+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).
 Proof. by constructor. Qed.
-- 
GitLab