gset.v 4.45 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
59
  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.

  Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
  Arguments op _ _ _ _ : simpl never.

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

78
79
80
81
82
83
84
85
86
87
88
89
90
91
  Lemma gset_alloc_empty_updateP_strong (Q : gset_disj K  Prop) (I : gset K) :
    ( i, i  I  Q (GSet {[i]}))  GSet  ~~>: Q.
  Proof.
    intros. apply (gset_alloc_updateP_strong _ I)=> i. rewrite right_id_L. auto.
  Qed.
  Lemma gset_alloc_empty_updateP (Q : gset_disj K  Prop) :
    ( i, Q (GSet {[i]}))  GSet  ~~>: Q.
  Proof. intro. eapply gset_alloc_empty_updateP_strong with (I:=); eauto. Qed.
  Lemma gset_alloc_empty_updateP_strong' (I : gset K) :
    GSet  ~~>: λ Y,  i, Y = GSet {[ i ]}  i  I.
  Proof. eauto using gset_alloc_empty_updateP_strong. Qed.
  Lemma gset_alloc_empty_updateP' : GSet  ~~>: λ Y,  i, Y = GSet {[ i ]}.
  Proof. eauto using gset_alloc_empty_updateP. Qed.

92
  Lemma gset_alloc_local_update X i Xf :
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
98
99
    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.
100
101
102
103
104
105
  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.
106
End gset.
107
108
109

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