gset.v 4.76 KB
Newer Older
1
From iris.algebra Require Export cmra.
2
From iris.algebra Require Import updates local_updates.
3
From iris.prelude Require Export collections gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

5
6
7
8
9
Inductive gset_disj K `{Countable K} :=
  | GSet : gset K  gset_disj K
  | GSetBot : gset_disj K.
Arguments GSet {_ _ _} _.
Arguments GSetBot {_ _ _}.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11

Section gset.
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
  Context `{Countable K}.
  Arguments op _ _ !_ !_ /.

  Canonical Structure gset_disjC := leibnizC (gset_disj K).

  Instance gset_disj_valid : Valid (gset_disj K) := λ X,
    match X with GSet _ => True | GSetBot => False end.
  Instance gset_disj_empty : Empty (gset_disj K) := GSet .
  Instance gset_disj_op : Op (gset_disj K) := λ X Y,
    match X, Y with
    | GSet X, GSet Y => if decide (X  Y) then GSet (X  Y) else GSetBot
    | _, _ => GSetBot
    end.
  Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some .

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

  Lemma gset_disj_valid_inv_l X Y :  (GSet X  Y)   Y', Y = GSet Y'  X  Y'.
  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
  Lemma gset_disj_union X Y : X  Y  GSet X  GSet Y = GSet (X  Y).
  Proof. intros. by rewrite /= decide_True. Qed.
  Lemma gset_disj_valid_op X Y :  (GSet X  GSet Y)  X  Y.
  Proof. simpl. case_decide; by split. Qed.

  Lemma gset_disj_ra_mixin : RAMixin (gset_disj K).
  Proof.
    apply ra_total_mixin; eauto.
    - intros [?|]; destruct 1; gset_disj_solve.
    - by constructor.
    - by destruct 1.
    - intros [X1|] [X2|] [X3|]; gset_disj_solve.
    - intros [X1|] [X2|]; gset_disj_solve.
    - intros [X|]; gset_disj_solve.
    - exists (GSet ); gset_disj_solve.
    - intros [X1|] [X2|]; gset_disj_solve.
  Qed.
  Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.

  Lemma gset_disj_ucmra_mixin : UCMRAMixin (gset_disj K).
  Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
  Canonical Structure gset_disjUR :=
    discreteUR (gset_disj K) gset_disj_ra_mixin gset_disj_ucmra_mixin.

  Arguments op _ _ _ _ : simpl never.

59
60
61
  Lemma gset_alloc_updateP_strong P (Q : gset_disj K  Prop) X :
    ( Y, X  Y   j, j  Y  P j) 
    ( i, i  X  P i  Q (GSet ({[i]}  X)))  GSet X ~~>: Q.
62
  Proof.
63
64
65
    intros Hfresh HQ.
    apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
    destruct (Hfresh (X  Y)) as (i&?&?); first set_solver.
66
67
68
69
    exists (GSet ({[ i ]}  X)); split.
    - apply HQ; set_solver by eauto.
    - apply gset_disj_valid_op. set_solver by eauto.
  Qed.
70
71
72
  Lemma gset_alloc_updateP_strong' P X :
    ( Y, X  Y   j, j  Y  P j) 
    GSet X ~~>: λ Y,  i, Y = GSet ({[ i ]}  X)  i  X  P i.
73
  Proof. eauto using gset_alloc_updateP_strong. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
74

75
76
77
  Lemma gset_alloc_empty_updateP_strong P (Q : gset_disj K  Prop) :
    ( Y : gset K,  j, j  Y  P j) 
    ( i, P i  Q (GSet {[i]}))  GSet  ~~>: Q.
78
  Proof.
79
80
    intros. apply (gset_alloc_updateP_strong P); eauto.
    intros i; rewrite right_id_L; auto.
81
  Qed.
82
83
84
  Lemma gset_alloc_empty_updateP_strong' P :
    ( Y : gset K,  j, j  Y  P j) 
    GSet  ~~>: λ Y,  i, Y = GSet {[ i ]}  P i.
85
86
  Proof. eauto using gset_alloc_empty_updateP_strong. Qed.

87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
  Section fresh_updates.
    Context `{Fresh K (gset K), !FreshSpec K (gset K)}.

    Lemma gset_alloc_updateP (Q : gset_disj K  Prop) X :
      ( i, i  X  Q (GSet ({[i]}  X)))  GSet X ~~>: Q.
    Proof.
      intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
      intros Y ?; exists (fresh Y); eauto using is_fresh.
    Qed.
    Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y,  i, Y = GSet ({[ i ]}  X)  i  X.
    Proof. eauto using gset_alloc_updateP. Qed.

    Lemma gset_alloc_empty_updateP (Q : gset_disj K  Prop) :
      ( i, Q (GSet {[i]}))  GSet  ~~>: Q.
    Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
    Lemma gset_alloc_empty_updateP' : GSet  ~~>: λ Y,  i, Y = GSet {[ i ]}.
    Proof. eauto using gset_alloc_empty_updateP. Qed.
  End fresh_updates.
Zhen Zhang's avatar
Zhen Zhang committed
105

106
  Lemma gset_alloc_local_update X i Xf :
Robbert Krebbers's avatar
Robbert Krebbers committed
107
108
109
110
111
112
113
    i  X  i  Xf  GSet X ~l~> GSet ({[i]}  X) @ Some (GSet Xf).
  Proof.
    intros ??; apply local_update_total; split; simpl.
    - rewrite !gset_disj_valid_op; set_solver.
    - intros mZ ?%gset_disj_valid_op HXf.
      rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
  Qed.
114
115
116
117
118
119
  Lemma gset_alloc_empty_local_update i Xf :
    i  Xf  GSet  ~l~> GSet {[i]} @ Some (GSet Xf).
  Proof.
    intros. rewrite -(right_id_L _ _ {[i]}).
    apply gset_alloc_local_update; set_solver.
  Qed.
120
End gset.
121
122
123

Arguments gset_disjR _ {_ _}.
Arguments gset_disjUR _ {_ _}.