coPset.v 4.13 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
From iris.prelude Require Export collections coPset.
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 coPsetC := discreteC coPset.
13 14 15

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

  Lemma coPset_op_union X Y : X  Y = X  Y.
  Proof. done. Qed.
20
  Lemma coPset_core_self X : core X = X.
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.
37
    - intros X. by rewrite coPset_core_self idemp_L.
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.

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

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

65
Section coPset_disj.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.

83
  Lemma coPset_disj_included X Y : CoPset X  CoPset Y  X  Y.
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's avatar
Robbert Krebbers committed
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.
116
End coPset_disj.