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

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

Ralf Jung's avatar
Ralf Jung committed
14
Inductive stuckness := NotStuck | MaybeStuck.
Ralf Jung's avatar
Ralf Jung committed
15

16
Definition stuckness_leb (s1 s2 : stuckness) : bool :=
Ralf Jung's avatar
Ralf Jung committed
17
  match s1, s2 with
Ralf Jung's avatar
Ralf Jung committed
18
  | MaybeStuck, NotStuck => false
Ralf Jung's avatar
Ralf Jung committed
19
20
  | _, _ => true
  end.
21
22
23
Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
Instance stuckness_le_po : PreOrder stuckness_le.
Proof. split; by repeat intros []. Qed.
Ralf Jung's avatar
Ralf Jung committed
24

Ralf Jung's avatar
Ralf Jung committed
25
Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
Ralf Jung's avatar
Ralf Jung committed
26
  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
Ralf Jung's avatar
Ralf Jung committed
27

28
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
29
    (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
30
31
32
33
    coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
  match to_val e1 with
  | Some v => |={E}=> Φ v
  | None =>  σ1,
Ralf Jung's avatar
Ralf Jung committed
34
     state_interp σ1 ={E,}= if s is NotStuck then reducible e1 σ1 else True 
35
      e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,,E}=
36
       state_interp σ2  wp E e2 Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
       [ list] ef  efs, wp  ef (λ _, True)
  end%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
39

40
Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).
41
42
Proof.
  rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
43
  repeat (f_contractive || f_equiv); apply Hwp.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Qed.
45

46
Definition wp_def `{irisG Λ Σ} (s : stuckness) :
47
  coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ := fixpoint (wp_pre s).
48
Definition wp_aux : seal (@wp_def). by eexists. Qed.
49
50
Definition wp := wp_aux.(unseal).
Definition wp_eq : @wp = @wp_def := wp_aux.(seal_eq).
Ralf Jung's avatar
Ralf Jung committed
51

52
53
Arguments wp {_ _ _} _ _ _%E _.
Instance: Params (@wp) 6.
Robbert Krebbers's avatar
Robbert Krebbers committed
54

55
56
Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
  (at level 20, e, Φ at level 200,
57
   format "'[' 'WP'  e  '/' @  s ;  E  {{  Φ  } } ']'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
58
Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
59
  (at level 20, e, Φ at level 200,
60
   format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
61
Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
62
  (at level 20, e, Φ at level 200,
63
   format "'[' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
64
Notation "'WP' e {{ Φ } }" := (wp NotStuck  e%E Φ)
65
  (at level 20, e, Φ at level 200,
66
   format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
67
Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck  e%E Φ)
68
  (at level 20, e, Φ at level 200,
69
   format "'[' 'WP'  e  '/' ? {{  Φ  } } ']'") : bi_scope.
70

71
72
Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
  (at level 20, e, Q at level 200,
73
   format "'[' 'WP'  e  '/' @  s ;  E  {{  v ,  Q  } } ']'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
74
Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
75
  (at level 20, e, Q at level 200,
76
   format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
77
Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
78
  (at level 20, e, Q at level 200,
79
   format "'[' 'WP'  e  '/' @  E  ? {{  v ,  Q  } } ']'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
80
Notation "'WP' e {{ v , Q } }" := (wp NotStuck  e%E (λ v, Q))
81
  (at level 20, e, Q at level 200,
82
   format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
83
Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck  e%E (λ v, Q))
84
  (at level 20, e, Q at level 200,
85
   format "'[' 'WP'  e  '/' ? {{  v ,  Q  } } ']'") : bi_scope.
86

Ralf Jung's avatar
Ralf Jung committed
87
(* Texan triples *)
88
89
90
91
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
  (  Φ,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ s; E {{ Φ }})%I
    (at level 20, x closed binder, y closed binder,
92
     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
93
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
Ralf Jung's avatar
Ralf Jung committed
94
  (  Φ,
95
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
96
    (at level 20, x closed binder, y closed binder,
97
     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
98
99
100
101
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,
102
     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
103
104
105
106
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,
107
     format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q  } } }") : bi_scope.
108
109
110
111
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,
112
     format "{{{  P  } } }  e  ? {{{  x .. y ,   RET  pat ;  Q  } } }") : bi_scope.
113
114
115
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e @ s; E {{ Φ }})%I
    (at level 20,
116
     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q  } } }") : bi_scope.
117
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
118
  (  Φ, P -  (Q - Φ pat%V) - WP e @ E {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
119
    (at level 20,
120
     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q  } } }") : bi_scope.
121
122
123
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e @ E ?{{ Φ }})%I
    (at level 20,
124
     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q  } } }") : bi_scope.
125
126
127
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e {{ Φ }})%I
    (at level 20,
128
     format "{{{  P  } } }  e  {{{  RET  pat ;  Q  } } }") : bi_scope.
129
130
131
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e ?{{ Φ }})%I
    (at level 20,
132
     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q  } } }") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
133

134
135
136
137
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _,
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ s; E {{ Φ }})
    (at level 20, x closed binder, y closed binder,
138
     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
139
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
140
  ( Φ : _  uPred _,
141
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})
Ralf Jung's avatar
Ralf Jung committed
142
    (at level 20, x closed binder, y closed binder,
143
     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
144
145
146
147
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,
148
     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
149
150
151
152
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,
153
     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
154
155
156
157
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,
158
     format "{{{  P  } } }  e  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
159
160
161
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e @ s; E {{ Φ }})
    (at level 20,
162
     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
163
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
164
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e @ E {{ Φ }})
Ralf Jung's avatar
Ralf Jung committed
165
    (at level 20,
166
     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
167
168
169
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e @ E ?{{ Φ }})
    (at level 20,
170
     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q  } } }") : stdpp_scope.
171
172
173
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e {{ Φ }})
    (at level 20,
174
     format "{{{  P  } } }  e  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
175
176
177
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e ?{{ Φ }})
    (at level 20,
178
     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q  } } }") : stdpp_scope.
179

Robbert Krebbers's avatar
Robbert Krebbers committed
180
Section wp.
181
Context `{irisG Λ Σ}.
182
Implicit Types s : stuckness.
183
184
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
185
186
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
187

