Commit 06c4bfe2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' into 'master'

Make the elements of gset persistent by changing the core



See merge request !11
parents 7d2b0a28 bfad9bff
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_core_self 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 gset_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
......
Supports Markdown
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