resources.v 9.38 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2
Require Export algebra.fin_maps algebra.agree algebra.excl algebra.functor.
Require Export program_logic.language.
3

4
Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
5
  wld : mapRA positive (agreeRA A);
6
  pst : exclRA (istateC Λ);
7
  gst : optionRA (Σ A);
8 9
}.
Add Printing Constructor res.
10 11 12 13 14 15 16 17
Arguments Res {_ _ _} _ _ _.
Arguments wld {_ _ _} _.
Arguments pst {_ _ _} _.
Arguments gst {_ _ _} _.
Instance: Params (@Res) 3.
Instance: Params (@wld) 3.
Instance: Params (@pst) 3.
Instance: Params (@gst) 3.
18 19

Section res.
20 21
Context {Λ : language} {Σ : iFunctor} {A : cofeT}.
Implicit Types r : res Λ Σ A.
22

23
Inductive res_equiv' (r1 r2 : res Λ Σ A) := Res_equiv :
24
  wld r1  wld r2  pst r1  pst r2  gst r1  gst r2  res_equiv' r1 r2.
25 26
Instance res_equiv : Equiv (res Λ Σ A) := res_equiv'.
Inductive res_dist' (n : nat) (r1 r2 : res Λ Σ A) := Res_dist :
27
  wld r1 {n} wld r2  pst r1 {n} pst r2  gst r1 {n} gst r2 
28
  res_dist' n r1 r2.
29
Instance res_dist : Dist (res Λ Σ A) := res_dist'.
30
Global Instance Res_ne n :
31
  Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Λ Σ A).
32
Proof. done. Qed.
33
Global Instance Res_proper : Proper (() ==> () ==> () ==> ()) (@Res Λ Σ A).
34
Proof. done. Qed.
35
Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Λ Σ A).
36
Proof. by destruct 1. Qed.
37
Global Instance wld_proper : Proper (() ==> ()) (@wld Λ Σ A).
38
Proof. by destruct 1. Qed.
39
Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ Σ A).
40
Proof. by destruct 1. Qed.
41
Global Instance pst_ne' n : Proper (dist (S n) ==> ()) (@pst Λ Σ A).
42
Proof. destruct 1; apply (timeless _), dist_le with (S n); auto with lia. Qed.
43
Global Instance pst_proper : Proper (() ==> (=)) (@pst Λ Σ A).
44
Proof. by destruct 1; unfold_leibniz. Qed.
45
Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ Σ A).
46
Proof. by destruct 1. Qed.
47
Global Instance gst_proper : Proper (() ==> ()) (@gst Λ Σ A).
48
Proof. by destruct 1. Qed.
49
Instance res_compl : Compl (res Λ Σ A) := λ c,
50 51
  Res (compl (chain_map wld c))
      (compl (chain_map pst c)) (compl (chain_map gst c)).
52
Definition res_cofe_mixin : CofeMixin (res Λ Σ A).
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
Proof.
  split.
  * intros w1 w2; split.
    + by destruct 1; constructor; apply equiv_dist.
    + by intros Hw; constructor; apply equiv_dist=>n; destruct (Hw n).
  * intros n; split.
    + done.
    + by destruct 1; constructor.
    + do 2 destruct 1; constructor; etransitivity; eauto.
  * by destruct 1; constructor; apply dist_S.
  * done.
  * intros c n; constructor.
    + apply (conv_compl (chain_map wld c) n).
    + apply (conv_compl (chain_map pst c) n).
    + apply (conv_compl (chain_map gst c) n).
Qed.
Canonical Structure resC : cofeT := CofeT res_cofe_mixin.
Global Instance res_timeless r :
  Timeless (wld r)  Timeless (gst r)  Timeless r.
Proof. by destruct 3; constructor; try apply (timeless _). Qed.

74
Instance res_op : Op (res Λ Σ A) := λ r1 r2,
75
  Res (wld r1  wld r2) (pst r1  pst r2) (gst r1  gst r2).