188
(* Weakest pre *)
189
190
Lemma wp_unfold s E e Φ : WP e @ s; E {{ Φ }}  wp_pre s (wp s) E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
191

192
193
Global Instance wp_ne s E e n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ s E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
194
Proof.
195
  revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
196
197
198
199
  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 *)
200
  do 18 (f_contractive || f_equiv). apply IH; first lia.
201
  intros v. eapply dist_le; eauto with omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
Qed.
203
204
Global Instance wp_proper s E e :
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ s E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Proof.
206
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Qed.
208

209
Lemma wp_value' s E Φ v : Φ v  WP of_val v @ s; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
211
Lemma wp_value_inv' s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}= Φ v.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213

214
215
Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
  s1  s2  E1  E2 
216
  WP e @ s1; E1 {{ Φ }} - ( v, Φ v ={E2}= Ψ v) - WP e @ s2; E2 {{ Ψ }}.
217
Proof.
218
  iIntros (? HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
219
  rewrite !wp_unfold /wp_pre.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  destruct (to_val e) as [v|] eqn:?.
221
  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
222
  iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
223
  iMod ("H" with "[$]") as "[% H]".
224
225
  iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
  iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & Hefs)".
226
  iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
227
  - iApply ("IH" with "[//] H HΦ").
228
  - iApply (big_sepL_impl with "[$Hefs]"); iIntros "!#" (k ef _) "H".
229
    by iApply ("IH" with "[] H").
230
231
232
Qed.

Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }})  WP e @ s; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
Proof.
234
  rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
  { by iMod "H". }
  iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
237
Qed.
238
Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }}  WP e @ s; E {{ Φ }}.
239
Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
240

Ralf Jung's avatar
Ralf Jung committed
241
Lemma wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
242
  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ s; E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
Proof.
David Swasey's avatar
David Swasey committed
244
  iIntros "H". rewrite !wp_unfold /wp_pre.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
246
247
  destruct (to_val e) as [v|] eqn:He.
  { by iDestruct "H" as ">>> $". }
  iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
248
249
  iModIntro. iIntros (e2 σ2 efs Hstep).
  iMod ("H" with "[//]") as "H". iIntros "!>!>". iMod "H" as "(Hphy & H & $)". destruct s.
250
  - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
David Swasey's avatar
David Swasey committed
251
252
    + iDestruct "H" as ">> $". by iFrame.
    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
Ralf Jung's avatar
Ralf Jung committed
253
254
      by edestruct (atomic _ _ _ _ Hstep).
  - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
