diff --git a/algebra/coPset.v b/algebra/coPset.v index dd86f3b41b6e909af10f1e9fe8607d57d6fa9c17..cc3aa38d21a9bb4e84e45a49c1d82d380e6743e1 100644 --- a/algebra/coPset.v +++ b/algebra/coPset.v @@ -1,15 +1,68 @@ From iris.algebra Require Export cmra. From iris.algebra Require Import updates local_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. *) +(* The union CMRA *) +Section coPset. + Implicit Types X Y : coPset. + + Canonical Structure coPsetC := leibnizC coPset. + + Instance coPset_valid : Valid coPset := λ _, True. + Instance coPset_op : Op coPset := union. + Instance coPset_pcore : PCore coPset := λ _, Some ∅. + + Lemma coPset_op_union X Y : X ⋅ Y = X ∪ Y. + Proof. done. Qed. + Lemma coPset_core_empty X : core X = ∅. + Proof. done. Qed. + Lemma coPset_included X Y : X ≼ Y ↔ X ⊆ Y. + Proof. + split. + - intros [Z ->]. rewrite coPset_op_union. set_solver. + - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z. + Qed. + + Lemma coPset_ra_mixin : RAMixin coPset. + Proof. + apply ra_total_mixin; eauto. + - solve_proper. + - solve_proper. + - solve_proper. + - intros X1 X2 X3. by rewrite !coPset_op_union assoc_L. + - intros X1 X2. by rewrite !coPset_op_union comm_L. + - intros X. by rewrite coPset_op_union coPset_core_empty left_id_L. + - intros X1 X2 _. by rewrite coPset_included !coPset_core_empty. + Qed. + Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin. + + Lemma coPset_ucmra_mixin : UCMRAMixin coPset. + Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed. + Canonical Structure coPsetUR := + discreteUR coPset coPset_ra_mixin coPset_ucmra_mixin. + + Lemma coPset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY. + Proof. destruct mY; by rewrite /= ?right_id_L. Qed. + + Lemma coPset_update X Y : X ~~> Y. + Proof. done. Qed. + + Lemma coPset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf. + Proof. + intros (Z&->&?)%subseteq_disjoint_union_L. + intros; apply local_update_total; split; [done|]; simpl. + intros mZ _. rewrite !coPset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX. + Qed. +End coPset. + +(* The disjoiny union CMRA *) Inductive coPset_disj := | CoPset : coPset → coPset_disj | CoPsetBot : coPset_disj. -Section coPset. +Section coPset_disj. Arguments op _ _ !_ !_ /. Canonical Structure coPset_disjC := leibnizC coPset_disj. @@ -27,7 +80,7 @@ Section coPset. repeat (simpl || case_decide); first [apply (f_equal CoPset)|done|exfalso]; set_solver by eauto. - Lemma coPset_included X Y : CoPset X ≼ CoPset Y ↔ X ⊆ Y. + Lemma coPset_disj_included X Y : CoPset X ≼ CoPset Y ↔ X ⊆ Y. Proof. split. - move=> [[Z|]]; simpl; try case_decide; set_solver. @@ -60,4 +113,4 @@ Section coPset. 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. +End coPset_disj. diff --git a/algebra/gset.v b/algebra/gset.v index cfbc7d21bd023e36011496c4283d7e2c7ce31c6b..4bd7d5a42c08d2240e16ca494f3c79613102348e 100644 --- a/algebra/gset.v +++ b/algebra/gset.v @@ -2,13 +2,68 @@ From iris.algebra Require Export cmra. From iris.algebra Require Import updates local_updates. From iris.prelude Require Export collections gmap. +(* The union CMRA *) +Section gset. + Context `{Countable K}. + Implicit Types X Y : gset K. + + Canonical Structure gsetC := leibnizC (gset K). + + Instance gset_valid : Valid (gset K) := λ _, True. + Instance gset_op : Op (gset K) := union. + Instance gset_pcore : PCore (gset K) := λ _, Some ∅. + + Lemma gset_op_union X Y : X ⋅ Y = X ∪ Y. + Proof. done. Qed. + Lemma gset_core_empty X : core X = ∅. + Proof. done. Qed. + Lemma gset_included X Y : X ≼ Y ↔ X ⊆ Y. + Proof. + split. + - intros [Z ->]. rewrite gset_op_union. set_solver. + - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z. + Qed. + + Lemma gset_ra_mixin : RAMixin (gset K). + Proof. + apply ra_total_mixin; eauto. + - solve_proper. + - solve_proper. + - solve_proper. + - intros X1 X2 X3. by rewrite !gset_op_union assoc_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 X1 X2 _. by rewrite gset_included !gset_core_empty. + Qed. + Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin. + + Lemma gset_ucmra_mixin : UCMRAMixin (gset K). + Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed. + Canonical Structure gsetUR := + discreteUR (gset K) gset_ra_mixin gset_ucmra_mixin. + + Lemma gset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY. + Proof. destruct mY; by rewrite /= ?right_id_L. Qed. + + Lemma gset_update X Y : X ~~> Y. + Proof. done. Qed. + + Lemma gset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf. + Proof. + intros (Z&->&?)%subseteq_disjoint_union_L. + intros; apply local_update_total; split; [done|]; simpl. + intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX. + Qed. +End gset. + +(* The disjoint union CMRA *) Inductive gset_disj K `{Countable K} := | GSet : gset K → gset_disj K | GSetBot : gset_disj K. Arguments GSet {_ _ _} _. Arguments GSetBot {_ _ _}. -Section gset. +Section gset_disj. Context `{Countable K}. Arguments op _ _ !_ !_ /. @@ -28,7 +83,7 @@ Section gset. repeat (simpl || case_decide); first [apply (f_equal GSet)|done|exfalso]; set_solver by eauto. - Lemma coPset_included X Y : GSet X ≼ GSet Y ↔ X ⊆ Y. + Lemma gset_disj_included X Y : GSet X ≼ GSet Y ↔ X ⊆ Y. Proof. split. - move=> [[Z|]]; simpl; try case_decide; set_solver. @@ -63,7 +118,7 @@ Section gset. Arguments op _ _ _ _ : simpl never. - Lemma gset_alloc_updateP_strong P (Q : gset_disj K → Prop) X : + Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K → Prop) X : (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) → (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q. Proof. @@ -74,43 +129,46 @@ Section gset. - apply HQ; set_solver by eauto. - apply gset_disj_valid_op. set_solver by eauto. Qed. - Lemma gset_alloc_updateP_strong' P X : + Lemma gset_disj_alloc_updateP_strong' P X : (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) → GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X ∧ P i. - Proof. eauto using gset_alloc_updateP_strong. Qed. + Proof. eauto using gset_disj_alloc_updateP_strong. Qed. - Lemma gset_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) : + Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) : (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) → (∀ i, P i → Q (GSet {[i]})) → GSet ∅ ~~>: Q. Proof. - intros. apply (gset_alloc_updateP_strong P); eauto. + intros. apply (gset_disj_alloc_updateP_strong P); eauto. intros i; rewrite right_id_L; auto. Qed. - Lemma gset_alloc_empty_updateP_strong' P : + Lemma gset_disj_alloc_empty_updateP_strong' P : (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) → GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i. - Proof. eauto using gset_alloc_empty_updateP_strong. Qed. + Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed. Section fresh_updates. Context `{Fresh K (gset K), !FreshSpec K (gset K)}. - Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X : + Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X : (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q. Proof. - intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto. + intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto. intros Y ?; exists (fresh Y); eauto using is_fresh. Qed. - Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X. - Proof. eauto using gset_alloc_updateP. Qed. + Lemma gset_disj_alloc_updateP' X : + GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X. + Proof. eauto using gset_disj_alloc_updateP. Qed. - Lemma gset_alloc_empty_updateP (Q : gset_disj K → Prop) : + Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K → Prop) : (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q. - Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed. - Lemma gset_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}. - Proof. eauto using gset_alloc_empty_updateP. Qed. + Proof. + intro. apply gset_disj_alloc_updateP. intros i; rewrite right_id_L; auto. + Qed. + Lemma gset_disj_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}. + Proof. eauto using gset_disj_alloc_empty_updateP. Qed. End fresh_updates. - Lemma gset_alloc_local_update X i Xf : + Lemma gset_disj_alloc_local_update X i Xf : i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf). Proof. intros ??; apply local_update_total; split; simpl. @@ -118,13 +176,13 @@ Section gset. - intros mZ ?%gset_disj_valid_op HXf. rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver. Qed. - Lemma gset_alloc_empty_local_update i Xf : + Lemma gset_disj_alloc_empty_local_update i Xf : i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf). Proof. intros. rewrite -(right_id_L _ _ {[i]}). - apply gset_alloc_local_update; set_solver. + apply gset_disj_alloc_local_update; set_solver. Qed. -End gset. +End gset_disj. Arguments gset_disjR _ {_ _}. Arguments gset_disjUR _ {_ _}. diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v index 9611cd2bb46752cc3eb0ed72aeda13a73dc42539..28fa844df19a5ae1408ebaf7b0909941ff4b199d 100644 --- a/heap_lang/lib/ticket_lock.v +++ b/heap_lang/lib/ticket_lock.v @@ -141,7 +141,7 @@ Section proof. - wp_cas_suc. iDestruct "Hainv" as (s) "[Ho %]"; subst. iVs (own_update with "Ho") as "Ho". - { eapply auth_update_no_frag, (gset_alloc_empty_local_update n). + { eapply auth_update_no_frag, (gset_disj_alloc_empty_local_update n). rewrite elem_of_seq_set; omega. } iDestruct "Ho" as "[Hofull Hofrag]". iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]"). diff --git a/program_logic/ownership.v b/program_logic/ownership.v index f59c7af6fe158f124e9987a945d40f7d0ee7c92b..aa42399a2fbe6873124186e7564ef59ca25d4d8b 100644 --- a/program_logic/ownership.v +++ b/program_logic/ownership.v @@ -156,7 +156,7 @@ Proof. iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]". iVs (own_empty (A:=gset_disjUR positive) disabled_name) as "HE". iVs (own_updateP with "HE") as "HE". - { apply (gset_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)). + { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)). intros E. destruct (Hfresh (E ∪ dom _ I)) as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. } iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?). diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v index 85f075ff9b7468e48e5043f5f8d3838404905833..d3126bf039879f208136c7e9d9201b3d50aaffd5 100644 --- a/program_logic/thread_local.v +++ b/program_logic/thread_local.v @@ -56,7 +56,7 @@ Section proofs. iVs (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty". iVs (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]". { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)). - apply (gset_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)). + apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)). intros Ef. exists (coPpick (nclose N ∖ coPset.of_gset Ef)). rewrite -coPset.elem_of_of_gset comm -elem_of_difference. apply coPpick_elem_of=> Hfin.