coPset.v 4.32 KB
Newer Older
1
From stdpp Require Export sets coPset.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.algebra Require Export cmra.
3
From iris.algebra Require Import updates local_updates.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
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. *)

8 9 10 11
(* The union CMRA *)
Section coPset.
  Implicit Types X Y : coPset.

12
  Canonical Structure coPsetO := discreteO coPset.
13 14

  Instance coPset_valid : Valid coPset := λ _, True.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
  Instance coPset_unit : Unit coPset := ( : coPset).
16
  Instance coPset_op : Op coPset := union.
17
  Instance coPset_pcore : PCore coPset := Some.
18 19 20

  Lemma coPset_op_union X Y : X  Y = X  Y.
  Proof. done. Qed.
21
  Lemma coPset_core_self X : core X = X.
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.
38
    - intros X. by rewrite coPset_core_self idemp_L.
39 40 41
  Qed.
  Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.

42
  Global Instance coPset_cmra_discrete : CmraDiscrete coPsetR.
43 44
  Proof. apply discrete_cmra_discrete. Qed.

45
  Lemma coPset_ucmra_mixin : UcmraMixin coPset.
46
  Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed.
47
  Canonical Structure coPsetUR := UcmraT coPset coPset_ucmra_mixin.
48

49
  Lemma coPset_opM X mY : X ? mY = X  default  mY.
50 51 52 53 54
  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.

  Lemma coPset_update X Y : X ~~> Y.
  Proof. done. Qed.

55
  Lemma coPset_local_update X Y X' : X  X'  (X,Y) ~l~> (X',X').
56 57
  Proof.
    intros (Z&->&?)%subseteq_disjoint_union_L.
58 59
    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
    split. done. rewrite coPset_op_union. set_solver.
60 61 62 63
  Qed.
End coPset.

(* The disjoiny union CMRA *)
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66 67
Inductive coPset_disj :=
  | CoPset : coPset  coPset_disj
  | CoPsetBot : coPset_disj.

68
Section coPset_disj.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  Arguments op _ _ !_ !_ /.
70
  Canonical Structure coPset_disjO := leibnizO coPset_disj.
Robbert Krebbers's avatar
Robbert Krebbers committed
71 72 73

  Instance coPset_disj_valid : Valid coPset_disj := λ X,
    match X with CoPset _ => True | CoPsetBot => False end.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  Instance coPset_disj_unit : Unit coPset_disj := CoPset .
Robbert Krebbers's avatar
Robbert Krebbers committed
75 76
  Instance coPset_disj_op : Op coPset_disj := λ X Y,
    match X, Y with
77
    | CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X  Y) else CoPsetBot
Robbert Krebbers's avatar
Robbert Krebbers committed
78 79
    | _, _ => CoPsetBot
    end.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ε.
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82 83 84 85

  Ltac coPset_disj_solve :=
    repeat (simpl || case_decide);
    first [apply (f_equal CoPset)|done|exfalso]; set_solver by eauto.

86
  Lemma coPset_disj_included X Y : CoPset X  CoPset Y  X  Y.
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's avatar
Robbert Krebbers committed
93
  Lemma coPset_disj_valid_inv_l X Y :
94
     (CoPset X  Y)   Y', Y = CoPset Y'  X ## Y'.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
96
  Lemma coPset_disj_union X Y : X ## Y  CoPset X  CoPset Y = CoPset (X  Y).
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Proof. intros. by rewrite /= decide_True. Qed.
98
  Lemma coPset_disj_valid_op X Y :  (CoPset X  CoPset Y)  X ## Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
  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.

115
  Global Instance coPset_disj_cmra_discrete : CmraDiscrete coPset_disjR.
116 117
  Proof. apply discrete_cmra_discrete. Qed.

118
  Lemma coPset_disj_ucmra_mixin : UcmraMixin coPset_disj.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
120
  Canonical Structure coPset_disjUR := UcmraT coPset_disj coPset_disj_ucmra_mixin.
121
End coPset_disj.