255
    iMod (wp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
Qed.
257

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

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

286
Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
287
  WP K e @ s; E {{ Φ }}  WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
288
289
290
291
292
293
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.
294
  { destruct s; eauto using reducible_fill. }
295
296
297
  iIntros (e2 σ2 efs Hstep).
  iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
  iIntros "!>!>". iMod "H" as "($ & H & $)". by iApply "IH".
298
299
Qed.

300
(** * Derived rules *)
301
Lemma wp_mono s E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ s; E {{ Φ }}  WP e @ s; E {{ Ψ }}.
302
Proof.
303
304
  iIntros (HΦ) "H"; iApply (wp_strong_mono with "H"); auto.
  iIntros (v) "?". by iApply HΦ.
305
Qed.
David Swasey's avatar
David Swasey committed
306
Lemma wp_stuck_mono s1 s2 E e Φ :
307
  s1  s2  WP e @ s1; E {{ Φ }}  WP e @ s2; E {{ Φ }}.
308
Proof. iIntros (?) "H". iApply (wp_strong_mono with "H"); auto. Qed.
309
310
311
Lemma wp_stuck_weaken s E e Φ :
  WP e @ s; E {{ Φ }}  WP e @ E ?{{ Φ }}.
Proof. apply wp_stuck_mono. by destruct s. Qed.
312
Lemma wp_mask_mono s E1 E2 e Φ : E1  E2  WP e @ s; E1 {{ Φ }}  WP e @ s; E2 {{ Φ }}.
313
Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
314
315
Global Instance wp_mono' s E e :
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ s E e).
316
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
317

318
Lemma wp_value s E Φ e v `{!IntoVal e v} : Φ v  WP e @ s; E {{ Φ }}.
319
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
320
Lemma wp_value_fupd' s E Φ v : (|={E}=> Φ v)  WP of_val v @ s; E {{ Φ }}.
321
Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
322
323
Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
  (|={E}=> Φ v)  WP e @ s; E {{ Φ }}.
324
Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
325
326
Lemma wp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E {{ Φ }} ={E}= Φ v.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value_inv'. Qed.
327

328
Lemma wp_frame_l s E e Φ R : R  WP e @ s; E {{ Φ }}  WP e @ s; E {{ v, R  Φ v }}.
329
Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
330
Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }}  R  WP e @ s; E {{ v, Φ v  R }}.
331
Proof. iIntros "[H ?]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
332

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

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

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

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

379
  Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
380
  Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
381

382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
  Global Instance elim_modal_bupd_wp p s E e P Φ :
    ElimModal True p false (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
  Proof.
    by rewrite /ElimModal intuitionistically_if_elim
      (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp.
  Qed.

  Global Instance elim_modal_fupd_wp p s E e P Φ :
    ElimModal True p false (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
  Proof.
    by rewrite /ElimModal intuitionistically_if_elim
      fupd_frame_r wand_elim_r fupd_wp.
  Qed.

  Global Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
Ralf Jung's avatar
Ralf Jung committed
397
    Atomic (stuckness_to_atomicity s) e 
398
    ElimModal True p false (|={E1,E2}=> P) P
399
            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
400
401
402
403
  Proof.
    intros. by rewrite /ElimModal intuitionistically_if_elim
      fupd_frame_r wand_elim_r wp_atomic.
  Qed.
404
405
406
407

  Global Instance add_modal_fupd_wp s E e P Φ :
    AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
Ralf Jung's avatar
Ralf Jung committed
408

Ralf Jung's avatar
Ralf Jung committed
409
  Global Instance elim_acc_wp {X} E1 E2 α β γ e s Φ :
Ralf Jung's avatar
Ralf Jung committed
410
    Atomic (stuckness_to_atomicity s) e 
411
412
    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
            α β γ (WP e @ s; E1 {{ Φ }})
413
            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x  coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
Ralf Jung's avatar
Ralf Jung committed
414
  Proof.
Ralf Jung's avatar
Ralf Jung committed
415
    intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
416
417
    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
    iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
418
    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
Ralf Jung's avatar
Ralf Jung committed
419
420
  Qed.

Ralf Jung's avatar
Ralf Jung committed
421
  Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
422
423
    ElimAcc (X:=X) (fupd E E) (fupd E E)
            α β γ (WP e @ s; E {{ Φ }})
424
            (λ x, WP e @ s; E {{ v, |={E}=> β x  coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
Ralf Jung's avatar
Ralf Jung committed
425
  Proof.
Ralf Jung's avatar
Ralf Jung committed
426
    rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
427
428
429
    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
    iApply wp_fupd.
    iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
430
    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
Ralf Jung's avatar
Ralf Jung committed
431
432
  Qed.

433
End proofmode_classes.