total_weakestpre.v 19.3 KB
Newer Older
1 2
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
3
From iris.bi Require Import fixpoint big_op.
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
Set Default Proof Using "Type".
Import uPred.

Definition twp_pre `{irisG Λ Σ} (s : stuckness)
      (wp : coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ) :
    coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ := λ E e1 Φ,
  match to_val e1 with
  | Some v => |={E}=> Φ v
  | None =>  σ1,
     state_interp σ1 ={E,}= if s is NotStuck then reducible e1 σ1 else True 
      e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
       state_interp σ2  wp E e2 Φ 
       [ list] ef  efs, wp  ef (λ _, True)
  end%I.

Lemma twp_pre_mono `{irisG Λ Σ} s
    (wp1 wp2 : coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ) :
  ((  E e Φ, wp1 E e Φ - wp2 E e Φ) 
   E e Φ, twp_pre s wp1 E e Φ - twp_pre s wp2 E e Φ)%I.
Proof.
  iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
  destruct (to_val e1) as [v|]; first done.
  iIntros (σ1) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
  iIntros (e2 σ2 efs) "Hstep".
  iMod ("Hwp" with "Hstep") as "($ & Hwp & Hfork)"; iModIntro; iSplitL "Hwp".
  - by iApply "H".
  - iApply (@big_sepL_impl with "[$Hfork]"); iIntros "!#" (k e _) "Hwp".
    by iApply "H".
Qed.

(* Uncurry [twp_pre] and equip its type with an OFE structure *)
Definition twp_pre' `{irisG Λ Σ} (s : stuckness) :
  (prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ)  iProp Σ) 
  prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ)  iProp Σ :=
    curry3  twp_pre s  uncurry3.

40
Local Instance twp_pre_mono' `{irisG Λ Σ} s : BiMonoPred (twp_pre' s).
41 42 43 44 45 46 47 48 49 50 51
Proof.
  constructor.
  - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
    iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
  - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
    rewrite /uncurry3 /twp_pre. do 16 (f_equiv || done). by apply Hwp, pair_ne.
Qed.

Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
    (e : expr Λ) (Φ : val Λ  iProp Σ) :
52
  iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
53 54 55 56 57 58 59 60 61 62 63
Definition twp_aux : seal (@twp_def). by eexists. Qed.
Definition twp := unseal twp_aux.
Definition twp_eq : @twp = @twp_def := seal_eq twp_aux.

Arguments twp {_ _ _} _ _ _%E _.
Instance: Params (@twp) 6.

(* Note that using '[[' instead of '[{' results in conflicts with the list
notations. *)
Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
  (at level 20, e, Φ at level 200,
64
   format "'[' 'WP'  e  '/' @  s ;  E  [{  Φ  } ] ']'") : bi_scope.
65 66
Notation "'WP' e @ E [{ Φ } ]" := (twp NotStuck E e%E Φ)
  (at level 20, e, Φ at level 200,
67
   format "'[' 'WP'  e  '/' @  E  [{  Φ  } ] ']'") : bi_scope.
68 69
Notation "'WP' e @ E ? [{ Φ } ]" := (twp MaybeStuck E e%E Φ)
  (at level 20, e, Φ at level 200,
70
   format "'[' 'WP'  e  '/' @  E  ? [{  Φ  } ] ']'") : bi_scope.
71 72
Notation "'WP' e [{ Φ } ]" := (twp NotStuck  e%E Φ)
  (at level 20, e, Φ at level 200,
73
   format "'[' 'WP'  e  '/' [{  Φ  } ] ']'") : bi_scope.
74 75
Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck  e%E Φ)
  (at level 20, e, Φ at level 200,
76
   format "'[' 'WP'  e  '/' ? [{  Φ  } ] ']'") : bi_scope.
77 78 79

Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
  (at level 20, e, Q at level 200,
80
   format "'[' 'WP'  e  '/' @  s ;  E  [{  v ,  Q  } ] ']'") : bi_scope.
81 82
Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
  (at level 20, e, Q at level 200,
83
   format "'[' 'WP'  e  '/' @  E  [{  v ,  Q  } ] ']'") : bi_scope.
84 85
Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
  (at level 20, e, Q at level 200,
86
   format "'[' 'WP'  e  '/' @  E  ? [{  v ,  Q  } ] ']'") : bi_scope.
87 88
Notation "'WP' e [{ v , Q } ]" := (twp NotStuck  e%E (λ v, Q))
  (at level 20, e, Q at level 200,
89
   format "'[' 'WP'  e  '/' [{  v ,  Q  } ] ']'") : bi_scope.
