weakestpre.v 18.6 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 Λ) Σ).

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

Ralf Jung's avatar
Ralf Jung committed
16 17
Definition stuckness_le (s1 s2 : stuckness) : bool :=
  match s1, s2 with
Ralf Jung's avatar
Ralf Jung committed
18
  | MaybeStuck, NotStuck => false
Ralf Jung's avatar
Ralf Jung committed
19 20 21 22 23 24
  | _, _ => true
  end.
Instance: PreOrder stuckness_le.
Proof.
  split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
Qed.
25
Instance: SqSubsetEq stuckness := stuckness_le.
Ralf Jung's avatar
Ralf Jung committed
26

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

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

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

48 49
Definition wp_def `{irisG Λ Σ} s :
  coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ := fixpoint (wp_pre s).
50 51 52
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
53

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

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

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

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

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

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

190
(* Weakest pre *)
191 192
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.
193

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

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

216 217
Lemma wp_strong_mono s E1 E2 e Φ Ψ :
  E1  E2  ( v, Φ v ={E2}= Ψ v)  WP e @ s; E1 {{ Φ }}  WP e @ s; E2 {{ Ψ }}.
218
Proof.
219
  iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). 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
  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
225
  iMod ("H" with "[//]") as "($ & H & $)"; auto.
226
  iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
227 228
Qed.

David Swasey's avatar
David Swasey committed
229
Lemma wp_stuck_weaken s E e Φ :
230 231 232 233 234 235 236 237 238 239 240 241 242 243
  WP e @ s; 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 s E e Φ : (|={E}=> WP e @ s; E {{ Φ }})  WP e @ s; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
Proof.
245
  rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
Robbert Krebbers's avatar
Robbert Krebbers committed
246 247
  { by iMod "H". }
  iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
248
Qed.
249 250
Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }}  WP e @ s; E {{ Φ }}.
Proof. iIntros "H". iApply (wp_strong_mono s E); try iFrame; auto. Qed.
251

Ralf Jung's avatar
Ralf Jung committed
252
Lemma wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
253 254
  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ s; E1 {{ Φ }}.
Proof.
David Swasey's avatar
David Swasey committed
255
  iIntros "H". rewrite !wp_unfold /wp_pre.
256 257 258
  destruct (to_val e) as [v|] eqn:He.
  { by iDestruct "H" as ">>> $". }
  iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
David Swasey's avatar
David Swasey committed
259 260 261 262 263
  iModIntro. iNext. iIntros (e2 σ2 efs Hstep). destruct s.
  - iMod ("H" with "[//]") as "(Hphy & H & $)".
    rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
    + iDestruct "H" as ">> $". by iFrame.
    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
Ralf Jung's avatar
Ralf Jung committed
264 265
      by edestruct (atomic _ _ _ _ Hstep).
  - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
David Swasey's avatar
David Swasey committed
266 267
    iMod ("H" with "[#]") as "($ & H & $)"; first done.
    iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
Qed.
269

270
Lemma wp_step_fupd s E1 E2 e P Φ :
271
  to_val e = None  E2  E1 
272
  (|={E1,E2}=> P) - WP e @ s; E2 {{ v, P ={E1}= Φ v }} - WP e @ s; E1 {{ Φ }}.
273
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
  rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
275
  iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
276
  iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
277
  iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
278
  iMod "HR". iModIntro. iApply (wp_strong_mono s E2); first done.
279
  iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
280
Qed.
281

282
Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
283
  WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}  WP K e @ s; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
Proof.
285
  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
Robbert Krebbers's avatar
Robbert Krebbers committed
286 287 288
  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 //.
289
  iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
290 291
  { iPureIntro. destruct s; last done.
    unfold reducible in *. naive_solver eauto using fill_step. }
292 293
  iNext; iIntros (e2 σ2 efs Hstep).
  destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
294
  iMod ("H" $! e2' σ2 efs with "[//]") as "($ & H & $)".
295
  by iApply "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
296 297
Qed.

298
Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
299
  WP K e @ s; E {{ Φ }}  WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
300 301 302 303 304 305
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.
306
  { destruct s; eauto using reducible_fill. }
307 308 309 310 311
  iNext; iIntros (e2 σ2 efs Hstep).
  iMod ("H" $! (K e2) σ2 efs with "[]") as "($ & H & $)"; eauto using fill_step.
  by iApply "IH".
Qed.

312
(** * Derived rules *)
313
Lemma wp_mono s E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ s; E {{ Φ }}  WP e @ s; E {{ Ψ }}.
314
Proof.
315
  iIntros (HΦ) "H"; iApply (wp_strong_mono s E E); auto.
316
  iIntros "{$H}" (v) "?". by iApply HΦ.
317
Qed.
David Swasey's avatar
David Swasey committed
318
Lemma wp_stuck_mono s1 s2 E e Φ :
319
  s1  s2  WP e @ s1; E {{ Φ }}  WP e @ s2; E {{ Φ }}.
David Swasey's avatar
David Swasey committed
320
Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed.
321 322 323 324
Lemma wp_mask_mono s E1 E2 e Φ : E1  E2  WP e @ s; E1 {{ Φ }}  WP e @ s; E2 {{ Φ }}.
Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed.
Global Instance wp_mono' s E e :
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ s E e).
325
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
326

327
Lemma wp_value s E Φ e v `{!IntoVal e v} : Φ v  WP e @ s; E {{ Φ }}.
328
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
329
Lemma wp_value_fupd' s E Φ v : (|={E}=> Φ v)  WP of_val v @ s; E {{ Φ }}.
330
Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
331 332
Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
  (|={E}=> Φ v)  WP e @ s; E {{ Φ }}.
333
Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
334

335 336 337 338 339 340
Lemma wp_frame_l s E e Φ R : R  WP e @ s; E {{ Φ }}  WP e @ s; E {{ v, R  Φ v }}.
Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.
Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }}  R  WP e @ s; E {{ v, Φ v  R }}.
Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.

Lemma wp_frame_step_l s E1 E2 e Φ R :
341
  to_val e = None  E2  E1 
342
  (|={E1,E2}=> R)  WP e @ s; E2 {{ Φ }}  WP e @ s; E1 {{ v, R  Φ v }}.
343
Proof.
344
  iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
345 346
  iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
Qed.
347
Lemma wp_frame_step_r s E1 E2 e Φ R :
348
  to_val e = None  E2  E1 
349
  WP e @ s; E2 {{ Φ }}  (|={E1,E2}=> R)  WP e @ s; E1 {{ v, Φ v  R }}.
Ralf Jung's avatar
Ralf Jung committed
350
Proof.
351
  rewrite [(WP _ @ _; _ {{ _ }}  _)%I]comm; setoid_rewrite (comm _ _ R).
352
  apply wp_frame_step_l.
Ralf Jung's avatar
Ralf Jung committed
353
Qed.
354 355 356 357 358 359 360 361 362
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 {{ Ψ }}.
363
Proof.
364
  iIntros "Hwp H". iApply (wp_strong_mono s E); auto.
365
  iIntros "{$Hwp}" (?) "?". by iApply "H".
366
Qed.
367 368
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
369
Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
370 371
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
372
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
End wp.
374 375 376 377 378 379 380

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

381 382
  Global Instance frame_wp p s E e R Φ Ψ :
    ( v, Frame p R (Φ v) (Ψ v))  Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
383 384
  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.

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

388 389
  Global Instance elim_modal_bupd_wp s E e P Φ :
    ElimModal (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
390
  Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
391

392 393
  Global Instance elim_modal_fupd_wp s E e P Φ :
    ElimModal (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
394
  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
395

396
  (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
397
  Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
Ralf Jung's avatar
Ralf Jung committed
398
    Atomic (stuckness_to_atomicity s) e 
399
    ElimModal (|={E1,E2}=> P) P
400
            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
401
  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
402
End proofmode_classes.
Ralf Jung's avatar
Ralf Jung committed
403