coPset.v 4.34 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. `````` Ralf Jung committed Feb 06, 2017 3 ``````From stdpp Require Export collections coPset. `````` Ralf Jung committed Jan 05, 2017 4 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Jul 23, 2016 5 6 7 ``````(** This is pretty much the same as algebra/gset, but I was not able to generalize the construction without breaking canonical structures. *) `````` Robbert Krebbers committed Sep 06, 2016 8 9 10 11 ``````(* The union CMRA *) Section coPset. Implicit Types X Y : coPset. `````` Robbert Krebbers committed Nov 28, 2016 12 `````` Canonical Structure coPsetC := discreteC coPset. `````` Robbert Krebbers committed Sep 06, 2016 13 14 `````` Instance coPset_valid : Valid coPset := λ _, True. `````` Robbert Krebbers committed Sep 17, 2017 15 `````` Instance coPset_unit : Unit coPset := (∅ : coPset). `````` Robbert Krebbers committed Sep 06, 2016 16 `````` Instance coPset_op : Op coPset := union. `````` Robbert Krebbers committed Sep 19, 2016 17 `````` Instance coPset_pcore : PCore coPset := Some. `````` Robbert Krebbers committed Sep 06, 2016 18 19 20 `````` Lemma coPset_op_union X Y : X ⋅ Y = X ∪ Y. Proof. done. Qed. `````` Robbert Krebbers committed Sep 19, 2016 21 `````` Lemma coPset_core_self X : core X = X. `````` Robbert Krebbers committed Sep 06, 2016 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 `````` 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. `````` Robbert Krebbers committed Sep 19, 2016 38 `````` - intros X. by rewrite coPset_core_self idemp_L. `````` Robbert Krebbers committed Sep 06, 2016 39 40 41 `````` Qed. Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin. `````` Robbert Krebbers committed Oct 25, 2017 42 `````` Global Instance coPset_cmra_discrete : CmraDiscrete coPsetR. `````` Robbert Krebbers committed Feb 09, 2017 43 44 `````` Proof. apply discrete_cmra_discrete. Qed. `````` Robbert Krebbers committed Oct 25, 2017 45 `````` Lemma coPset_ucmra_mixin : UcmraMixin coPset. `````` Robbert Krebbers committed Sep 06, 2016 46 `````` Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed. `````` Robbert Krebbers committed Oct 25, 2017 47 `````` Canonical Structure coPsetUR := UcmraT coPset coPset_ucmra_mixin. `````` Robbert Krebbers committed Sep 06, 2016 48 49 50 51 52 53 54 `````` 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. `````` Robbert Krebbers committed Oct 06, 2016 55 `````` Lemma coPset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X'). `````` Robbert Krebbers committed Sep 06, 2016 56 57 `````` Proof. intros (Z&->&?)%subseteq_disjoint_union_L. `````` Robbert Krebbers committed Oct 06, 2016 58 59 `````` rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->. split. done. rewrite coPset_op_union. set_solver. `````` Robbert Krebbers committed Sep 06, 2016 60 61 62 63 `````` Qed. End coPset. (* The disjoiny union CMRA *) `````` Robbert Krebbers committed Jul 23, 2016 64 65 66 67 ``````Inductive coPset_disj := | CoPset : coPset → coPset_disj | CoPsetBot : coPset_disj. `````` Robbert Krebbers committed Sep 06, 2016 68 ``````Section coPset_disj. `````` Robbert Krebbers committed Jul 23, 2016 69 70 71 72 73 `````` Arguments op _ _ !_ !_ /. Canonical Structure coPset_disjC := leibnizC coPset_disj. Instance coPset_disj_valid : Valid coPset_disj := λ X, match X with CoPset _ => True | CoPsetBot => False end. `````` Robbert Krebbers committed Sep 17, 2017 74 `````` Instance coPset_disj_unit : Unit coPset_disj := CoPset ∅. `````` Robbert Krebbers committed Jul 23, 2016 75 76 77 78 79 `````` Instance coPset_disj_op : Op coPset_disj := λ X Y, match X, Y with | CoPset X, CoPset Y => if decide (X ⊥ Y) then CoPset (X ∪ Y) else CoPsetBot | _, _ => CoPsetBot end. `````` Robbert Krebbers committed Sep 17, 2017 80 `````` Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ε. `````` Robbert Krebbers committed Jul 23, 2016 81 82 83 84 85 `````` Ltac coPset_disj_solve := repeat (simpl || case_decide); first [apply (f_equal CoPset)|done|exfalso]; set_solver by eauto. `````` Robbert Krebbers committed Sep 06, 2016 86 `````` Lemma coPset_disj_included X Y : CoPset X ≼ CoPset Y ↔ X ⊆ Y. `````` Robbert Krebbers committed Sep 01, 2016 87 88 89 90 91 92 `````` Proof. split. - move=> [[Z|]]; simpl; try case_decide; set_solver. - intros (Z&->&?)%subseteq_disjoint_union_L. exists (CoPset Z). coPset_disj_solve. Qed. `````` Robbert Krebbers committed Jul 23, 2016 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 `````` Lemma coPset_disj_valid_inv_l X Y : ✓ (CoPset X ⋅ Y) → ∃ Y', Y = CoPset Y' ∧ X ⊥ Y'. Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed. Lemma coPset_disj_union X Y : X ⊥ Y → CoPset X ⋅ CoPset Y = CoPset (X ∪ Y). Proof. intros. by rewrite /= decide_True. Qed. Lemma coPset_disj_valid_op X Y : ✓ (CoPset X ⋅ CoPset Y) ↔ X ⊥ Y. Proof. simpl. case_decide; by split. Qed. Lemma coPset_disj_ra_mixin : RAMixin coPset_disj. Proof. apply ra_total_mixin; eauto. - intros [?|]; destruct 1; coPset_disj_solve. - by constructor. - by destruct 1. - intros [X1|] [X2|] [X3|]; coPset_disj_solve. - intros [X1|] [X2|]; coPset_disj_solve. - intros [X|]; coPset_disj_solve. - exists (CoPset ∅); coPset_disj_solve. - intros [X1|] [X2|]; coPset_disj_solve. Qed. Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin. `````` Robbert Krebbers committed Oct 25, 2017 115 `````` Global Instance coPset_disj_cmra_discrete : CmraDiscrete coPset_disjR. `````` Robbert Krebbers committed Feb 09, 2017 116 117 `````` Proof. apply discrete_cmra_discrete. Qed. `````` Robbert Krebbers committed Oct 25, 2017 118 `````` Lemma coPset_disj_ucmra_mixin : UcmraMixin coPset_disj. `````` Robbert Krebbers committed Jul 23, 2016 119 `````` Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed. `````` Robbert Krebbers committed Oct 25, 2017 120 `````` Canonical Structure coPset_disjUR := UcmraT coPset_disj coPset_disj_ucmra_mixin. `````` Robbert Krebbers committed Sep 06, 2016 121 ``End coPset_disj.``