76 77
Global Instance res_empty : Empty (res Λ Σ A) := Res   .
Instance res_unit : Unit (res Λ Σ A) := λ r,
78
  Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
79
Instance res_validN : ValidN (res Λ Σ A) := λ n r,
80
  {n} (wld r)  {n} (pst r)  {n} (gst r).
81
Instance res_minus : Minus (res Λ Σ A) := λ r1 r2,
82
  Res (wld r1  wld r2) (pst r1  pst r2) (gst r1  gst r2).
83
Lemma res_included (r1 r2 : res Λ Σ A) :
84 85 86 87 88 89
  r1  r2  wld r1  wld r2  pst r1  pst r2  gst r1  gst r2.
Proof.
  split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
  intros [r Hr]; split_ands;
    [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
Qed.
90
Lemma res_includedN (r1 r2 : res Λ Σ A) n :
91 92 93 94 95 96
  r1 {n} r2  wld r1 {n} wld r2  pst r1 {n} pst r2  gst r1 {n} gst r2.
Proof.
  split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
  intros [r Hr]; split_ands;
    [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
Qed.
97
Definition res_cmra_mixin : CMRAMixin (res Λ Σ A).
98 99 100 101 102 103 104 105
Proof.
  split.
  * by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst.
  * by intros n [???] ? [???]; constructor; simpl in *; cofe_subst.
  * by intros n [???] ? [???] (?&?&?); split_ands'; simpl in *; cofe_subst.
  * by intros n [???] ? [???] [???] ? [???];
      constructor; simpl in *; cofe_subst.
  * done.
106
  * by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
107 108
  * intros ???; constructor; simpl; apply (associative _).
  * intros ??; constructor; simpl; apply (commutative _).
109 110
  * intros ?; constructor; simpl; apply cmra_unit_l.
  * intros ?; constructor; simpl; apply cmra_unit_idempotent.
111
  * intros n r1 r2; rewrite !res_includedN.
112
    by intros (?&?&?); split_ands'; apply cmra_unit_preservingN.
113
  * intros n r1 r2 (?&?&?);
114
      split_ands'; simpl in *; eapply cmra_validN_op_l; eauto.
115 116 117
  * intros n r1 r2; rewrite res_includedN; intros (?&?&?).
    by constructor; apply cmra_op_minus.
Qed.
118
Definition res_cmra_extend_mixin : CMRAExtendMixin (res Λ Σ A).
119 120 121 122 123 124 125 126 127
Proof.
  intros n r r1 r2 (?&?&?) [???]; simpl in *.
  destruct (cmra_extend_op n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
    (cmra_extend_op n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),
    (cmra_extend_op n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
  by exists (Res w σ m, Res w' σ' m').
Qed.
Canonical Structure resRA : cmraT :=
  CMRAT res_cofe_mixin res_cmra_mixin res_cmra_extend_mixin.
128 129 130 131 132 133 134
Global Instance res_cmra_identity : CMRAIdentity resRA.
Proof.
  split.
  * intros n; split_ands'; apply cmra_empty_valid.
  * by split; rewrite /= (left_id _ _).
  * apply _.
Qed.
135

136
Definition update_pst (σ : state Λ) (r : res Λ Σ A) : res Λ Σ A :=
137
  Res (wld r) (Excl σ) (gst r).
138
Definition update_gst (m : Σ A) (r : res Λ Σ A) : res Λ Σ A :=
139
  Res (wld r) (pst r) (Some m).
140 141

Lemma wld_validN n r : {n} r  {n} (wld r).
142
Proof. by intros (?&?&?). Qed.
143 144 145 146 147 148 149 150
Lemma gst_validN n r : {n} r  {n} (gst r).
Proof. by intros (?&?&?). Qed.
Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
  Res w1 σ1 m1  Res w2 σ2 m2 = Res (w1  w2) (σ1  σ2) (m1  m2).
Proof. done. Qed.
Lemma Res_unit w σ m : unit (Res w σ m) = Res (unit w) (unit σ) (unit m).
Proof. done. Qed.
Lemma lookup_wld_op_l n r1 r2 i P :
151
  {n} (r1r2)  wld r1 !! i {n} Some P  (wld r1  wld r2) !! i {n} Some P.
152 153
Proof.
  move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
154
  destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
155 156 157
  by constructor; rewrite (agree_op_inv P P') // agree_idempotent.
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
158
  {n} (r1r2)  wld r2 !! i {n} Some P  (wld r1  wld r2) !! i {n} Some P.
159 160 161
Proof.
  rewrite (commutative _ r1) (commutative _ (wld r1)); apply lookup_wld_op_l.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163
Global Instance Res_timeless eσ m : Timeless m  Timeless (Res  eσ m).
Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
164
End res.
165 166

Arguments resC : clear implicits.
167 168
Arguments resRA : clear implicits.

169
Definition res_map {Λ Σ A B} (f : A -n> B) (r : res Λ Σ A) : res Λ Σ B :=
170
  Res (agree_map f <$> wld r)
171
      (pst r)
172
      (ifunctor_map Σ f <$> gst r).
173
Instance res_map_ne Λ Σ (A B : cofeT) (f : A -n> B) :
174
  ( n, Proper (dist n ==> dist n) f) 
175
   n, Proper (dist n ==> dist n) (@res_map Λ Σ _ _ f).
176
Proof. by intros Hf n [] ? [???]; constructor; simpl in *; cofe_subst. Qed.
177
Lemma res_map_id {Λ Σ A} (r : res Λ Σ A) : res_map cid r  r.
178 179 180
Proof.
  constructor; simpl; [|done|].
  * rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=.
181 182 183
    by rewrite -{2}(agree_map_id y); apply agree_map_ext.
  * rewrite -{2}(option_fmap_id (gst r)); apply option_fmap_setoid_ext=> m /=.
    by rewrite -{2}(ifunctor_map_id Σ m); apply ifunctor_map_ext.
184
Qed.
185
Lemma res_map_compose {Λ Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Λ Σ A) :
186 187 188 189
  res_map (g  f) r  res_map g (res_map f r).
Proof.
  constructor; simpl; [|done|].
  * rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
190 191 192
    by rewrite -agree_map_compose; apply agree_map_ext.
  * rewrite -option_fmap_compose; apply option_fmap_setoid_ext=> m /=.
    by rewrite -ifunctor_map_compose; apply ifunctor_map_ext.
193
Qed.
194
Lemma res_map_ext {Λ Σ A B} (f g : A -n> B) (r : res Λ Σ A) :
195
  ( x, f x  g x)  res_map f r  res_map g r.
196
Proof.
197 198
  intros Hfg; split; simpl; auto.
  * by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
199
  * by apply option_fmap_setoid_ext=>m; apply ifunctor_map_ext.
200
Qed.
201 202
Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
  CMRAMonotone (@res_map Λ Σ _ _ f).
203 204 205 206 207 208
Proof.
  split.
  * by intros n r1 r2; rewrite !res_includedN;
      intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
  * by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
Qed.
209 210 211 212
Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B :=
  CofeMor (res_map f : resRA Λ Σ A  resRA Λ Σ B).
Instance resC_map_ne {Λ Σ A B} n :
  Proper (dist n ==> dist n) (@resC_map Λ Σ A B).
213
Proof.
214
  intros f g Hfg r; split; simpl; auto.
215
  * by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
216
  * by apply optionC_map_ne, ifunctor_map_ne.
217
Qed.
Ralf Jung's avatar
Ralf Jung committed
218 219 220 221 222 223 224 225 226 227 228

Program Definition resF {Λ Σ} : iFunctor := {|
  ifunctor_car := resRA Λ Σ;
  ifunctor_map A B := resC_map
|}.
Next Obligation.
  intros Λ Σ A x. by rewrite /= res_map_id.
Qed.
Next Obligation.
  intros Λ Σ A B C f g x. by rewrite /= res_map_compose.
Qed.