proph_map.v 5.04 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.proofmode Require Import proofmode.
2
From iris.base_logic.lib Require Export own.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.base_logic.lib Require Import ghost_map.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.prelude Require Import options.
5
6
Import uPred.

Ralf Jung's avatar
tweaks    
Ralf Jung committed
7
Local Notation proph_map P V := (gmap P (list V)).
8
9
10
Definition proph_val_list (P V : Type) := list (P * V).

(** The CMRA we need. *)
11
Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
12
  proph_map_GpreS_inG : ghost_mapG Σ P (list V)
Ralf Jung's avatar
Ralf Jung committed
13
}.
14
Local Existing Instances proph_map_GpreS_inG.
15

16
Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS {
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
17
  proph_map_inG : proph_mapGpreS P V Σ;
18
19
  proph_map_name : gname
}.
Ralf Jung's avatar
Ralf Jung committed
20
Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
21
Local Existing Instances proph_map_inG.
22
23

Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
Ralf Jung's avatar
Ralf Jung committed
24
  #[ghost_mapΣ P (list V)].
25

26
27
Global Instance subG_proph_mapGpreS {Σ P V} `{Countable P} :
  subG (proph_mapΣ P V) Σ  proph_mapGpreS P V Σ.
28
29
30
Proof. solve_inG. Qed.

Section definitions.
31
  Context `{pG : proph_mapGS P V Σ}.
32
33
34
  Implicit Types pvs : proph_val_list P V.
  Implicit Types R : proph_map P V.
  Implicit Types p : P.
Ralf Jung's avatar
Ralf Jung committed
35

36
  (** The list of resolves for [p] in [pvs]. *)
37
  Fixpoint proph_list_resolves pvs p : list V :=
38
39
    match pvs with
    | []         => []
40
41
    | (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
                    else proph_list_resolves pvs p
42
    end.
Ralf Jung's avatar
Ralf Jung committed
43

44
45
  Definition proph_resolves_in_list R pvs :=
    map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
46

47
  Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
48
49
     R, proph_resolves_in_list R pvs 
         dom (gset _) R  ps  ghost_map_auth (proph_map_name pG) 1 R.
50
51

  Definition proph_def (p : P) (vs : list V) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
52
    p [proph_map_name pG] vs.
53

54
  Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
55
  Definition proph := proph_aux.(unseal).
56
  Definition proph_eq : @proph = @proph_def := proph_aux.(seal_eq).
57
58
End definitions.

59
Section list_resolves.
Ralf Jung's avatar
Ralf Jung committed
60
61
62
63
64
  Context {P V : Type} `{Countable P}.
  Implicit Type pvs : proph_val_list P V.
  Implicit Type p : P.
  Implicit Type R : proph_map P V.

65
  Lemma resolves_insert pvs p R :
66
    proph_resolves_in_list R pvs 
Ralf Jung's avatar
Ralf Jung committed
67
    p  dom (gset _) R 
68
    proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
Ralf Jung's avatar
Ralf Jung committed
69
  Proof.
70
71
72
73
    intros Hinlist Hp q vs HEq.
    destruct (decide (p = q)) as [->|NEq].
    - rewrite lookup_insert in HEq. by inversion HEq.
    - rewrite lookup_insert_ne in HEq; last done. by apply Hinlist.
Ralf Jung's avatar
Ralf Jung committed
74
  Qed.
75
End list_resolves.
Ralf Jung's avatar
Ralf Jung committed
76

Ralf Jung's avatar
Ralf Jung committed
77
78
Lemma proph_map_init `{Countable P, !proph_mapGpreS P V Σ} pvs ps :
   |==>  _ : proph_mapGS P V Σ, proph_map_interp pvs ps.
79
Proof.
Ralf Jung's avatar
Ralf Jung committed
80
  iMod (ghost_map_alloc_empty) as (γ) "Hh".
Ralf Jung's avatar
Ralf Jung committed
81
  iModIntro. iExists (ProphMapGS P V _ _ _ _ γ), . iSplit; last by iFrame.
82
  iPureIntro. done.
83
84
85
Qed.

Section proph_map.
86
  Context `{proph_mapGS P V Σ}.
87
  Implicit Types p : P.
88
89
  Implicit Types v : V.
  Implicit Types vs : list V.
90
  Implicit Types R : proph_map P V.
91
  Implicit Types ps : gset P.
92
93

  (** General properties of mapsto *)
94
  Global Instance proph_timeless p vs : Timeless (proph p vs).
95
  Proof. rewrite proph_eq /proph_def. apply _. Qed.
96

97
98
99
100
  Lemma proph_exclusive p vs1 vs2 :
    proph p vs1 - proph p vs2 - False.
  Proof.
    rewrite proph_eq /proph_def. iIntros "Hp1 Hp2".
Ralf Jung's avatar
Ralf Jung committed
101
    by iDestruct (ghost_map_elem_ne with "Hp1 Hp2") as %?.
102
103
  Qed.

104
105
  Lemma proph_map_new_proph p ps pvs :
    p  ps 
106
107
    proph_map_interp pvs ps ==
    proph_map_interp pvs ({[p]}  ps)  proph p (proph_list_resolves pvs p).
108
  Proof.
109
110
    iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
    rewrite proph_eq /proph_def.
Ralf Jung's avatar
Ralf Jung committed
111
112
    iMod (ghost_map_insert p (proph_list_resolves pvs p) with "H●") as "[H● H◯]".
    { apply (not_elem_of_dom (D:=gset P)). set_solver. }
113
    iModIntro. iFrame.
114
115
116
117
    iExists (<[p := proph_list_resolves pvs p]> R).
    iFrame. iPureIntro. split.
    - apply resolves_insert; first done. set_solver.
    - rewrite dom_insert. set_solver.
118
119
  Qed.

120
  Lemma proph_map_resolve_proph p v pvs ps vs :
121
122
    proph_map_interp ((p,v) :: pvs) ps  proph p vs ==
    vs', vs = v::vs'  proph_map_interp pvs ps  proph p vs'.
123
  Proof.
Ralf Jung's avatar
tweaks    
Ralf Jung committed
124
    iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
125
    rewrite /proph_map_interp proph_eq /proph_def.
Ralf Jung's avatar
Ralf Jung committed
126
    iDestruct (ghost_map_lookup with "H● Hp") as %HR.
127
128
    assert (vs = v :: proph_list_resolves pvs p) as ->.
    { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
Ralf Jung's avatar
Ralf Jung committed
129
    iMod (ghost_map_update (proph_list_resolves pvs p) with "H● Hp") as "[H● H◯]".
130
    iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
Ralf Jung's avatar
tweaks    
Ralf Jung committed
131
    - iPureIntro. done.
132
133
134
135
    - iExists _. iFrame. iPureIntro. split.
      + intros q ws HEq. destruct (decide (p = q)) as [<-|NEq].
        * rewrite lookup_insert in HEq. by inversion HEq.
        * rewrite lookup_insert_ne in HEq; last done.
Ralf Jung's avatar
tweaks    
Ralf Jung committed
136
137
138
          rewrite (Hres q ws HEq).
          simpl. rewrite decide_False; done.
      + assert (p  dom (gset P) R) by exact: elem_of_dom_2.
139
        rewrite dom_insert. set_solver.
140
141
  Qed.
End proph_map.