coPset.v 4.09 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Export cmra.
2
From iris.algebra Require Import updates local_updates.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5
6
From iris.prelude Require Export collections coPset.
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)

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

11
  Canonical Structure coPsetC := discreteC coPset.
12
13
14

  Instance coPset_valid : Valid coPset := λ _, True.
  Instance coPset_op : Op coPset := union.
15
  Instance coPset_pcore : PCore coPset := Some.
16
17
18

  Lemma coPset_op_union X Y : X  Y = X  Y.
  Proof. done. Qed.
19
  Lemma coPset_core_self X : core X = X.
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
  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.
36
    - intros X. by rewrite coPset_core_self idemp_L.
37
38
39
40
41
42
43
44
45
46
47
48
49
50
  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.

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

(* The disjoiny union CMRA *)
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
62
63
Inductive coPset_disj :=
  | CoPset : coPset  coPset_disj
  | CoPsetBot : coPset_disj.

64
Section coPset_disj.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
  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.

82
  Lemma coPset_disj_included X Y : CoPset X  CoPset Y  X  Y.
83
84
85
86
87
88
  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
89
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
  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.
115
End coPset_disj.