CMRA structure on gsets that avoids the indirection via maps.

Also, add algebra/gset to _CoqProject.

_CoqProject

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

algebra/gset.v

-From iris.algebra Require Export gmap.
-From iris.algebra Require Import excl.
-From iris.prelude Require Import mapset.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import updates.
+From iris.prelude Require Export collections gmap.
 
-Definition gsetC K `{Countable K} := gmapC K (exclC unitC).
-
-Definition to_gsetC `{Countable K} (X : gset K) : gsetC K :=
-  to_gmap (Excl ()) X.
+Inductive gset_disj K `{Countable K} :=
+  | GSet : gset K → gset_disj K
+  | GSetBot : gset_disj K.
+Arguments GSet {_ _ _} _.
+Arguments GSetBot {_ _ _}.
 
 Section gset.
-Context `{Countable K}.
-Implicit Types X Y : gset K.
-
-Lemma to_gsetC_empty : to_gsetC (∅ : gset K) = ∅.
-Proof. apply to_gmap_empty. Qed.
-Lemma to_gsetC_union X Y : X ⊥ Y → to_gsetC X ⋅ to_gsetC Y = to_gsetC (X ∪ Y).
-Proof.
-  intros HXY; apply: map_eq=> i; rewrite /to_gsetC /=.
-  rewrite lookup_op !lookup_to_gmap. repeat case_option_guard; set_solver.
-Qed.
-Lemma to_gsetC_valid X : ✓ to_gsetC X.
-Proof. intros i. rewrite /to_gsetC lookup_to_gmap. by case_option_guard. Qed.
-Lemma to_gsetC_valid_op X Y : ✓ (to_gsetC X ⋅ to_gsetC Y) ↔ X ⊥ Y.
-Proof.
-  split; last (intros; rewrite to_gsetC_union //; apply to_gsetC_valid).
-  intros HXY i ??; move: (HXY i); rewrite lookup_op !lookup_to_gmap.
-  rewrite !option_guard_True //.
-Qed.
-
-Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma updateP_alloc_strong (Q : gsetC K → Prop) (I : gset K) X :
-  (∀ i, i ∉ X → i ∉ I → Q (to_gsetC ({[i]} ∪ X))) → to_gsetC X ~~>: Q.
-Proof.
-  intros; apply updateP_alloc_strong with I (Excl ()); [done|]=> i.
-  rewrite /to_gsetC lookup_to_gmap_None -to_gmap_union_singleton; eauto.
-Qed.
-Lemma updateP_alloc (Q : gsetC K → Prop) X :
-  (∀ i, i ∉ X → Q (to_gsetC ({[i]} ∪ X))) → to_gsetC X ~~>: Q.
-Proof. move=>??. eapply updateP_alloc_strong with (I:=∅); by eauto. Qed.
-Lemma updateP_alloc_strong' (I : gset K) X :
-  to_gsetC X ~~>: λ Y : gsetC K, ∃ i, Y = to_gsetC ({[ i ]} ∪ X) ∧ i ∉ I ∧ i ∉ X.
-Proof. eauto using updateP_alloc_strong. Qed.
-Lemma updateP_alloc' X :
-  to_gsetC X ~~>: λ Y : gsetC K, ∃ i, Y = to_gsetC ({[ i ]} ∪ X) ∧ i ∉ X.
-Proof. eauto using updateP_alloc. Qed.
-End gset.
+  Context `{Countable K}.
+  Arguments op _ _ !_ !_ /.
+
+  Canonical Structure gset_disjC := leibnizC (gset_disj K).
+
+  Instance gset_disj_valid : Valid (gset_disj K) := λ X,
+    match X with GSet _ => True | GSetBot => False end.
+  Instance gset_disj_empty : Empty (gset_disj K) := GSet ∅.
+  Instance gset_disj_op : Op (gset_disj K) := λ X Y,
+    match X, Y with
+    | GSet X, GSet Y => if decide (X ⊥ Y) then GSet (X ∪ Y) else GSetBot
+    | _, _ => GSetBot
+    end.
+  Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some ∅.
+
+  Ltac gset_disj_solve :=
+    repeat (simpl || case_decide);
+    first [apply (f_equal GSet)|done|exfalso]; set_solver by eauto.
+
+  Lemma gset_disj_valid_inv_l X Y : ✓ (GSet X ⋅ Y) → ∃ Y', Y = GSet Y' ∧ X ⊥ Y'.
+  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
+  Lemma gset_disj_union X Y : X ⊥ Y → GSet X ⋅ GSet Y = GSet (X ∪ Y).
+  Proof. intros. by rewrite /= decide_True. Qed.
+  Lemma gset_disj_valid_op X Y : ✓ (GSet X ⋅ GSet Y) ↔ X ⊥ Y.
+  Proof. simpl. case_decide; by split. Qed.
+
+  Lemma gset_disj_ra_mixin : RAMixin (gset_disj K).
+  Proof.
+    apply ra_total_mixin; eauto.
+    - intros [?|]; destruct 1; gset_disj_solve.
+    - by constructor.
+    - by destruct 1.
+    - intros [X1|] [X2|] [X3|]; gset_disj_solve.
+    - intros [X1|] [X2|]; gset_disj_solve.
+    - intros [X|]; gset_disj_solve.
+    - exists (GSet ∅); gset_disj_solve.
\ No newline at end of file
+    - intros [X1|] [X2|]; gset_disj_solve.
+  Qed.
+  Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.
+
+  Lemma gset_disj_ucmra_mixin : UCMRAMixin (gset_disj K).
+  Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
+  Canonical Structure gset_disjUR :=
+    discreteUR (gset_disj K) gset_disj_ra_mixin gset_disj_ucmra_mixin.
+
+  Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
+  Arguments op _ _ _ _ : simpl never.
+
+  Lemma updateP_alloc_strong (Q : gset_disj K → Prop) (I : gset K) X :
+    (∀ i, i ∉ X → i ∉ I → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
+  Proof.
+    intros HQ; apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
+    destruct (exist_fresh (X ∪ Y ∪ I)) as [i ?].
+    exists (GSet ({[ i ]} ∪ X)); split.
+    - apply HQ; set_solver by eauto.
+    - apply gset_disj_valid_op. set_solver by eauto.
+  Qed.
+  Lemma updateP_alloc (Q : gset_disj K → Prop) X :
+    (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
+  Proof. move=>??. eapply updateP_alloc_strong with (I:=∅); by eauto. Qed.
+  Lemma updateP_alloc_strong' (I : gset K) X :
+    GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ I ∧ i ∉ X.
+  Proof. eauto using updateP_alloc_strong. Qed.
+  Lemma updateP_alloc' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
+  Proof. eauto using updateP_alloc. Qed.
+End gset.