coPset.v 4.12 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. `````` Robbert Krebbers committed Jul 23, 2016 3 ``````From iris.prelude 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 15 `````` Instance coPset_valid : Valid coPset := λ _, True. Instance coPset_op : Op coPset := union. `````` Robbert Krebbers committed Sep 19, 2016 16 `````` Instance coPset_pcore : PCore coPset := Some. `````` Robbert Krebbers committed Sep 06, 2016 17 18 19 `````` Lemma coPset_op_union X Y : X ⋅ Y = X ∪ Y. Proof. done. Qed. `````` Robbert Krebbers committed Sep 19, 2016 20 `````` Lemma coPset_core_self X : core X = X. `````` Robbert Krebbers committed Sep 06, 2016 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 `````` 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 37 `````` - intros X. by rewrite coPset_core_self idemp_L. `````` Robbert Krebbers committed Sep 06, 2016 38 39 40 41 42 43 44 45 46 47 48 49 50 51 `````` 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. `````` Robbert Krebbers committed Oct 06, 2016 52 `````` Lemma coPset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X'). `````` Robbert Krebbers committed Sep 06, 2016 53 54 `````` Proof. intros (Z&->&?)%subseteq_disjoint_union_L. `````` Robbert Krebbers committed Oct 06, 2016 55 56 `````` rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->. split. done. rewrite coPset_op_union. set_solver. `````` Robbert Krebbers committed Sep 06, 2016 57 58 59 60 `````` Qed. End coPset. (* The disjoiny union CMRA *) `````` Robbert Krebbers committed Jul 23, 2016 61 62 63 64 ``````Inductive coPset_disj := | CoPset : coPset → coPset_disj | CoPsetBot : coPset_disj. `````` Robbert Krebbers committed Sep 06, 2016 65 ``````Section coPset_disj. `````` Robbert Krebbers committed Jul 23, 2016 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 `````` 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. Instance coPset_disj_empty : Empty coPset_disj := CoPset ∅. 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. Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ∅. 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 83 `````` Lemma coPset_disj_included X Y : CoPset X ≼ CoPset Y ↔ X ⊆ Y. `````` Robbert Krebbers committed Sep 01, 2016 84 85 86 87 88 89 `````` 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 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 `````` 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. Lemma coPset_disj_ucmra_mixin : UCMRAMixin coPset_disj. 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. `````` Robbert Krebbers committed Sep 06, 2016 116 ``End coPset_disj.``