pviewshifts.v 20.6 KB
Newer Older
1
From stdpp Require Export coPset.
2
From fri.algebra Require Export upred updates.
3
4
From fri.program_logic Require Export model.
From fri.program_logic Require Import ownership wsat.
5
From iris.proofmode Require Import tactics classes.
Ralf Jung's avatar
Ralf Jung committed
6
Local Hint Extern 10 (_  _) => lia.
7
Local Hint Extern 100 (_ ## _) => set_solver.
8
Local Hint Extern 100 (_  _) => set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
Local Hint Extern 10 ({_} _) =>
10
  repeat match goal with
Ralf Jung's avatar
Ralf Jung committed
11
  | H : wsat _ _ _ _ _ |- _ => apply wsat_valid in H; last lia
12
  end; solve_validN.
13
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
14

Ralf Jung's avatar
Ralf Jung committed
15
Program Definition pvs_def {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
16
  {| uPred_holds n r1 rl :=  k Ef σ rf rfl ,
17
       0 < k  n  E1  E2 ## Ef 
18
19
       wsat k (E1  Ef) σ (r1  rf) (rl  rfl)  
        r2, P k r2 rl  wsat k (E2  Ef) σ (r2  rf) (rl  rfl) |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Next Obligation.
21
22
23
  intros Λ Σ E1 E2 P n r1 rl1 r2 rl2 HP [r3 Hr2] Hrl k Ef σ rf rfl ?? Hwsat; simpl in *.
  edestruct (HP k Ef σ (r3  rf) rfl) as (r'&?&?); rewrite ?(assoc op); eauto.
  - rewrite ?(assoc op) -(dist_le _ _ _ _ Hr2); last lia.
24
    by rewrite (dist_le _ _ _ _ Hrl); last lia.
25
26
27
  - exists (r'  r3); rewrite -assoc -(dist_le _ _ _ _ Hrl) //; last lia. 
    split; last done.
    apply uPred_mono with r' rl1; eauto using cmra_includedN_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Qed.
29
Next Obligation. naive_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
30
31
32
33
34
35

Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
Definition pvs := proj1_sig pvs_aux.
Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.

Arguments pvs {_ _} _ _ _%I.
36
Instance: Params (@pvs) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
37

38
39
40
41
Global Instance pvs_FUpd {Λ Σ} : FUpd _ := @pvs Λ Σ.
Global Instance pvs_BUpd {Λ Σ} : BUpd _ := @pvs Λ Σ  .

(*
42
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
43
  (at level 99, E1, E2 at level 50, Q at level 200,
44
45
   format "|={ E1 , E2 }=>  Q") : uPred_scope.
Notation "|={ E }=> Q" := (pvs E E Q%I)
46
  (at level 99, E at level 50, Q at level 200,
47
   format "|={ E }=>  Q") : uPred_scope.
48
Notation "|==> Q" := (pvs   Q%I)
49
  (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
50

51
*)
52
Notation "P ={ E1 , E2 }=> Q" := (P  |={E1,E2}=> Q)
53
  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
54
Notation "P ={ E }=> Q" := (P  |={E}=> Q)
55
  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
56

57
58
59
(*
Infix "-∗" := bi_wand.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I
60
  (at level 99, E1,E2 at level 50, Q at level 200,
61
62
   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P ={E,E}= Q)%I
63
  (at level 99, E at level 50, Q at level 200,
64
65
   format "P  ={ E }=∗  Q") : uPred_scope.
*)
66

Robbert Krebbers's avatar
Robbert Krebbers committed
67
Section pvs.
68
Context {Λ : language} {Σ : iFunctor}.
69
70
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
71

72
Lemma pvs_zero E1 E2 P r rl: pvs_def E1 E2 P 0 r rl.
Ralf Jung's avatar
Ralf Jung committed
73
Proof. intros ??????. exfalso. lia. Qed.
74

75
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
Ralf Jung's avatar
Ralf Jung committed
77
  rewrite pvs_eq.
78
79
  intros P Q HPQ; split=> n' r1 ??; simpl; split; intros HP k Ef σ rf rfl ???;
    destruct (HP k Ef σ rf rfl) as (r2&?&?); auto;
80
    exists r2; split_and?; auto; apply HPQ; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Qed.
82
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
Proof. apply ne_proper, _. Qed.

85
Lemma pvs_intro E P : P ={E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Proof.
87
  rewrite /pvs_FUpd pvs_eq. split=> n r ? HP k Ef σ rf ???; exists r; split; last done.
88
  apply uPred_closed with n; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Qed.
90

91
Lemma pvs_mono E1 E2 P Q : (P  Q)  (|={E1,E2}=> P) ={E1,E2}=> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof.
93
  rewrite /pvs_FUpd pvs_eq. intros HPQ; split=> n r rl ? ? HP k Ef σ rf rfl ???.
94
  destruct (HP k Ef σ rf rfl) as (r2&?&?); eauto.
95
  exists r2; eauto using uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
Qed.
Lemma pvs_trans E1 E2 E3 P :
98
  E2  E1  E3  (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Proof.
100
  rewrite /pvs_FUpd pvs_eq. intros ?; split=> n r1 rl ? ? HP1 rf rfl k Ef σ ???.
101
  destruct (HP1 rf rfl k Ef σ) as (r2&HP2&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
104
  Ef ## E1  E2  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
Proof.
106
  rewrite /pvs_FUpd pvs_eq. intros ?; split=> n r rl ? ? HP k Ef' σ rf rfl ???.
107
  destruct (HP k (EfEf') σ rf rfl) as (r'&?&?); rewrite ?(assoc_L _); eauto.
108
  by exists r'; rewrite -(assoc_L _).
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Qed.
110
Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P)  Q)%I ={E1,E2}=> P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
Proof.
112
  rewrite /pvs_FUpd pvs_eq. 
113
114
  uPred.unseal; split; intros n r rl ? ? (r1&r2&rl1&rl2&Hr&Hrl&HP&HQ) k Ef σ rf rfl ???.
  destruct (HP k Ef σ (r2  rf) (rl2  rfl)) as (r'&?&?); eauto.
115
116
117
  { 
    rewrite ?assoc -(dist_le _ _ _ _ Hr); last lia.
    rewrite -(dist_le _ _ _ _ Hrl); last lia; auto. 
118
119
120
  }
  exists (r'  r2); split.
  - exists r', r2, rl1, rl2. split_and?; eauto using dist_le. 
121
    eauto using dist_le.
122
    apply uPred_closed with n; auto.
123
  - rewrite (dist_le _ _ _ _ Hrl); last lia.
124
    by rewrite ?right_id -?assoc. 
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Qed.
126
Lemma pvs_openI i P : ownI i P  (|={{[i]},}=> ⧆▷ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
128
  rewrite /pvs_FUpd pvs_eq. uPred.unseal; split=> -[|n] r rl ? ? Hinv [|k] Ef σ rf rfl ???; try lia.
129
  apply ownI_spec in Hinv as [Hinv Hrl]; auto. 
130
  destruct (wsat_open k Ef σ (r  rf) (rl  rfl) i P) as (rP&?&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
  { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
132
  exists (rP  r); split; last by rewrite (left_id_L _ _) -assoc.
133
  eapply uPred_mono with rP rl; eauto using cmra_includedN_l.
134
  unseal; split; auto; rewrite (dist_le _ _ _ _ Hrl); last lia; auto; split; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Qed.
136
Lemma pvs_closeI i P : (ownI i P  P)  (|={,{[i]}}=> emp).
Robbert Krebbers's avatar
Robbert Krebbers committed
137
Proof.
138
139
  rewrite /pvs_FUpd pvs_eq.
  uPred.unseal; split=> -[|n] r rl ? ? [HI HP] [|k] Ef σ rf rfl ? HE ?; try lia.
140
  rewrite ownI_spec in HI *; auto; intros (Heq&Hrl).
141
142
143
144
145
146
147
  exists ; split. 
  - rewrite (dist_le _ _ _ _ Hrl); last lia. 
    split; auto.
  - rewrite left_id; apply wsat_close with P r.
    + eauto using dist_le.
    + set_solver +HE.
    + by rewrite -(left_id_L  () Ef).
148
    + apply uPred_closed with n; auto.
149
    rewrite -(dist_le _ _ _ _ Hrl); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Qed.
151
Lemma pvs_closeI_sep i P : (ownI i P  ⧆▷P)  (|={,{[i]}}=> emp).
152
Proof.
153
  rewrite /pvs_FUpd pvs_eq. uPred.unseal; split=> -[|n] r rl Hv Hvl;
154
155
156
157
158
159
  intros (x1&y1&x2&y2&Heq&Heql&HI&HP) [|k] Ef σ rf rfl ? HE ?; try lia.
  rewrite Heq in Hv *=>Hv.
  rewrite {1}Heql in Hvl *=>Hvl.
  rewrite ownI_spec in HI *; eauto using cmra_validN_op_r, cmra_validN_op_l. 
  intros (Heq2&Hrl2).
  exists ; split. 
160
161
  - move: HP. unseal. intros [HAff HP].
    rewrite HAff in Heql *. 
162
163
164
165
166
167
168
169
170
171
    rewrite Hrl2 ?left_id. intros Heq1l'.
    rewrite (dist_le _ _ _ _ Heq1l'); last lia. 
    split; auto.
  - rewrite left_id; apply wsat_close with P r.
    + rewrite (dist_le _ _ _ _ Heq); eauto using dist_le.
      rewrite lookup_wld_op_l; eauto. 
      apply dist_le with (S n); eauto.
    + set_solver +HE.
    + by rewrite -(left_id_L  () Ef).
    + apply uPred_closed with n; auto.
172
      move: HP. unseal. intros [HAff HP].
173
174
175
      rewrite (dist_le _ _ _ _ Heq); last lia. 
      rewrite -(dist_le _ _ _ _ HAff); last lia.
      apply uPred_mono with y1 y2; eauto using cmra_includedN_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Qed.
177
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ  Prop) :
178
  m ~~>: P  ownG m ={E}=>  m',  P m'  ownG m'.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
Proof.
180
  rewrite /pvs_FUpd pvs_eq. intros Hup.
181
  uPred.unseal; split=> -[|n] r rl ? ? /ownG_spec [Hinv ?] [|k] Ef σ rf rfl ???; try lia.
182
  destruct (wsat_update_gst k (E  Ef) σ r rf (rl  rfl) m P) as (m'&?&?); eauto.
183
  { apply cmra_includedN_le with (S n); auto. }
184
185
  exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec; split; auto]|]; auto.
  eapply dist_le; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
Qed.
187
Lemma pvs_allocI E P : ¬set_finite E  ⧆▷ P  (|={E}=>  i,  (i  E)  ownI i P).
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Proof.
189
190
  rewrite /pvs_FUpd pvs_eq. intros ?; rewrite /ownI; unseal.
  unseal. split=> -[|n] r rl ? ? [Hrl HP] [|k] Ef σ rf rfl ???; try lia.
191
  destruct (wsat_alloc k E Ef σ rf (rl  rfl) P r) as (i&?&?&?); auto.
192
  { apply uPred_closed with n; eauto. rewrite -(dist_le _ _ _ _ Hrl); eauto. }
193
  exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]}  ).
194
  split; [|done]. exists i; split_and!; rewrite /uPred_holds /= /uPred_holds /= ; auto.
195
  split; eauto. eapply dist_le with (S n); eauto.
196
197
198
199
Qed.
Lemma pvs_affine E1 E2 P : ((|={E1, E2}=> P) ⊣⊢ (|={E1, E2}=> P))%I.
Proof.
  apply (anti_symm ()).
200
201
  - rewrite !/pvs_FUpd pvs_eq //=. unfold_bi. unseal.
    split=> -[|n] r rl ?? [Hrl HP]; split; auto;
202
203
    intros [|k] Ef σ rf rfl ???; try lia.
    destruct (HP (S k) Ef σ rf rfl) as (r'&?&?); eauto; try lia.
204
205
    exists r'; split; auto. split; eauto. apply dist_le with (S n); eauto.
  - rewrite -pvs_mono; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
Qed.

208
(** * Derived rules *)
Robbert Krebbers's avatar
Robbert Krebbers committed
209
Import uPred.
210
Global Instance pvs_mono' E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
211
Proof. intros P Q; apply pvs_mono. Qed.
212
Global Instance pvs_flip_mono' E1 E2 :
213
  Proper (flip () ==> flip ()) (@pvs Λ Σ E1 E2).
214
Proof. intros P Q; apply pvs_mono. Qed.
215
Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ={E}=> P.
216
Proof. apply pvs_trans; set_solver. Qed.
217
Lemma pvs_strip_pvs E P Q : (P ={E}=> Q)  (|={E}=> P) ={E}=> Q.
218
Proof. move=>->. by rewrite pvs_trans'. Qed.
219
Lemma pvs_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q)  |={E1,E2}=> P  Q.
220
Proof. rewrite !(comm _ P%I); apply pvs_frame_r. Qed.
221
Lemma pvs_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P)  |={E1,E2}=> Q.
222
Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
223
Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}=> Q.
224
Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
225
Lemma pvs_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}=> P  Q.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
226
Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
227

228
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
229
  E1'  E1  E2'  E2  E1  E1' = E2  E2'  (|={E1',E2'}=> P) ={E1,E2}=> P.
230
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
  intros HE1 HE2 HEE.
232
  rewrite (pvs_mask_frame _ _ (E1  E1')); last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
  by rewrite {2}HEE -!union_difference_L.
234
Qed.
235
Lemma pvs_openI' E i P : i  E  ownI i P  |={E, E  {[i]}}=> ⧆▷ P.
236
Proof. intros. etrans. apply pvs_openI. apply pvs_mask_frame'; set_solver. Qed.
237
Lemma pvs_closeI' E i P : i  E  (ownI i P   P)  |={E  {[i]}, E}=> emp.
238
Proof. intros. etrans. apply pvs_closeI. apply pvs_mask_frame'; set_solver. Qed.
239
Lemma pvs_closeI_sep' E i P : i  E  (ownI i P  ⧆▷ P)  |={E  {[i]}, E}=> emp.
240
Proof. intros. etrans. apply pvs_closeI_sep. apply pvs_mask_frame'; set_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
241
242
243

Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
244
  (P  Q)  (|={E1',E2'}=> P) ={E1,E2}=> Q.
Ralf Jung's avatar
Ralf Jung committed
245
246
Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.

247
(** It should be possible to give a stronger version of this rule
Ralf Jung's avatar
Ralf Jung committed
248
249
   that does not force the conclusion view shift to have twice the
   same mask. However, even expressing the side-conditions on the
250
   mask becomes really ugly then, and we have not found an instance
Ralf Jung's avatar
Ralf Jung committed
251
   where that would be useful. *)
Ralf Jung's avatar
Ralf Jung committed
252
Lemma pvs_trans3 E1 E2 Q :
253
  E2  E1  (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q) ={E1}=> Q.
254
Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
255

256
Lemma pvs_mask_weaken E1 E2 P : E1  E2  (|={E1}=> P) ={E2}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
Proof. auto using pvs_mask_frame'. Qed.
Ralf Jung's avatar
Ralf Jung committed
258

259
Lemma pvs_ownG_update E m m' : m ~~> m'  ownG m ={E}=> ownG m'.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
  intros; rewrite (pvs_ownG_updateP E _ (m' =.)); last by apply cmra_update_updateP.
262
  by apply pvs_mono, uPred.exist_elim=> m''; apply pure_elim_l=> ->.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Qed.
264
265
266
267

Lemma except_0_pvs E1 E2 P :  (|={E1,E2}=> P) ={E1,E2}= P.
Proof.
  rewrite /pvs_FUpd pvs_eq /sbi_except_0; unseal. split=> n r rl ? ? HP k Ef σ rf rfl ???.
Ralf Jung's avatar
Ralf Jung committed
268
  destruct n; first by lia. destruct HP as [Hfalse|HP].
269
270
271
272
273
274
275
  - rewrite /uPred_holds//= in Hfalse.
  - rewrite //= in HP. edestruct HP; eauto.
Qed.

(** Proofmode class instances *)
Section proofmode_classes.

276
  Global Instance from_pure_pvs b E P φ : FromPure b P φ  FromPure b (|={E,E}=> P)%I φ.
277
278
279
280
281
282
283
284
285
286
287
288
289
  Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed.

  (*
  Global Instance from_assumption_pvs E p P Q :
    FromAssumption p P (|==> Q)  FromAssumption p P (|={E}=> Q)%I.
  Proof. rewrite /FromAssumption=>->. apply bupd_pvs. Qed.
   *)

  Global Instance into_wand_pvs E p q R P Q :
    IntoWand false false R P Q 
    IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
  Proof.
    rewrite /IntoWand /= => HR.
290
    rewrite !intuitionistically_if_elim HR.
291
292
293
294
295
296
    apply wand_intro_l. by rewrite pvs_sep wand_elim_r.
  Qed.

  Global Instance into_wand_pvs_persistent E1 E2 p q R P Q :
    IntoWand false q R P Q  IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
  Proof.
297
    rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
298
299
300
301
302
303
304
    apply wand_intro_l. by rewrite pvs_frame_l wand_elim_r.
  Qed.

  Global Instance into_wand_pvs_args E1 E2 p q R P Q :
    IntoWand p false R P Q  IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
  Proof.
    rewrite /IntoWand' /IntoWand /= => ->.
305
    apply wand_intro_l. by rewrite intuitionistically_if_elim pvs_wand_r.
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
  Qed.

  Global Instance from_sep_pvs E P Q1 Q2 :
    FromSep P Q1 Q2  FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
  Proof. rewrite /FromSep =><-. apply pvs_sep. Qed.

  Global Instance from_or_pvs E1 E2 P Q1 Q2 :
    FromOr P Q1 Q2  FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
  Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.

  Global Instance from_exist_pvs {A} E1 E2 P (Φ : A  iProp Λ Σ) :
    FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
  Proof.
    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
  Qed.

  Global Instance frame_pvs p E1 E2 R P Q :
    Frame p R P Q  Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
  Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.

  Global Instance is_except_0_pvs E1 E2 P : IsExcept0 (|={E1,E2}=> P).
  Proof. rewrite /IsExcept0. apply except_0_pvs. Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
  Lemma modality_pvs_mixin E:
    modality_mixin (@pvs Λ Σ E E) MIEnvId MIEnvId.
  Proof.
    split.
    - intros P. apply pvs_intro.
    - intros P. apply pvs_intro.
    - apply pvs_intro.
    - intros P Q ?. by apply pvs_mono.
    - intros P Q. by apply pvs_sep.
  Qed.

  Definition modality_pvs E :=
    Modality _ (modality_pvs_mixin E).

  Global Instance from_modal_pvs E P :
    FromModal (modality_pvs E) (True : iProp Λ Σ)%I (|={E}=> P)%I P.
  Proof. rewrite /FromModal => //=. Qed.
346
347

  Global Instance elim_modal_pvs_pvs E1 E2 E3 P Q :
348
349
350
351
352
    ElimModal (E2  E1  E3) p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
  Proof.
    intros. rewrite /ElimModal bi.intuitionistically_if_elim => ?.
    rewrite pvs_frame_r wand_elim_r pvs_trans //=.
  Qed.
353
354
355

End proofmode_classes.

Ralf Jung's avatar
Ralf Jung committed
356
Hint Extern 2 (environments.of_envs _  |={_}=> _) => iModIntro.
357
358
359



Robbert Krebbers's avatar
Robbert Krebbers committed
360
End pvs.
361
362
363
364
365
366

(** * Frame Shift Assertions. *)
(* Yes, the name is horrible...
   Frame Shift Assertions take a mask and a predicate over some type (that's
   their "postcondition"). They support weakening the mask, framing resources
   into the postcondition, and composition witn mask-changing view shifts. *)
367
368
Notation FSA Λ Σ A := (coPset  (A  iProp Λ Σ)  iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
369
  fsa_mask_frame_mono E1 E2 Φ Ψ :
370
371
    E1  E2  ( a, Φ a  Ψ a)  fsa E1 Φ  fsa E2 Ψ;
  fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a))  fsa E Φ;
372
  fsa_open_close E1 E2 Φ :
373
    fsaV  E2  E1  (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a))  fsa E1 Φ;
374
  fsa_frame_r E P Φ : (fsa E Φ  P)  fsa E (λ a, Φ a  P)
375
376
377
378
379
380
381
382
383
384
}.

(** Affine Frame Shift Assertion -- (an even more horrible name)
     only allows framing affine resources. *)
Class AffineFrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
  afsa_mask_frame_mono E1 E2 Φ Ψ :
    E1  E2  ( a, Φ a  Ψ a)  fsa E1 Φ  fsa E2 Ψ;
  afsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a))  fsa E Φ;
  afsa_open_close E1 E2 Φ :
    fsaV  E2  E1  (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a))  fsa E1 Φ;
385
  afsa_frame_r E P Φ `{Affine _ P} : (fsa E Φ  P)  fsa E (λ a, Φ a  P)
386
}.
387
388
(* Used to solve side-conditions related to [fsaV] *)
Create HintDb fsaV.
389

390
391
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
392
Implicit Types Φ Ψ : A  iProp Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
393
Import uPred.
394

395
Lemma fsa_mono E Φ Ψ : ( a, Φ a  Ψ a)  fsa E Φ  fsa E Ψ.
396
Proof. apply fsa_mask_frame_mono; auto. Qed.
397
Lemma fsa_mask_weaken E1 E2 Φ : E1  E2  fsa E1 Φ  fsa E2 Φ.
398
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
399
Lemma fsa_frame_l E P Φ : P  fsa E Φ  fsa E (λ a, P  Φ a).
400
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
401
Lemma fsa_strip_pvs E P Φ : (P  fsa E Φ)  (|={E}=> P)  fsa E Φ.
402
Proof.
403
404
  move=>->. rewrite -{2}fsa_trans3.
  apply pvs_mono, fsa_mono=>a; apply pvs_intro.
405
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
406
407
Lemma fsa_pvs_fsa E Φ : (|={E}=> fsa E Φ) ⊣⊢ fsa E Φ.
Proof. apply (anti_symm ()); [by apply fsa_strip_pvs|apply pvs_intro]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
409
410
411
412
Lemma pvs_fsa_fsa E Φ : fsa E (λ a, |={E}=> Φ a) ⊣⊢ fsa E Φ.
Proof.
  apply (anti_symm ()); [|apply fsa_mono=> a; apply pvs_intro].
  by rewrite (pvs_intro E (fsa E _)) fsa_trans3.
Qed.
413
Lemma fsa_mono_pvs E Φ Ψ : ( a, Φ a ={E}=> Ψ a)  fsa E Φ  fsa E Ψ.
414
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
415
Lemma fsa_wand_l E Φ Ψ : ( a, Φ a - Ψ a)  fsa E Φ  fsa E Ψ.
Robbert Krebbers's avatar
Robbert Krebbers committed
416
417
Proof.
  rewrite fsa_frame_l. apply fsa_mono=> a.
418
  by rewrite (forall_elim a) wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
419
Qed.
420
Lemma fsa_wand_r E Φ Ψ : fsa E Φ  ( a, Φ a - Ψ a)  fsa E Ψ.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
Proof. by rewrite (comm _ (fsa _ _)) fsa_wand_l. Qed.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
422
423
424
425
426

Instance fsa_afsa : AffineFrameShiftAssertion fsaV fsa.
Proof.
  split; eauto using fsa_mask_frame_mono, fsa_trans3, fsa_open_close, fsa_frame_r.
Qed.
427
428
429
430

Global Instance is_except_0_fsa E Ψ: IsExcept0 (fsa E Ψ).
Proof. rewrite /IsExcept0. iIntros "HP". iApply fsa_pvs_fsa. iMod "HP". by iModIntro. Qed.

431
432
End fsa.

433
434
435
436
437
438
439
440
441
Section afsa.
Context {Λ Σ A} (afsa : FSA Λ Σ A) `{!AffineFrameShiftAssertion fsaV afsa}.
Implicit Types Φ Ψ : A  iProp Λ Σ.
Import uPred.

Lemma afsa_mono E Φ Ψ : ( a, Φ a  Ψ a)  afsa E Φ  afsa E Ψ.
Proof. apply afsa_mask_frame_mono; auto. Qed.
Lemma afsa_mask_weaken E1 E2 Φ : E1  E2  afsa E1 Φ  afsa E2 Φ.
Proof. intros. apply afsa_mask_frame_mono; auto. Qed.
442
Lemma afsa_frame_l E (P: iProp Λ Σ) Φ `{Affine _ P} : (P  afsa E Φ)  afsa E (λ a, P  Φ a).
443
Proof. rewrite comm afsa_frame_r. apply afsa_mono=>a. by rewrite comm. Qed.
444
Lemma afsa_strip_pvs E P Φ : (P  afsa E Φ)  (|={E}=> P)  afsa E Φ.
445
446
447
448
449
450
451
452
453
454
455
456
457
Proof.
  move=>->. rewrite -{2}afsa_trans3.
  apply pvs_mono, afsa_mono=>a; apply pvs_intro.
Qed.
Lemma afsa_pvs_afsa E Φ : (|={E}=> afsa E Φ) ⊣⊢ afsa E Φ.
Proof. apply (anti_symm ()); [by apply afsa_strip_pvs|apply pvs_intro]. Qed.
Lemma pvs_afsa_afsa E Φ : afsa E (λ a, |={E}=> Φ a) ⊣⊢ afsa E Φ.
Proof.
  apply (anti_symm ()); [|apply afsa_mono=> a; apply pvs_intro].
  by rewrite (pvs_intro E (afsa E _)) afsa_trans3.
Qed.
Lemma afsa_mono_pvs E Φ Ψ : ( a, Φ a  (|={E}=> Ψ a))  afsa E Φ  afsa E Ψ.
Proof. intros. rewrite -[afsa E Ψ]afsa_trans3 -pvs_intro. by apply afsa_mono. Qed.
458
Lemma afsa_wand_l E Φ Ψ : (( a, Φ a - Ψ a)  afsa E Φ)  (afsa E Ψ).
459
460
Proof.
  rewrite afsa_frame_l. apply afsa_mono=> a.
461
  by rewrite (forall_elim a) affinely_elim wand_elim_l.
462
Qed.
463
Lemma afsa_wand_r E Φ Ψ : (afsa E Φ  ( a, Φ a - Ψ a))  (afsa E Ψ).
464
Proof. by rewrite (comm _ (afsa _ _)) afsa_wand_l. Qed.
465
466
467

Global Instance is_except_0_afsa E Ψ: IsExcept0 (afsa E Ψ).
Proof. rewrite /IsExcept0. iIntros "HP". iApply afsa_pvs_afsa. iMod "HP". by iModIntro. Qed.
468
469
End afsa.

470
Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
471
472
Arguments pvs_fsa _ _ _ _/.

473
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
474
Proof.
475
  rewrite /pvs_fsa.
476
477
  split; auto using pvs_mask_frame_mono, pvs_trans3.
  intros. rewrite pvs_frame_r. done.
478
Qed.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
479

480
481
482
Instance pvs_afsa_prf {Λ Σ} : AffineFrameShiftAssertion True (@pvs_fsa Λ Σ).
Proof.
  rewrite /pvs_fsa.
483
484
  split; auto using pvs_mask_frame_mono, pvs_trans3.
  intros. rewrite pvs_frame_r. done.
485
Qed.
486

487
488
Global Instance elim_modal_fsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ:
  FrameShiftAssertion fsaV fsa 
489
  ElimModal True false false (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ).
490
Proof.
491
  rewrite /ElimModal /= => FSA H.
492
493
494
495
496
  iIntros "(H1&H2)".
  iApply fsa_pvs_fsa.
  iMod "H1"; first by set_solver. iModIntro. by iApply "H2".
Qed.

497
Global Instance elim_modal_afsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ p:
498
  AffineFrameShiftAssertion fsaV fsa 
499
  ElimModal True p false (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ).
500
Proof.
501
  rewrite /ElimModal intuitionistically_if_elim /= => FSA H.
502
503
504
  iIntros "(H1&H2)".
  iApply afsa_pvs_afsa.
  iMod "H1"; first by set_solver. iModIntro. by iApply "H2".
505
Qed.