Commit 3a70097c authored by Amin Timany's avatar Amin Timany

Make elements gset persistent.

We need to change the core of X from ∅ to X to make elements of gset persistent.
parent 282094bf
From iris.algebra Require Export cmra. From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates. From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections gmap. From iris.prelude Require Export collections gmap mapset.
(* The union CMRA *) (* The union CMRA *)
Section gset. Section gset.
...@@ -11,11 +11,11 @@ Section gset. ...@@ -11,11 +11,11 @@ Section gset.
Instance gset_valid : Valid (gset K) := λ _, True. Instance gset_valid : Valid (gset K) := λ _, True.
Instance gset_op : Op (gset K) := union. Instance gset_op : Op (gset K) := union.
Instance gset_pcore : PCore (gset K) := λ _, Some . Instance gset_pcore : PCore (gset K) := λ X, Some X.
Lemma gset_op_union X Y : X Y = X Y. Lemma gset_op_union X Y : X Y = X Y.
Proof. done. Qed. Proof. done. Qed.
Lemma gset_core_empty X : core X = . Lemma gset_core_self X : core X = X.
Proof. done. Qed. Proof. done. Qed.
Lemma gset_included X Y : X Y X Y. Lemma gset_included X Y : X Y X Y.
Proof. Proof.
...@@ -32,8 +32,7 @@ Section gset. ...@@ -32,8 +32,7 @@ Section gset.
- solve_proper. - solve_proper.
- intros X1 X2 X3. by rewrite !gset_op_union assoc_L. - intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
- intros X1 X2. by rewrite !gset_op_union comm_L. - intros X1 X2. by rewrite !gset_op_union comm_L.
- intros X. by rewrite gset_op_union gset_core_empty left_id_L. - intros X. by rewrite gset_op_union gset_core_self union_idemp_L.
- intros X1 X2 _. by rewrite gset_included !gset_core_empty.
Qed. Qed.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin. Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
...@@ -54,8 +53,15 @@ Section gset. ...@@ -54,8 +53,15 @@ Section gset.
intros; apply local_update_total; split; [done|]; simpl. intros; apply local_update_total; split; [done|]; simpl.
intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX. intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
Qed. Qed.
Global Instance gmap_persistent X : Persistent X.
Proof. by apply persistent_total; rewrite gset_core_self. Qed.
End gset. End gset.
Arguments gsetR _ {_ _}.
Arguments gsetUR _ {_ _}.
(* The disjoint union CMRA *) (* The disjoint union CMRA *)
Inductive gset_disj K `{Countable K} := Inductive gset_disj K `{Countable K} :=
| GSet : gset K gset_disj K | GSet : gset K gset_disj K
......
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