gset.v 3.07 KB
Newer Older
1
2
3
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
  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.

  Lemma updateP_alloc_strong (Q : gset_disj K  Prop) (I : gset K) X :
    ( 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.
  Lemma updateP_alloc (Q : gset_disj K  Prop) X :
    ( i, i  X  Q (GSet ({[i]}  X)))  GSet X ~~>: Q.
  Proof. move=>??. eapply updateP_alloc_strong with (I:=); by eauto. Qed.
  Lemma updateP_alloc_strong' (I : gset K) X :
    GSet X ~~>: λ Y,  i, Y = GSet ({[ i ]}  X)  i  I  i  X.
  Proof. eauto using updateP_alloc_strong. Qed.
  Lemma updateP_alloc' X : GSet X ~~>: λ Y,  i, Y = GSet ({[ i ]}  X)  i  X.
  Proof. eauto using updateP_alloc. Qed.
End gset.