resources.v 9.71 KB
Newer Older
1
From algebra Require Export fin_maps agree excl functor.
2
From algebra Require Import upred.
3
From program_logic Require Export language.
4

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

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

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

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_valid : Valid (res Λ Σ A) := λ r,  wld r   pst r   gst r.
80
Instance res_validN : ValidN (res Λ Σ A) := λ n r,
81
  {n} wld r  {n} pst r  {n} gst r.
82 83
Instance res_minus : Div (res Λ Σ A) := λ r1 r2,
  Res (wld r1 ÷ wld r2) (pst r1 ÷ pst r2) (gst r1 ÷ gst r2).
84

85
Lemma res_included (r1 r2 : res Λ Σ A) :
86 87 88
  r1  r2  wld r1  wld r2  pst r1  pst r2  gst r1  gst r2.
Proof.
  split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
89
  intros [r Hr]; split_and?;
90 91
    [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
Qed.
92
Lemma res_includedN (r1 r2 : res Λ Σ A) n :
93 94 95
  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)].
96
  intros [r Hr]; split_and?;
97 98
    [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
Qed.
99
Definition res_cmra_mixin : CMRAMixin (res Λ Σ A).
100 101
Proof.
  split.
102 103 104 105 106 107 108
  - by intros n x [???] ? [???]; constructor; cofe_subst.
  - by intros n [???] ? [???]; constructor; cofe_subst.
  - by intros n [???] ? [???] (?&?&?); split_and!; cofe_subst.
  - by intros n [???] ? [???] [???] ? [???]; constructor; cofe_subst.
  - intros r; split.
    + intros (?&?&?) n; split_and!; by apply cmra_valid_validN.
    + intros Hr; split_and!; apply cmra_valid_validN=> n; apply Hr.
109
  - by intros n ? (?&?&?); split_and!; apply cmra_validN_S.
110 111 112 113
  - by intros ???; constructor; rewrite /= assoc.
  - by intros ??; constructor; rewrite /= comm.
  - by intros ?; constructor; rewrite /= cmra_unit_l.
  - by intros ?; constructor; rewrite /= cmra_unit_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115
  - intros r1 r2; rewrite !res_included.
    by intros (?&?&?); split_and!; apply cmra_unit_preserving.
116
  - intros n r1 r2 (?&?&?);
117
      split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
  - intros r1 r2; rewrite res_included; intros (?&?&?).
119
    by constructor; apply cmra_op_div.
120 121 122 123 124
  - intros n r r1 r2 (?&?&?) [???]; simpl in *.
    destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
      (cmra_extend n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),
      (cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
    by exists (Res w σ m, Res w' σ' m').
125
Qed.
126 127
Canonical Structure resR : cmraT := CMRAT res_cofe_mixin res_cmra_mixin.
Global Instance res_cmra_identity : CMRAIdentity resR.
128 129
Proof.
  split.
130
  - split_and!; apply cmra_empty_valid.
131 132
  - by split; rewrite /= left_id.
  - apply _.
133
Qed.
134

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

140
Lemma wld_validN n r : {n} r  {n} wld r.
141
Proof. by intros (?&?&?). Qed.
142
Lemma gst_validN n r : {n} r  {n} gst r.
143 144 145 146 147 148 149
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 :
150
  {n} (r1r2)  wld r1 !! i {n} Some P  (wld r1  wld r2) !! i {n} Some P.
151 152
Proof.
  move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
153
  destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  by constructor; rewrite (agree_op_inv _ P P') // agree_idemp.
155 156
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
157
  {n} (r1r2)  wld r2 !! i {n} Some P  (wld r1  wld r2) !! i {n} Some P.
158
Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Global Instance Res_timeless eσ m : Timeless m  Timeless (Res  eσ m).
160
Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
161 162 163 164

(** Internalized properties *)
Lemma res_equivI {M} r1 r2 :
  (r1  r2)%I  (wld r1  wld r2  pst r1  pst r2  gst r1  gst r2: uPred M)%I.
165 166 167
Proof.
  uPred.unseal. do 2 split. by destruct 1. by intros (?&?&?); by constructor.
Qed.
168
Lemma res_validI {M} r : ( r)%I  ( wld r   pst r   gst r : uPred M)%I.
169
Proof. by uPred.unseal. Qed.
170
End res.
171 172

Arguments resC : clear implicits.
173
Arguments resR : clear implicits.
174

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

Program Definition resF {Λ Σ} : iFunctor := {|
224
  ifunctor_car := resR Λ Σ;
Ralf Jung's avatar
Ralf Jung committed
225 226
  ifunctor_map A B := resC_map
|}.
227 228
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.