CMRA structure on coPset.

_CoqProject

@@ -60,6 +60,7 @@ algebra/csum.v
 algebra/list.v
 algebra/updates.v
 algebra/gset.v
+algebra/coPset.v
 program_logic/model.v
 program_logic/adequacy.v
 program_logic/hoare_lifting.v

algebra/coPset.v

+From iris.algebra Require Export cmra.
+From iris.algebra Require Import updates.
+From iris.prelude Require Export collections coPset.
+
+(** This is pretty much the same as algebra/gset, but I was not able to
+generalize the construction without breaking canonical structures. *)
+
+Inductive coPset_disj :=
+  | CoPset : coPset → coPset_disj
+  | CoPsetBot : coPset_disj.
+
+Section coPset.
+  Arguments op _ _ !_ !_ /.
+  Canonical Structure coPset_disjC := leibnizC coPset_disj.
+
+  Instance coPset_disj_valid : Valid coPset_disj := λ X,
+    match X with CoPset _ => True | CoPsetBot => False end.
+  Instance coPset_disj_empty : Empty coPset_disj := CoPset ∅.
+  Instance coPset_disj_op : Op coPset_disj := λ X Y,
+    match X, Y with
+    | CoPset X, CoPset Y => if decide (X ⊥ Y) then CoPset (X ∪ Y) else CoPsetBot
+    | _, _ => CoPsetBot
+    end.
+  Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ∅.
+
+  Ltac coPset_disj_solve :=
+    repeat (simpl || case_decide);
+    first [apply (f_equal CoPset)|done|exfalso]; set_solver by eauto.
+
+  Lemma coPset_disj_valid_inv_l X Y :
+    ✓ (CoPset X ⋅ Y) → ∃ Y', Y = CoPset Y' ∧ X ⊥ Y'.
+  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
+  Lemma coPset_disj_union X Y : X ⊥ Y → CoPset X ⋅ CoPset Y = CoPset (X ∪ Y).
+  Proof. intros. by rewrite /= decide_True. Qed.
+  Lemma coPset_disj_valid_op X Y : ✓ (CoPset X ⋅ CoPset Y) ↔ X ⊥ Y.
+  Proof. simpl. case_decide; by split. Qed.
+
+  Lemma coPset_disj_ra_mixin : RAMixin coPset_disj.
+  Proof.
+    apply ra_total_mixin; eauto.
+    - intros [?|]; destruct 1; coPset_disj_solve.
+    - by constructor.
+    - by destruct 1.
+    - intros [X1|] [X2|] [X3|]; coPset_disj_solve.
+    - intros [X1|] [X2|]; coPset_disj_solve.
+    - intros [X|]; coPset_disj_solve.
+    - exists (CoPset ∅); coPset_disj_solve.
+    - intros [X1|] [X2|]; coPset_disj_solve.
+  Qed.
+  Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
+
+  Lemma coPset_disj_ucmra_mixin : UCMRAMixin coPset_disj.
+  Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
+  Canonical Structure coPset_disjUR :=
+    discreteUR coPset_disj coPset_disj_ra_mixin coPset_disj_ucmra_mixin.
+End coPset.