gset.v 8.15 KB
Newer Older
 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. `````` Ralf Jung committed Jan 03, 2017 4 ``````Set Default Proof Using "Type*". `````` Robbert Krebbers committed Mar 29, 2016 5 `````` `````` Robbert Krebbers committed Sep 06, 2016 6 7 8 9 10 ``````(* The union CMRA *) Section gset. Context `{Countable K}. Implicit Types X Y : gset K. `````` Robbert Krebbers committed Nov 28, 2016 11 `````` Canonical Structure gsetC := discreteC (gset K). `````` Robbert Krebbers committed Sep 06, 2016 12 13 14 `````` Instance gset_valid : Valid (gset K) := λ _, True. Instance gset_op : Op (gset K) := union. `````` Amin Timany committed Sep 14, 2016 15 `````` Instance gset_pcore : PCore (gset K) := λ X, Some X. `````` Robbert Krebbers committed Sep 06, 2016 16 17 18 `````` Lemma gset_op_union X Y : X ⋅ Y = X ∪ Y. Proof. done. Qed. `````` Amin Timany committed Sep 14, 2016 19 `````` Lemma gset_core_self X : core X = X. `````` Robbert Krebbers committed Sep 06, 2016 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 `````` 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 36 `````` - intros X. by rewrite gset_core_self idemp_L. `````` Robbert Krebbers committed Sep 06, 2016 37 38 39 40 41 42 43 44 45 46 47 48 49 50 `````` 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. `````` Robbert Krebbers committed Oct 06, 2016 51 `````` Lemma gset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X'). `````` Robbert Krebbers committed Sep 06, 2016 52 53 `````` Proof. intros (Z&->&?)%subseteq_disjoint_union_L. `````` Robbert Krebbers committed Oct 06, 2016 54 55 `````` rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->. split. done. rewrite gset_op_union. set_solver. `````` Robbert Krebbers committed Sep 06, 2016 56 `````` Qed. `````` Amin Timany committed Sep 14, 2016 57 `````` `````` Amin Timany committed Sep 14, 2016 58 `````` Global Instance gset_persistent X : Persistent X. `````` Amin Timany committed Sep 14, 2016 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 `````` Context `{Countable K}. Arguments op _ _ !_ !_ /. `````` Robbert Krebbers committed Oct 06, 2016 75 76 `````` Arguments cmra_op _ !_ !_ /. Arguments ucmra_op _ !_ !_ /. `````` Robbert Krebbers committed Jul 23, 2016 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 `````` 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 94 `````` Lemma gset_disj_included X Y : GSet X ≼ GSet Y ↔ X ⊆ Y. `````` Robbert Krebbers committed Sep 01, 2016 95 96 97 98 99 100 `````` 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 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 127 128 `````` 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 129 `````` Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K → Prop) X : `````` Robbert Krebbers committed Aug 01, 2016 130 131 `````` (∀ 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 132 `````` Proof. `````` Robbert Krebbers committed Aug 01, 2016 133 134 135 `````` 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 136 137 138 139 `````` 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 140 `````` Lemma gset_disj_alloc_updateP_strong' P X : `````` Robbert Krebbers committed Aug 01, 2016 141 142 `````` (∀ 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 143 `````` Proof. eauto using gset_disj_alloc_updateP_strong. Qed. `````` Robbert Krebbers committed Jul 23, 2016 144 `````` `````` Robbert Krebbers committed Sep 06, 2016 145 `````` Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) : `````` Robbert Krebbers committed Aug 01, 2016 146 147 `````` (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) → (∀ i, P i → Q (GSet {[i]})) → GSet ∅ ~~>: Q. `````` Robbert Krebbers committed Jul 28, 2016 148 `````` Proof. `````` Robbert Krebbers committed Sep 06, 2016 149 `````` intros. apply (gset_disj_alloc_updateP_strong P); eauto. `````` Robbert Krebbers committed Aug 01, 2016 150 `````` intros i; rewrite right_id_L; auto. `````` Robbert Krebbers committed Jul 28, 2016 151 `````` Qed. `````` Robbert Krebbers committed Sep 06, 2016 152 `````` Lemma gset_disj_alloc_empty_updateP_strong' P : `````` Robbert Krebbers committed Aug 01, 2016 153 154 `````` (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) → GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i. `````` Robbert Krebbers committed Sep 06, 2016 155 `````` Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed. `````` Robbert Krebbers committed Jul 28, 2016 156 `````` `````` Robbert Krebbers committed Aug 02, 2016 157 158 159 `````` Section fresh_updates. Context `{Fresh K (gset K), !FreshSpec K (gset K)}. `````` Robbert Krebbers committed Sep 06, 2016 160 `````` Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X : `````` Robbert Krebbers committed Aug 02, 2016 161 162 `````` (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q. Proof. `````` Robbert Krebbers committed Sep 06, 2016 163 `````` intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto. `````` Robbert Krebbers committed Aug 02, 2016 164 165 `````` intros Y ?; exists (fresh Y); eauto using is_fresh. Qed. `````` Robbert Krebbers committed Sep 06, 2016 166 167 168 `````` 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 169 `````` `````` Robbert Krebbers committed Sep 06, 2016 170 `````` Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K → Prop) : `````` Robbert Krebbers committed Aug 02, 2016 171 `````` (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q. `````` Robbert Krebbers committed Sep 06, 2016 172 173 174 175 176 `````` 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 177 `````` End fresh_updates. `````` Zhen Zhang committed Aug 02, 2016 178 `````` `````` Robbert Krebbers committed Oct 06, 2016 179 180 181 182 183 184 185 186 187 188 189 `````` Lemma gset_disj_dealloc_local_update X Y : (GSet X, GSet Y) ~l~> (GSet (X ∖ Y), ∅). Proof. apply local_update_total_valid=> _ _ /gset_disj_included HYX. rewrite local_update_unital_discrete=> -[Xf|] _ /leibniz_equiv_iff //=. rewrite {1}/op /=. destruct (decide _) as [HXf|]; [intros[= ->]|done]. by rewrite difference_union_distr_l_L difference_diag_L !left_id_L difference_disjoint_L. Qed. Lemma gset_disj_dealloc_empty_local_update X Z : (GSet Z ⋅ GSet X, GSet Z) ~l~> (GSet X,∅). `````` Robbert Krebbers committed Oct 03, 2016 190 `````` Proof. `````` Robbert Krebbers committed Oct 06, 2016 191 192 193 `````` apply local_update_total_valid=> /gset_disj_valid_op HZX _ _. assert (X = (Z ∪ X) ∖ Z) as HX by set_solver. rewrite gset_disj_union // {2}HX. apply gset_disj_dealloc_local_update. `````` Robbert Krebbers committed Oct 03, 2016 194 `````` Qed. `````` Robbert Krebbers committed Oct 06, 2016 195 196 `````` Lemma gset_disj_dealloc_op_local_update X Y Z : (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y) ~l~> (GSet X,GSet Y). `````` Robbert Krebbers committed Oct 03, 2016 197 `````` Proof. `````` Robbert Krebbers committed Oct 06, 2016 198 199 `````` rewrite -{2}(left_id ∅ _ (GSet Y)). apply op_local_update_frame, gset_disj_dealloc_empty_local_update. `````` Robbert Krebbers committed Oct 03, 2016 200 201 `````` Qed. `````` Robbert Krebbers committed Oct 06, 2016 202 203 204 205 206 207 208 `````` Lemma gset_disj_alloc_op_local_update X Y Z : Z ⊥ X → (GSet X,GSet Y) ~l~> (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y). Proof. intros. apply op_local_update_discrete. by rewrite gset_disj_valid_op. Qed. Lemma gset_disj_alloc_local_update X Y Z : Z ⊥ X → (GSet X,GSet Y) ~l~> (GSet (Z ∪ X), GSet (Z ∪ Y)). `````` Robbert Krebbers committed Jul 23, 2016 209 `````` Proof. `````` Robbert Krebbers committed Oct 06, 2016 210 211 212 `````` intros. apply local_update_total_valid=> _ _ /gset_disj_included ?. rewrite -!gset_disj_union //; last set_solver. auto using gset_disj_alloc_op_local_update. `````` Robbert Krebbers committed Jul 23, 2016 213 `````` Qed. `````` Robbert Krebbers committed Oct 06, 2016 214 215 `````` Lemma gset_disj_alloc_empty_local_update X Z : Z ⊥ X → (GSet X, GSet ∅) ~l~> (GSet (Z ∪ X), GSet Z). `````` Robbert Krebbers committed Jul 28, 2016 216 `````` Proof. `````` Robbert Krebbers committed Oct 06, 2016 217 `````` intros. rewrite -{2}(right_id_L _ union Z). `````` Robbert Krebbers committed Sep 06, 2016 218 `````` apply gset_disj_alloc_local_update; set_solver. `````` Robbert Krebbers committed Jul 28, 2016 219 `````` Qed. `````` Robbert Krebbers committed Sep 06, 2016 220 ``````End gset_disj. `````` Robbert Krebbers committed Jul 25, 2016 221 222 223 `````` Arguments gset_disjR _ {_ _}. Arguments gset_disjUR _ {_ _}.``````