weakestpre.v 18.7 KB
Newer Older
1
2
From iris.base_logic.lib Require Export fancy_updates.
From iris.program_logic Require Export language.
3
From iris.base_logic Require Import big_op.
4
From iris.proofmode Require Import tactics classes.
5
Set Default Proof Using "Type".
6
7
Import uPred.

8
Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
9
  iris_invG :> invG Σ;
10
  state_interp : Λstate  iProp Σ;
11
12
13
}.
Notation irisG Λ Σ := (irisG' (state Λ) Σ).

14
Definition wp_pre `{irisG Λ Σ}
15
16
    (wp : bool -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
    bool -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ p E e1 Φ,
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
  match to_val e1 with
  | Some v => |={E}=> Φ v
  | None =>  σ1,
20
     state_interp σ1 ={E,}= if p then reducible e1 σ1 else True 
Ralf Jung's avatar
Ralf Jung committed
21
       e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
22
23
       state_interp σ2  wp p E e2 Φ 
       [ list] ef  efs, wp p  ef (λ _, True)
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  end%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
25

26
27
Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
Proof.
28
  rewrite /wp_pre=> n wp wp' Hwp p E e1 Φ.
29
  repeat (f_contractive || f_equiv); apply Hwp.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Qed.
31

32
Definition wp_def `{irisG Λ Σ} :
33
  bool  coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ := fixpoint wp_pre.
34
35
36
Definition wp_aux : seal (@wp_def). by eexists. Qed.
Definition wp := unseal wp_aux.
Definition wp_eq : @wp = @wp_def := seal_eq wp_aux.
Ralf Jung's avatar
Ralf Jung committed
37

38
39
Arguments wp {_ _ _} _ _ _%E _.
Instance: Params (@wp) 6.
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41
42
43
44
Notation "'WP' e @ p ; E {{ Φ } }" := (wp p E e%E Φ)
  (at level 20, e, Φ at level 200,
   format "'[' 'WP'  e  '/' @  p ;  E  {{  Φ  } } ']'") : uPred_scope.
Notation "'WP' e @ E {{ Φ } }" := (wp true E e%E Φ)
45
  (at level 20, e, Φ at level 200,
46
   format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : uPred_scope.
47
48
49
50
Notation "'WP' e @ E ? {{ Φ } }" := (wp false E e%E Φ)
  (at level 20, e, Φ at level 200,
   format "'[' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : uPred_scope.
Notation "'WP' e {{ Φ } }" := (wp true  e%E Φ)
51
  (at level 20, e, Φ at level 200,
52
   format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : uPred_scope.
53
54
55
Notation "'WP' e ? {{ Φ } }" := (wp false  e%E Φ)
  (at level 20, e, Φ at level 200,
   format "'[' 'WP'  e  '/' ? {{  Φ  } } ']'") : uPred_scope.
56

57
58
59
60
Notation "'WP' e @ p ; E {{ v , Q } }" := (wp p E e%E (λ v, Q))
  (at level 20, e, Q at level 200,
   format "'[' 'WP'  e  '/' @  p ;  E  {{  v ,  Q  } } ']'") : uPred_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp true E e%E (λ v, Q))
61
  (at level 20, e, Q at level 200,
62
   format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : uPred_scope.
63
64
65
66
Notation "'WP' e @ E ? {{ v , Q } }" := (wp false E e%E (λ v, Q))
  (at level 20, e, Q at level 200,
   format "'[' 'WP'  e  '/' @  E  ? {{  v ,  Q  } } ']'") : uPred_scope.
Notation "'WP' e {{ v , Q } }" := (wp true  e%E (λ v, Q))
67
  (at level 20, e, Q at level 200,
68
   format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : uPred_scope.
69
70
71
Notation "'WP' e ? {{ v , Q } }" := (wp false  e%E (λ v, Q))
  (at level 20, e, Q at level 200,
   format "'[' 'WP'  e  '/' ? {{  v ,  Q  } } ']'") : uPred_scope.
72

Ralf Jung's avatar
Ralf Jung committed
73
(* Texan triples *)
74
75
76
77
78
Notation "'{{{' P } } } e @ p ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
  (  Φ,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ p; E {{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "{{{  P  } } }  e  @  p ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
79
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
Ralf Jung's avatar
Ralf Jung committed
80
  (  Φ,
81
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
82
    (at level 20, x closed binder, y closed binder,
83
     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
84
85
86
87
88
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
  (  Φ,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E ?{{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
89
90
91
92
93
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
  (  Φ,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q } } }") : uPred_scope.
94
95
96
97
98
99
100
101
102
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
  (  Φ,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e ?{{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
     format "{{{  P  } } }  e  ? {{{  x .. y ,   RET  pat ;  Q } } }") : uPred_scope.
Notation "'{{{' P } } } e @ p ; E {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e @ p; E {{ Φ }})%I
    (at level 20,
     format "{{{  P  } } }  e  @  p ;  E  {{{  RET  pat ;  Q } } }") : uPred_scope.
103
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
104
  (  Φ, P -  (Q - Φ pat%V) - WP e @ E {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
105
    (at level 20,
106
     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : uPred_scope.
107
108
109
110
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e @ E ?{{ Φ }})%I
    (at level 20,
     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q } } }") : uPred_scope.
111
112
113
114
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e {{ Φ }})%I
    (at level 20,
     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : uPred_scope.
115
116
117
118
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e ?{{ Φ }})%I
    (at level 20,
     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q } } }") : uPred_scope.
Ralf Jung's avatar
Ralf Jung committed
119

120
121
122
123
124
Notation "'{{{' P } } } e @ p ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ p; E {{ Φ }})
    (at level 20, x closed binder, y closed binder,
     format "{{{  P  } } }  e  @  p ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
125
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
126
  ( Φ : _  uPred _,
127
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})
Ralf Jung's avatar
Ralf Jung committed
128
    (at level 20, x closed binder, y closed binder,
129
     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
130
131
132
133
134
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E ?{{ Φ }})
    (at level 20, x closed binder, y closed binder,
     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
135
136
137
138
139
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})
    (at level 20, x closed binder, y closed binder,
     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
140
141
142
143
144
145
146
147
148
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e ?{{ Φ }})
    (at level 20, x closed binder, y closed binder,
     format "{{{  P  } } }  e  ? {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
Notation "'{{{' P } } } e @ p ; E {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e @ p; E {{ Φ }})
    (at level 20,
     format "{{{  P  } } }  e  @  p ;  E  {{{  RET  pat ;  Q } } }") : C_scope.
149
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
150
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e @ E {{ Φ }})
Ralf Jung's avatar
Ralf Jung committed
151
    (at level 20,
152
     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : C_scope.
153
154
155
156
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e @ E ?{{ Φ }})
    (at level 20,
     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q } } }") : C_scope.
157
158
159
160
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e {{ Φ }})
    (at level 20,
     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : C_scope.
161
162
163
164
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e ?{{ Φ }})
    (at level 20,
     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q } } }") : C_scope.
165

Robbert Krebbers's avatar
Robbert Krebbers committed
166
Section wp.
167
Context `{irisG Λ Σ}.
168
Implicit Types p : bool.
169
170
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
171
172
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
173

174
(* Weakest pre *)
175
Lemma wp_unfold p E e Φ : WP e @ p; E {{ Φ }}  wp_pre wp p E e Φ.
176
177
Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.

178
179
Global Instance wp_ne p E e n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ p E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
180
Proof.
181
  revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
182
183
184
185
  rewrite !wp_unfold /wp_pre.
  (* FIXME: figure out a way to properly automate this proof *)
  (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
  is very slow here *)
Robbert Krebbers's avatar
Robbert Krebbers committed
186
  do 17 (f_contractive || f_equiv). apply IH; first lia.
187
  intros v. eapply dist_le; eauto with omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Qed.
189
190
Global Instance wp_proper p E e :
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ p E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Proof.
192
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
Qed.
194

195
Lemma wp_value' p E Φ v : Φ v  WP of_val v @ p; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
197
Lemma wp_value_inv p E Φ v : WP of_val v @ p; E {{ Φ }} ={E}= Φ v.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
199

200
201
Lemma wp_strong_mono p E1 E2 e Φ Ψ :
  E1  E2  ( v, Φ v ={E2}= Ψ v)  WP e @ p; E1 {{ Φ }}  WP e @ p; E2 {{ Ψ }}.
202
Proof.
203
  iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
  destruct (to_val e) as [v|] eqn:?.
205
  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
207
  iMod ("H" with "[$]") as "[$ H]".
208
  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
209
  iMod ("H" with "[//]") as "($ & H & $)"; auto.
210
  iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
211
212
Qed.

213
214
215
216
217
218
219
220
221
222
223
224
225
226
Lemma wp_forget_progress E e Φ : WP e @ E {{ Φ }}  WP e @ E ?{{ Φ }}.
Proof.
  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
  destruct (to_val e) as [v|]; first iExact "H".
  iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[#Hred H]". iModIntro.
  iSplit; first done. iNext. iIntros (e2 σ2 efs) "#Hstep".
  iMod ("H" with "Hstep") as "($ & He2 & Hefs)". iModIntro.
  iSplitL "He2"; first by iApply ("IH" with "He2"). iClear "Hred Hstep".
  induction efs as [|ef efs IH]; first by iApply big_sepL_nil.
  rewrite !big_sepL_cons. iDestruct "Hefs" as "(Hef & Hefs)".
  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH. 
Qed.

Lemma fupd_wp p E e Φ : (|={E}=> WP e @ p; E {{ Φ }})  WP e @ p; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
Proof.
228
  rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
  { by iMod "H". }
  iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
231
Qed.
232
233
Lemma wp_fupd p E e Φ : WP e @ p; E {{ v, |={E}=> Φ v }}  WP e @ p; E {{ Φ }}.
Proof. iIntros "H". iApply (wp_strong_mono p E); try iFrame; auto. Qed.
234

235
236
Lemma wp_atomic' p E1 E2 e Φ :
  StronglyAtomic e  p  Atomic e 
237
  (|={E1,E2}=> WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ p; E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
238
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
  iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
240
  destruct (to_val e) as [v|].
Robbert Krebbers's avatar
Robbert Krebbers committed
241
242
  { by iDestruct "H" as ">>> $". }
  iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
243
  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
244
245
246
247
248
249
250
251
252
  destruct Hatomic as [Hstrong|[? Hweak]].
  - destruct (Hstrong _ _ _ _ Hstep) as [v <-%of_to_val].
    iMod ("H" with "[#]") as "($ & H & $)"; first done.
    iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
  - destruct p; last done. iMod ("H" with "[//]") as "(Hphy & H & $)".
    rewrite !wp_unfold /wp_pre. destruct (to_val e2).
    + iDestruct "H" as ">> $". by iFrame.
    + iMod ("H" with "[$]") as "[H _]".
      iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hweak _ _ _ _ Hstep).
Robbert Krebbers's avatar
Robbert Krebbers committed
253
Qed.
254

255
Lemma wp_step_fupd p E1 E2 e P Φ :
256
  to_val e = None  E2  E1 
257
  (|={E1,E2}=> P) - WP e @ p; E2 {{ v, P ={E1}= Φ v }} - WP e @ p; E1 {{ Φ }}.
258
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
  rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
260
  iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
261
  iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
262
  iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
263
  iMod "HR". iModIntro. iApply (wp_strong_mono p E2); first done.
264
  iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
265
Qed.
266

267
268
Lemma wp_bind K `{!LanguageCtx Λ K} p E e Φ :
  WP e @ p; E {{ v, WP K (of_val v) @ p; E {{ Φ }} }}  WP K e @ p; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
Proof.
270
  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
273
  destruct (to_val e) as [v|] eqn:He.
  { apply of_to_val in He as <-. by iApply fupd_wp. }
  rewrite wp_unfold /wp_pre fill_not_val //.
274
  iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
275
276
  { iPureIntro. destruct p; last done.
    unfold reducible in *. naive_solver eauto using fill_step. }
277
278
  iNext; iIntros (e2 σ2 efs Hstep).
  destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
279
  iMod ("H" $! e2' σ2 efs with "[//]") as "($ & H & $)".
280
  by iApply "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
281
282
Qed.

283
284
Lemma wp_bind_inv K `{!LanguageCtx Λ K} p E e Φ :
  WP K e @ p; E {{ Φ }}  WP e @ p; E {{ v, WP K (of_val v) @ p; E {{ Φ }} }}.
285
286
287
288
289
290
Proof.
  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
  destruct (to_val e) as [v|] eqn:He.
  { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
  rewrite fill_not_val //.
  iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
291
  { destruct p; eauto using reducible_fill. }
292
293
294
295
296
  iNext; iIntros (e2 σ2 efs Hstep).
  iMod ("H" $! (K e2) σ2 efs with "[]") as "($ & H & $)"; eauto using fill_step.
  by iApply "IH".
Qed.

297
(** * Derived rules *)
298
Lemma wp_mono p E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ p; E {{ Φ }}  WP e @ p; E {{ Ψ }}.
299
Proof.
300
  iIntros (HΦ) "H"; iApply (wp_strong_mono p E E); auto.
301
  iIntros "{$H}" (v) "?". by iApply HΦ.
302
Qed.
303
304
305
306
Lemma wp_mask_mono p E1 E2 e Φ : E1  E2  WP e @ p; E1 {{ Φ }}  WP e @ p; E2 {{ Φ }}.
Proof. iIntros (?) "H"; iApply (wp_strong_mono p E1 E2); auto. iFrame; eauto. Qed.
Global Instance wp_mono' p E e :
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ p E e).
307
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
308

309
Lemma wp_value p E Φ e v `{!IntoVal e v} : Φ v  WP e @ p; E {{ Φ }}.
310
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
311
Lemma wp_value_fupd' p E Φ v : (|={E}=> Φ v)  WP of_val v @ p; E {{ Φ }}.
312
Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
313
314
Lemma wp_value_fupd p E Φ e v `{!IntoVal e v} :
  (|={E}=> Φ v)  WP e @ p; E {{ Φ }}.
315
Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
316

317
318
319
320
321
322
323
324
325
Lemma wp_strong_atomic p E1 E2 e Φ :
  StronglyAtomic e 
  (|={E1,E2}=> WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ p; E1 {{ Φ }}.
Proof. by eauto using wp_atomic'. Qed.
Lemma wp_atomic E1 E2 e Φ :
  Atomic e 
  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ E1 {{ Φ }}.
Proof. by eauto using wp_atomic'. Qed.

326
327
328
329
Lemma wp_frame_l p E e Φ R : R  WP e @ p; E {{ Φ }}  WP e @ p; E {{ v, R  Φ v }}.
Proof. iIntros "[??]". iApply (wp_strong_mono p E E _ Φ); try iFrame; eauto. Qed.
Lemma wp_frame_r p E e Φ R : WP e @ p; E {{ Φ }}  R  WP e @ p; E {{ v, Φ v  R }}.
Proof. iIntros "[??]". iApply (wp_strong_mono p E E _ Φ); try iFrame; eauto. Qed.
330

331
Lemma wp_frame_step_l p E1 E2 e Φ R :
332
  to_val e = None  E2  E1 
333
  (|={E1,E2}=> R)  WP e @ p; E2 {{ Φ }}  WP e @ p; E1 {{ v, R  Φ v }}.
334
Proof.
335
  iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
336
337
  iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
Qed.
338
Lemma wp_frame_step_r p E1 E2 e Φ R :
339
  to_val e = None  E2  E1 
340
  WP e @ p; E2 {{ Φ }}  (|={E1,E2}=> R)  WP e @ p; E1 {{ v, Φ v  R }}.
Ralf Jung's avatar
Ralf Jung committed
341
Proof.
342
  rewrite [(WP _ @ _; _ {{ _ }}  _)%I]comm; setoid_rewrite (comm _ _ R).
343
  apply wp_frame_step_l.
Ralf Jung's avatar
Ralf Jung committed
344
Qed.
345
346
347
348
349
350
Lemma wp_frame_step_l' p E e Φ R :
  to_val e = None   R  WP e @ p; E {{ Φ }}  WP e @ p; E {{ v, R  Φ v }}.
Proof. iIntros (?) "[??]". iApply (wp_frame_step_l p E E); try iFrame; eauto. Qed.
Lemma wp_frame_step_r' p E e Φ R :
  to_val e = None  WP e @ p; E {{ Φ }}   R  WP e @ p; E {{ v, Φ v  R }}.
Proof. iIntros (?) "[??]". iApply (wp_frame_step_r p E E); try iFrame; eauto. Qed.
351

352
353
Lemma wp_wand p E e Φ Ψ :
  WP e @ p; E {{ Φ }} - ( v, Φ v - Ψ v) - WP e @ p; E {{ Ψ }}.
354
Proof.
355
  iIntros "Hwp H". iApply (wp_strong_mono p E); auto.
356
  iIntros "{$Hwp}" (?) "?". by iApply "H".
357
Qed.
358
359
Lemma wp_wand_l p E e Φ Ψ :
  ( v, Φ v - Ψ v)  WP e @ p; E {{ Φ }}  WP e @ p; E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
360
Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
361
362
Lemma wp_wand_r p E e Φ Ψ :
  WP e @ p; E {{ Φ }}  ( v, Φ v - Ψ v)  WP e @ p; E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
End wp.
365
366
367
368
369
370
371

(** Proofmode class instances *)
Section proofmode_classes.
  Context `{irisG Λ Σ}.
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val Λ  iProp Σ.

372
373
  Global Instance frame_wp p p' E e R Φ Ψ :
    ( v, Frame p' R (Φ v) (Ψ v))  Frame p' R (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Ψ }}).
374
375
  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.

376
  Global Instance is_except_0_wp p E e Φ : IsExcept0 (WP e @ p; E {{ Φ }}).
377
  Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
378

379
380
  Global Instance elim_modal_bupd_wp p E e P Φ :
    ElimModal (|==> P) P (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Φ }}).
381
  Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
382

383
384
  Global Instance elim_modal_fupd_wp p E e P Φ :
    ElimModal (|={E}=> P) P (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Φ }}).
385
  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
386

387
  (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
388
  Global Instance elim_modal_fupd_wp_strong_atomic E1 E2 e P Φ :
389
    StronglyAtomic e 
390
    ElimModal (|={E1,E2}=> P) P
391
            (WP e @ p; E1 {{ Φ }}) (WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
392
393
394
395
396
397
398
  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_strong_atomic. Qed.

  (* lower precedence than elim_modal_fupd_wp_strong_atomic (for no good reason) *)
  Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
    Atomic e 
    ElimModal (|={E1,E2}=> P) P
            (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 110.
399
  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
400
End proofmode_classes.