90 91
Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck  e%E (λ v, Q))
  (at level 20, e, Q at level 200,
92
   format "'[' 'WP'  e  '/' ? [{  v ,  Q  } ] ']'") : bi_scope.
93 94 95 96 97 98

(* Texan triples *)
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,
99
     format "[[{  P  } ] ]  e  @  s ;  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : bi_scope.
100 101 102 103
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,
104
     format "[[{  P  } ] ]  e  @  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : bi_scope.
105 106 107 108
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,
109
     format "[[{  P  } ] ]  e  @  E  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : bi_scope.
110 111 112 113
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,
114
     format "[[{  P  } ] ]  e  [[{  x .. y ,   RET  pat ;  Q } ] ]") : bi_scope.
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,
119
     format "[[{  P  } ] ]  e  ? [[{  x .. y ,   RET  pat ;  Q } ] ]") : bi_scope.
120 121 122
Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
  (  Φ, P - (Q - Φ pat%V) - WP e @ s; E [{ Φ }])%I
    (at level 20,
123
     format "[[{  P  } ] ]  e  @  s ;  E  [[{  RET  pat ;  Q } ] ]") : bi_scope.
124 125 126
Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
  (  Φ, P - (Q - Φ pat%V) - WP e @ E [{ Φ }])%I
    (at level 20,
127
     format "[[{  P  } ] ]  e  @  E  [[{  RET  pat ;  Q } ] ]") : bi_scope.
128 129 130
Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
  (  Φ, P - (Q - Φ pat%V) - WP e @ E ?[{ Φ }])%I
    (at level 20,
131
     format "[[{  P  } ] ]  e  @  E  ? [[{  RET  pat ;  Q } ] ]") : bi_scope.
132 133 134
Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
  (  Φ, P - (Q - Φ pat%V) - WP e [{ Φ }])%I
    (at level 20,
135
     format "[[{  P  } ] ]  e  [[{  RET  pat ;  Q } ] ]") : bi_scope.
