gset.v 7.64 KB
 Robbert Krebbers committed Jul 23, 2016 1 ``````From iris.algebra Require Export cmra. `````` Robbert Krebbers committed Jul 25, 2016 2 ``````From iris.algebra Require Import updates local_updates. `````` Amin Timany committed Sep 14, 2016 3 ``````From iris.prelude Require Export collections gmap mapset. `````` Robbert Krebbers committed Mar 29, 2016 4 `````` `````` Robbert Krebbers committed Sep 06, 2016 5 6 7 8 9 10 11 12 13 ``````(* 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. `````` Amin Timany committed Sep 14, 2016 14 `````` Instance gset_pcore : PCore (gset K) := λ X, Some X. `````` Robbert Krebbers committed Sep 06, 2016 15 16 17 `````` Lemma gset_op_union X Y : X ⋅ Y = X ∪ Y. Proof. done. Qed. `````` Amin Timany committed Sep 14, 2016 18 `````` Lemma gset_core_self X : core X = X. `````` Robbert Krebbers committed Sep 06, 2016 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 `````` 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. `````` Amin Timany committed Sep 14, 2016 35 `````` - intros X. by rewrite gset_core_self idemp_L. `````` Robbert Krebbers committed Sep 06, 2016 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 `````` 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. `````` Amin Timany committed Sep 14, 2016 56 `````` `````` Amin Timany committed Sep 14, 2016 57 `````` Global Instance gset_persistent X : Persistent X. `````` Amin Timany committed Sep 14, 2016 58 59 `````` Proof. by apply persistent_total; rewrite gset_core_self. Qed. `````` Robbert Krebbers committed Sep 06, 2016 60 61 ``````End gset. `````` Amin Timany committed Sep 14, 2016 62 63 64 ``````Arguments gsetR _ {_ _}. Arguments gsetUR _ {_ _}. `````` Robbert Krebbers committed Sep 06, 2016 65 ``````(* The disjoint union CMRA *) `````` Robbert Krebbers committed Jul 23, 2016 66 67 68 69 70 ``````Inductive gset_disj K `{Countable K} := | GSet : gset K → gset_disj K | GSetBot : gset_disj K. Arguments GSet {_ _ _} _. Arguments GSetBot {_ _ _}. `````` Robbert Krebbers committed Mar 29, 2016 71 `````` `````` Robbert Krebbers committed Sep 06, 2016 72 ``````Section gset_disj. `````` Robbert Krebbers committed Jul 23, 2016 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 `````` 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. `````` Robbert Krebbers committed Sep 06, 2016 92 `````` Lemma gset_disj_included X Y : GSet X ≼ GSet Y ↔ X ⊆ Y. `````` Robbert Krebbers committed Sep 01, 2016 93 94 95 96 97 98 `````` Proof. split. - move=> [[Z|]]; simpl; try case_decide; set_solver. - intros (Z&->&?)%subseteq_disjoint_union_L. exists (GSet Z). gset_disj_solve. Qed. `````` Robbert Krebbers committed Jul 23, 2016 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 `````` 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. - 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. Arguments op _ _ _ _ : simpl never. `````` Robbert Krebbers committed Sep 06, 2016 127 `````` Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K → Prop) X : `````` Robbert Krebbers committed Aug 01, 2016 128 129 `````` (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) → (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q. `````` Robbert Krebbers committed Jul 23, 2016 130 `````` Proof. `````` Robbert Krebbers committed Aug 01, 2016 131 132 133 `````` intros Hfresh HQ. apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]]. destruct (Hfresh (X ∪ Y)) as (i&?&?); first set_solver. `````` Robbert Krebbers committed Jul 23, 2016 134 135 136 137 `````` exists (GSet ({[ i ]} ∪ X)); split. - apply HQ; set_solver by eauto. - apply gset_disj_valid_op. set_solver by eauto. Qed. `````` Robbert Krebbers committed Sep 06, 2016 138 `````` Lemma gset_disj_alloc_updateP_strong' P X : `````` Robbert Krebbers committed Aug 01, 2016 139 140 `````` (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) → GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X ∧ P i. `````` Robbert Krebbers committed Sep 06, 2016 141 `````` Proof. eauto using gset_disj_alloc_updateP_strong. Qed. `````` Robbert Krebbers committed Jul 23, 2016 142 `````` `````` Robbert Krebbers committed Sep 06, 2016 143 `````` Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) : `````` Robbert Krebbers committed Aug 01, 2016 144 145 `````` (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) → (∀ i, P i → Q (GSet {[i]})) → GSet ∅ ~~>: Q. `````` Robbert Krebbers committed Jul 28, 2016 146 `````` Proof. `````` Robbert Krebbers committed Sep 06, 2016 147 `````` intros. apply (gset_disj_alloc_updateP_strong P); eauto. `````` Robbert Krebbers committed Aug 01, 2016 148 `````` intros i; rewrite right_id_L; auto. `````` Robbert Krebbers committed Jul 28, 2016 149 `````` Qed. `````` Robbert Krebbers committed Sep 06, 2016 150 `````` Lemma gset_disj_alloc_empty_updateP_strong' P : `````` Robbert Krebbers committed Aug 01, 2016 151 152 `````` (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) → GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i. `````` Robbert Krebbers committed Sep 06, 2016 153 `````` Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed. `````` Robbert Krebbers committed Jul 28, 2016 154 `````` `````` Robbert Krebbers committed Aug 02, 2016 155 156 157 `````` Section fresh_updates. Context `{Fresh K (gset K), !FreshSpec K (gset K)}. `````` Robbert Krebbers committed Sep 06, 2016 158 `````` Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X : `````` Robbert Krebbers committed Aug 02, 2016 159 160 `````` (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q. Proof. `````` Robbert Krebbers committed Sep 06, 2016 161 `````` intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto. `````` Robbert Krebbers committed Aug 02, 2016 162 163 `````` intros Y ?; exists (fresh Y); eauto using is_fresh. Qed. `````` Robbert Krebbers committed Sep 06, 2016 164 165 166 `````` Lemma gset_disj_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X. Proof. eauto using gset_disj_alloc_updateP. Qed. `````` Robbert Krebbers committed Aug 02, 2016 167 `````` `````` Robbert Krebbers committed Sep 06, 2016 168 `````` Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K → Prop) : `````` Robbert Krebbers committed Aug 02, 2016 169 `````` (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q. `````` Robbert Krebbers committed Sep 06, 2016 170 171 172 173 174 `````` 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. `````` Robbert Krebbers committed Aug 02, 2016 175 `````` End fresh_updates. `````` Zhen Zhang committed Aug 02, 2016 176 `````` `````` Robbert Krebbers committed Oct 03, 2016 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 `````` Lemma gset_disj_dealloc_local_update X Y Xf : GSet X ~l~> GSet (X ∖ Y) @ Some (GSet Xf). Proof. apply local_update_total; split; simpl. { rewrite !gset_disj_valid_op; set_solver. } intros mZ ?%gset_disj_valid_op. rewrite gset_disj_union //. destruct mZ as [[Z|]|]; simpl; try done. - rewrite {1}/op {1}/cmra_op /=. destruct (decide _); simpl; try done. intros [=]. do 2 f_equal. by apply union_cancel_l_L with X. - intros [=]. assert (Xf = ∅) as -> by set_solver. by rewrite right_id. Qed. Lemma gset_disj_dealloc_empty_local_update X Xf : GSet X ~l~> GSet ∅ @ Some (GSet Xf). Proof. rewrite -(difference_diag_L X). apply gset_disj_dealloc_local_update. Qed. `````` Robbert Krebbers committed Sep 06, 2016 194 `````` Lemma gset_disj_alloc_local_update X i Xf : `````` Robbert Krebbers committed Jul 23, 2016 195 196 197 198 199 200 201 `````` i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf). Proof. intros ??; apply local_update_total; split; simpl. - rewrite !gset_disj_valid_op; set_solver. - intros mZ ?%gset_disj_valid_op HXf. rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver. Qed. `````` Robbert Krebbers committed Sep 06, 2016 202 `````` Lemma gset_disj_alloc_empty_local_update i Xf : `````` Robbert Krebbers committed Jul 28, 2016 203 204 205 `````` i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf). Proof. intros. rewrite -(right_id_L _ _ {[i]}). `````` Robbert Krebbers committed Sep 06, 2016 206 `````` apply gset_disj_alloc_local_update; set_solver. `````` Robbert Krebbers committed Jul 28, 2016 207 `````` Qed. `````` Robbert Krebbers committed Sep 06, 2016 208 ``````End gset_disj. `````` Robbert Krebbers committed Jul 25, 2016 209 210 211 `````` Arguments gset_disjR _ {_ _}. Arguments gset_disjUR _ {_ _}.``````