gset.v 3.52 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
72
  Proof. move=>??. eapply gset_alloc_updateP_strong with (I:=); by eauto. Qed.
  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
  Lemma gset_alloc_local_update X i Xf :
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
81
82
83
84
85
    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.
86
End gset.
87
88
89

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