136 137 138
Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
  (  Φ, P - (Q - Φ pat%V) - WP e ?[{ Φ }])%I
    (at level 20,
139
     format "[[{  P  } ] ]  e  ? [[{  RET  pat ;  Q } ] ]") : bi_scope.
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224

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,
     format "[[{  P  } ] ]  e  @  s ;  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
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 } ] ]") : stdpp_scope.
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 } ] ]") : stdpp_scope.
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 } ] ]") : stdpp_scope.
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 } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
  ( Φ : _  uPred _, P - (Q - Φ pat%V) - WP e @ s; E [{ Φ }])
    (at level 20,
     format "[[{  P  } ] ]  e  @  s ;  E  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
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 } ] ]") : stdpp_scope.
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 } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
  ( Φ : _  uPred _, P - (Q - Φ pat%V) - WP e [{ Φ }])
    (at level 20,
     format "[[{  P  } ] ]  e  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
  ( Φ : _  uPred _, P - (Q - Φ pat%V) - WP e ?[{ Φ }])
    (at level 20,
     format "[[{  P  } ] ]  e  ? [[{  RET  pat ;  Q } ] ]") : stdpp_scope.

Section twp.
Context `{irisG Λ Σ}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.

(* Weakest pre *)
Lemma twp_unfold s E e Φ : WP e @ s; E [{ Φ }]  twp_pre s (twp s) E e Φ.
Proof. by rewrite twp_eq /twp_def least_fixpoint_unfold. Qed.
Lemma twp_ind s Ψ :
  ( n E e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ E e)) 
  ( ( e E Φ, twp_pre s (λ E e Φ, Ψ E e Φ  WP e @ s; E [{ Φ }]) E e Φ - Ψ E e Φ) 
   e E Φ, WP e @ s; E [{ Φ }] - Ψ E e Φ)%I.
Proof.
  iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
  set (Ψ' := curry3 Ψ :
    prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ)  iProp Σ).
  assert (NonExpansive Ψ').
  { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
  iApply (least_fixpoint_strong_ind _ Ψ' with "[] H").
  iIntros "!#" ([[??] ?]) "H". by iApply "IH".
Qed.

Global Instance twp_ne s E e n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@twp Λ Σ _ s E e).
Proof.
  intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
Qed.
Global Instance twp_proper s E e :
  Proper (pointwise_relation _ () ==> ()) (@twp Λ Σ _ s E e).
Proof.
  by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist.
Qed.

Lemma twp_value' s E Φ v : Φ v - WP of_val v @ s; E [{ Φ }].
Proof. iIntros "HΦ". rewrite twp_unfold /twp_pre to_of_val. auto. Qed.
225
Lemma twp_value_inv' s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}= Φ v.
226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
Proof. by rewrite twp_unfold /twp_pre to_of_val. Qed.

Lemma twp_strong_mono s1 s2 E1 E2 e Φ Ψ :
  s1  s2  E1  E2 
  WP e @ s1; E1 [{ Φ }] - ( v, Φ v ={E2}= Ψ v) - WP e @ s2; E2 [{ Ψ }].
Proof.
  iIntros (? HE) "H HΦ". iRevert (E2 Ψ HE) "HΦ"; iRevert (e E1 Φ) "H".
  iApply twp_ind; first solve_proper.
  iIntros "!#" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
  rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
  iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
  iMod ("IH" with "[$]") as "[% IH]".
  iModIntro; iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
  iMod ("IH" with "[//]") as "($ & IH & IHefs)"; auto.
  iMod "Hclose" as "_"; iModIntro. iSplitR "IHefs".
  - iDestruct "IH" as "[IH _]". iApply ("IH" with "[//] HΦ").
  - iApply (big_sepL_impl with "[$IHefs]"); iIntros "!#" (k ef _) "[IH _]".
    by iApply "IH".
Qed.

247
Lemma fupd_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) - WP e @ s; E [{ Φ }].
248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
Proof.
  rewrite twp_unfold /twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
  { by iMod "H". }
  iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
Qed.
Lemma twp_fupd s E e Φ : WP e @ s; E [{ v, |={E}=> Φ v }] - WP e @ s; E [{ Φ }].
Proof. iIntros "H". iApply (twp_strong_mono with "H"); auto. Qed.

Lemma twp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
  (|={E1,E2}=> WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }]) - WP e @ s; E1 [{ Φ }].
Proof.
  iIntros "H". rewrite !twp_unfold /twp_pre /=.
  destruct (to_val e) as [v|] eqn:He.
  { by iDestruct "H" as ">>> $". }
  iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
  iModIntro. iIntros (e2 σ2 efs Hstep).
  iMod ("H" with "[//]") as "(Hphy & H & $)". destruct s.
  - rewrite !twp_unfold /twp_pre. destruct (to_val e2) as [v2|] eqn:He2.
    + iDestruct "H" as ">> $". by iFrame.
    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
      by edestruct (atomic _ _ _ _ Hstep).
  - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
270
    iMod (twp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
271 272 273 274 275 276 277 278 279 280 281
Qed.

Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
  WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] - WP K e @ s; E [{ Φ }].
Proof.
  revert Φ. cut ( Φ', WP e @ s; E [{ Φ' }] -  Φ,
    ( v, Φ' v - WP K (of_val v) @ s; E [{ Φ }]) - WP K e @ s; E [{ Φ }]).
  { iIntros (help Φ) "H". iApply (help with "H"); auto. }
  iIntros (Φ') "H". iRevert (e E Φ') "H". iApply twp_ind; first solve_proper.
  iIntros "!#" (e E1 Φ') "IH". iIntros (Φ) "HΦ".
  rewrite /twp_pre. destruct (to_val e) as [v|] eqn:He.
282
  { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
  rewrite twp_unfold /twp_pre fill_not_val //.
  iIntros (σ1) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
  { iPureIntro. unfold reducible in *.
    destruct s; naive_solver eauto using fill_step. }
  iIntros (e2 σ2 efs Hstep).
  destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
  iMod ("IH" $! e2' σ2 efs with "[//]") as "($ & IH & IHfork)".
  iModIntro; iSplitR "IHfork".
  - iDestruct "IH" as "[IH _]". by iApply "IH".
  - by setoid_rewrite and_elim_r.
Qed.

Lemma twp_bind_inv K `{!LanguageCtx K} s E e Φ :
  WP K e @ s; E [{ Φ }] - WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }].
