Commit 383fee40 authored by Robbert Krebbers's avatar Robbert Krebbers

No longer allow ownership of persistent elements to be split.

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.
parent 572e4e50
...@@ -354,12 +354,19 @@ Proof. by rewrite /FromSep big_sepL_app. Qed. ...@@ -354,12 +354,19 @@ Proof. by rewrite /FromSep big_sepL_app. Qed.
(* FromOp *) (* FromOp *)
Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a b) a b. Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a b) a b.
Proof. by rewrite /FromOp. Qed. Proof. by rewrite /FromOp. Qed.
Global Instance from_op_persistent {A : cmraT} (a : A) :
Persistent a FromOp a a a. (* TODO: Worst case there could be a lot of backtracking on these instances,
Proof. intros. by rewrite /FromOp -(persistent_dup a). Qed. try to refactor. *)
Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) : 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'). FromOp a b1 b2 FromOp a' b1' b2' FromOp (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed. 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 : Global Instance from_op_Some {A : cmraT} (a : A) b1 b2 :
FromOp a b1 b2 FromOp (Some a) (Some b1) (Some b2). FromOp a b1 b2 FromOp (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed. Proof. by constructor. Qed.
...@@ -367,13 +374,18 @@ Proof. by constructor. Qed. ...@@ -367,13 +374,18 @@ Proof. by constructor. Qed.
(* IntoOp *) (* IntoOp *)
Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a b) a b. Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a b) a b.
Proof. by rewrite /IntoOp. Qed. 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) : 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 b1 b2 IntoOp a' b1' b2'
IntoOp (a,a') (b1,b1') (b2,b2'). IntoOp (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed. 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 : Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
IntoOp a b1 b2 IntoOp (Some a) (Some b1) (Some b2). IntoOp a b1 b2 IntoOp (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed. Proof. by constructor. Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment