proph_map.v 6.89 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris.algebra Require Import auth excl list gmap.
3 4 5 6
From iris.base_logic.lib Require Export own.
Set Default Proof Using "Type".
Import uPred.

Ralf Jung's avatar
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).

Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
11
  gmapUR P $ exclR $ listO $ leibnizO V.
12 13

Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
14
  fmap (λ vs, Excl (vs : list (leibnizO V))) pvs.
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33

(** The CMRA we need. *)
Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
  proph_map_inG :> inG Σ (authR (proph_mapUR P V));
  proph_map_name : gname
}.
Arguments proph_map_name {_ _ _ _ _} _ : assert.

Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
  { proph_map_preG_inG :> inG Σ (authR (proph_mapUR P V)) }.

Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
  #[GFunctor (authR (proph_mapUR P V))].

Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
  subG (proph_mapΣ P V) Σ  proph_mapPreG P V Σ.
Proof. solve_inG. Qed.

Section definitions.
34 35 36 37
  Context `{pG : proph_mapG P V Σ}.
  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
38

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

47 48
  Definition proph_resolves_in_list R pvs :=
    map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
49

50
  Definition proph_map_ctx pvs (ps : gset P) : iProp Σ :=
51
    ( R, proph_resolves_in_list R pvs 
52
          dom (gset _) R  ps 
53 54 55 56
          own (proph_map_name pG) ( (to_proph_map R)))%I.

  Definition proph_def (p : P) (vs : list V) : iProp Σ :=
    own (proph_map_name pG) ( {[p := Excl vs]}).
57

58 59
  Definition proph_aux : seal (@proph_def). by eexists. Qed.
  Definition proph := proph_aux.(unseal).
60
  Definition proph_eq : @proph = @proph_def := proph_aux.(seal_eq).
61 62
End definitions.

63
Section list_resolves.
Ralf Jung's avatar
Ralf Jung committed
64 65 66 67 68
  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.

69
  Lemma resolves_insert pvs p R :
70
    proph_resolves_in_list R pvs 
Ralf Jung's avatar
Ralf Jung committed
71
    p  dom (gset _) R 
72
    proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
Ralf Jung's avatar
Ralf Jung committed
73
  Proof.
74 75 76 77
    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
78
  Qed.
79
End list_resolves.
Ralf Jung's avatar
Ralf Jung committed
80

81 82 83
Section to_proph_map.
  Context (P V : Type) `{Countable P}.
  Implicit Types p : P.
84
  Implicit Types vs : list V.
85 86 87 88 89
  Implicit Types R : proph_map P V.

  Lemma to_proph_map_valid R :  to_proph_map R.
  Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.

90
  Lemma to_proph_map_insert p vs R :
91
    to_proph_map (<[p := vs]> R) = <[p := Excl (vs: list (leibnizO V))]> (to_proph_map R).
92 93 94 95 96 97 98 99 100 101
  Proof. by rewrite /to_proph_map fmap_insert. Qed.

  Lemma to_proph_map_delete p R :
    to_proph_map (delete p R) = delete p (to_proph_map R).
  Proof. by rewrite /to_proph_map fmap_delete. Qed.

  Lemma lookup_to_proph_map_None R p :
    R !! p = None  to_proph_map R !! p = None.
  Proof. by rewrite /to_proph_map lookup_fmap=> ->. Qed.

102 103
  Lemma proph_map_singleton_included R p vs :
    {[p := Excl vs]}  to_proph_map R  R !! p = Some vs.
104
  Proof.
105 106
    rewrite singleton_included_exclusive; last by apply to_proph_map_valid.
    by rewrite leibniz_equiv_iff /to_proph_map lookup_fmap fmap_Some=> -[v' [-> [->]]].
107 108 109
  Qed.
End to_proph_map.

110
Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
111 112 113
  (|==>  _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
Proof.
  iMod (own_alloc ( to_proph_map )) as (γ) "Hh".
114
  { rewrite auth_auth_valid. exact: to_proph_map_valid. }
115 116 117 118 119
  iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), . iSplit; last by iFrame.
  iPureIntro. split =>//.
Qed.

Section proph_map.
120
  Context `{proph_mapG P V Σ}.
121
  Implicit Types p : P.
122 123
  Implicit Types v : V.
  Implicit Types vs : list V.
124
  Implicit Types R : proph_map P V.
125
  Implicit Types ps : gset P.
126 127

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

131 132 133 134 135 136
  Lemma proph_exclusive p vs1 vs2 :
    proph p vs1 - proph p vs2 - False.
  Proof.
    rewrite proph_eq /proph_def. iIntros "Hp1 Hp2".
    iCombine "Hp1 Hp2" as "Hp".
    iDestruct (own_valid with "Hp") as %Hp.
137 138
    (* FIXME: FIXME(Coq #6294): needs new unification *)
    move:Hp. rewrite auth_frag_valid singleton_valid //.
139 140
  Qed.

141 142 143
  Lemma proph_map_new_proph p ps pvs :
    p  ps 
    proph_map_ctx pvs ps ==
144
    proph_map_ctx pvs ({[p]}  ps)  proph p (proph_list_resolves pvs p).
145
  Proof.
146 147
    iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
    rewrite proph_eq /proph_def.
148 149
    iMod (own_update with "H●") as "[H● H◯]".
    { eapply auth_update_alloc, (alloc_singleton_local_update _ p (Excl _))=> //.
Ralf Jung's avatar
Ralf Jung committed
150
      apply lookup_to_proph_map_None.
151
      apply (not_elem_of_dom (D:=gset P)). set_solver. }
152
    iModIntro. iFrame.
153
    iExists (<[p := proph_list_resolves pvs p]> R). iSplitR "H●".
154
    - iPureIntro. split.
Ralf Jung's avatar
Ralf Jung committed
155
      + apply resolves_insert; first done. set_solver.
156
      + rewrite dom_insert. set_solver.
157
    - by rewrite /to_proph_map fmap_insert.
158 159
  Qed.

160 161 162
  Lemma proph_map_resolve_proph p v pvs ps vs :
    proph_map_ctx ((p,v) :: pvs) ps  proph p vs ==
    vs', vs = v::vs'  proph_map_ctx pvs ps  proph p vs'.
163
  Proof.
Ralf Jung's avatar
Ralf Jung committed
164
    iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
165
    rewrite /proph_map_ctx proph_eq /proph_def.
166
    iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_both_valid.
167 168 169
    assert (vs = v :: proph_list_resolves pvs p) as ->.
    { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
    iMod (own_update_2 with "H● Hp") as "[H● H◯]".
170 171
    { (* FIXME: FIXME(Coq #6294): needs new unification *)
      eapply auth_update. apply: singleton_local_update.
172
      - by rewrite /to_proph_map lookup_fmap HR.
173
      - by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizO V)))). }
174
    rewrite /to_proph_map -fmap_insert.
175
    iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
Ralf Jung's avatar
Ralf Jung committed
176
    - iPureIntro. done.
177 178 179 180
    - 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
Ralf Jung committed
181 182 183
          rewrite (Hres q ws HEq).
          simpl. rewrite decide_False; done.
      + assert (p  dom (gset P) R) by exact: elem_of_dom_2.
184
        rewrite dom_insert. set_solver.
185 186
  Qed.
End proph_map.