Proof.
  iIntros "H". remember (K e) as e' eqn:He'.
  iRevert (e He'). iRevert (e' E Φ) "H". iApply twp_ind; first solve_proper.
  iIntros "!#" (e' E1 Φ) "IH". iIntros (e ->).
  rewrite !twp_unfold {2}/twp_pre. destruct (to_val e) as [v|] eqn:He.
  { iModIntro. apply of_to_val in He as <-. rewrite !twp_unfold.
    iApply (twp_pre_mono with "[] IH"). by iIntros "!#" (E e Φ') "[_ ?]". }
  rewrite /twp_pre fill_not_val //.
  iIntros (σ1) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
  { destruct s; eauto using reducible_fill. }
  iIntros (e2 σ2 efs Hstep).
  iMod ("IH" $! (K e2) σ2 efs with "[]") as "($ & IH & IHfork)"; eauto using fill_step.
  iModIntro; iSplitR "IHfork".
  - iDestruct "IH" as "[IH _]". by iApply "IH".
  - by setoid_rewrite and_elim_r.
Qed.

Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] - WP e @ s; E {{ Φ }}.
Proof.
  iIntros "H". iLöb as "IH" forall (E e Φ).
  rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
  iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iModIntro; iNext.
  iIntros (e2 σ2 efs) "Hstep".
  iMod ("H" with "Hstep") as "($ & H & Hfork)"; iModIntro.
  iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
  iIntros "!#" (k e' _) "H". by iApply "IH".
Qed.

(** * Derived rules *)
Lemma twp_mono s E e Φ Ψ :
  ( v, Φ v - Ψ v)  WP e @ s; E [{ Φ }] - WP e @ s; E [{ Ψ }].
Proof.
  iIntros (HΦ) "H"; iApply (twp_strong_mono with "H"); auto.
  iIntros (v) "?". by iApply HΦ.
Qed.
Lemma twp_stuck_mono s1 s2 E e Φ :
  s1  s2  WP e @ s1; E [{ Φ }]  WP e @ s2; E [{ Φ }].
Proof. iIntros (?) "H". iApply (twp_strong_mono with "H"); auto. Qed.
Lemma twp_stuck_weaken s E e Φ :
  WP e @ s; E [{ Φ }]  WP e @ E ?[{ Φ }].
Proof. apply twp_stuck_mono. by destruct s. Qed.
Lemma twp_mask_mono s E1 E2 e Φ :
  E1  E2  WP e @ s; E1 [{ Φ }] - WP e @ s; E2 [{ Φ }].
Proof. iIntros (?) "H"; iApply (twp_strong_mono with "H"); auto. Qed.
Global Instance twp_mono' s E e :
  Proper (pointwise_relation _ () ==> ()) (@twp Λ Σ _ s E e).
Proof. by intros Φ Φ' ?; apply twp_mono. Qed.

Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v - WP e @ s; E [{ Φ }].
Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value'. Qed.
Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) - WP of_val v @ s; E [{ Φ }].
Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
Lemma twp_value_fupd s E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) - WP e @ s; E [{ Φ }].
Proof. intros. rewrite -twp_fupd -twp_value //. Qed.
351 352
Lemma twp_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 twp_value_inv'. Qed.
353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379

Lemma twp_frame_l s E e Φ R : R  WP e @ s; E [{ Φ }] - WP e @ s; E [{ v, R  Φ v }].
Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
Lemma twp_frame_r s E e Φ R : WP e @ s; E [{ Φ }]  R - WP e @ s; E [{ v, Φ v  R }].
Proof. iIntros "[H ?]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.

Lemma twp_wand s E e Φ Ψ :
  WP e @ s; E [{ Φ }] - ( v, Φ v - Ψ v) - WP e @ s; E [{ Ψ }].
Proof.
  iIntros "H HΦ". iApply (twp_strong_mono with "H"); auto.
  iIntros (?) "?". by iApply "HΦ".
Qed.
Lemma twp_wand_l s E e Φ Ψ :
  ( v, Φ v - Ψ v)  WP e @ s; E [{ Φ }] - WP e @ s; E [{ Ψ }].
Proof. iIntros "[H Hwp]". iApply (twp_wand with "Hwp H"). Qed.
Lemma twp_wand_r s E e Φ Ψ :
  WP e @ s; E [{ Φ }]  ( v, Φ v - Ψ v) - WP e @ s; E [{ Ψ }].
Proof. iIntros "[Hwp H]". iApply (twp_wand with "Hwp H"). Qed.
End twp.

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

  Global Instance frame_twp p s E e R Φ Ψ :
380 381 382
    ( v, Frame p R (Φ v) (Ψ v)) 
    KnownFrame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
  Proof. rewrite /KnownFrame /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
383 384

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

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

  Global Instance elim_modal_fupd_twp s E e P Φ :
392
    ElimModal True (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
393
  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_twp. Qed.
394 395 396

  Global Instance elim_modal_fupd_twp_atomic s E1 E2 e P Φ :
    Atomic (stuckness_to_atomicity s) e 
397
    ElimModal True (|={E1,E2}=> P) P
398
            (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I.
399
  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r twp_atomic. Qed.
400 401 402 403

  Global Instance add_modal_fupd_twp s E e P Φ :
    AddModal (|={E}=> P) P (WP e @ s; E [{ Φ }]).
  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_twp. Qed.
404
End proofmode_classes.