weakestpre.v 12.5 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 12
}.
Notation irisG Λ Σ := (irisG' (state Λ) Σ).

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

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

31 32
Definition wp_def `{irisG Λ Σ} :
  coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ := fixpoint wp_pre.
33 34 35
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
36

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

Janno's avatar
Janno committed
40
Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
41
  (at level 20, e, Φ at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
42
   format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : bi_scope.
Janno's avatar
Janno committed
43
Notation "'WP' e {{ Φ } }" := (wp  e%E Φ)
44
  (at level 20, e, Φ at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
45
   format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : bi_scope.
46

Janno's avatar
Janno committed
47
Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
48
  (at level 20, e, Q at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
49
   format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : bi_scope.
Janno's avatar
Janno committed
50
Notation "'WP' e {{ v , Q } }" := (wp  e%E (λ v, Q))
51
  (at level 20, e, Q at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
52
   format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : bi_scope.
53

Ralf Jung's avatar
Ralf Jung committed
54
(* Texan triples *)
55
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
Ralf Jung's avatar
Ralf Jung committed
56
  (  Φ,
57
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
58
    (at level 20, x closed binder, y closed binder,
Robbert Krebbers's avatar
Robbert Krebbers committed
59
     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : bi_scope.
60 61 62 63
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,
Robbert Krebbers's avatar
Robbert Krebbers committed
64
     format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q } } }") : bi_scope.
65
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
66
  (  Φ, P -  (Q - Φ pat%V) - WP e @ E {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
67
    (at level 20,
Robbert Krebbers's avatar
Robbert Krebbers committed
68
     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : bi_scope.
69 70 71
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
  (  Φ, P -  (Q - Φ pat%V) - WP e {{ Φ }})%I
    (at level 20,
Robbert Krebbers's avatar
Robbert Krebbers committed
72
     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
73

74
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
75
  ( Φ : _  uPred _,
76
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})
Ralf Jung's avatar
Ralf Jung committed
77
    (at level 20, x closed binder, y closed binder,
Robbert Krebbers's avatar
Robbert Krebbers committed
78
     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : stdpp_scope.
79 80 81 82
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
83
     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q } } }") : stdpp_scope.
84
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
85
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e @ E {{ Φ }})
Ralf Jung's avatar
Ralf Jung committed
86
    (at level 20,
Robbert Krebbers's avatar
Robbert Krebbers committed
87
     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : stdpp_scope.
88 89 90
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e {{ Φ }})
    (at level 20,
Robbert Krebbers's avatar
Robbert Krebbers committed
91
     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : stdpp_scope.
92

Robbert Krebbers's avatar
Robbert Krebbers committed
93
Section wp.
94 95 96
Context `{irisG Λ Σ}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
97 98
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
99

100
(* Weakest pre *)
101 102 103
Lemma wp_unfold E e Φ : WP e @ E {{ Φ }}  wp_pre wp E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.

104
Global Instance wp_ne E e n :
105
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Proof.
107
  revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
108 109 110 111
  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
112
  do 17 (f_contractive || f_equiv). apply IH; first lia.
113
  intros v. eapply dist_le; eauto with omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115
Qed.
Global Instance wp_proper E e :
116
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Proof.
118
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Qed.
120

121
Lemma wp_value' E Φ v : Φ v  WP of_val v @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
123
Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}= Φ v.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
125

126
Lemma wp_strong_mono E1 E2 e Φ Ψ :
127
  E1  E2  ( v, Φ v ={E2}= Ψ v)  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Ψ }}.
128
Proof.
129
  iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
  destruct (to_val e) as [v|] eqn:?.
131
  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
133
  iMod ("H" with "[$]") as "[$ H]".
134
  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
135
  iMod ("H" with "[//]") as "($ & H & $)"; auto.
136
  iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
137 138
Qed.

139
Lemma fupd_wp E e Φ : (|={E}=> WP e @ E {{ Φ }})  WP e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Proof.
141
  rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143
  { by iMod "H". }
  iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
144
Qed.
145
Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }}  WP e @ E {{ Φ }}.
146
Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
147

148
Lemma wp_atomic E1 E2 e Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  Atomic e 
150
  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
152 153 154 155
  iIntros (Hatomic) "H". rewrite !wp_unfold /wp_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]".
156
  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
157
  iMod ("H" with "[//]") as "(Hphy & H & $)".
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
159 160
  - iDestruct "H" as ">> $". eauto with iFrame.
  - iMod ("H" with "[$]") as "[H _]".
Robbert Krebbers's avatar
Robbert Krebbers committed
161
    iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hatomic _ _ _ _ Hstep).
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Qed.
163

164
Lemma wp_step_fupd E1 E2 e P Φ :
165
  to_val e = None  E2  E1 
166
  (|={E1,E2}=> P) - WP e @ E2 {{ v, P ={E1}= Φ v }} - WP e @ E1 {{ Φ }}.
167
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
169
  iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
170
  iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
171
  iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
172 173
  iMod "HR". iModIntro. iApply (wp_strong_mono E2); first done.
  iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
174
Qed.
175

176
Lemma wp_bind K `{!LanguageCtx K} E e Φ :
177
  WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}  WP K e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
Proof.
179
  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182
  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 //.
183
  iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
184
  { iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
185 186
  iNext; iIntros (e2 σ2 efs Hstep).
  destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
187
  iMod ("H" $! e2' σ2 efs with "[//]") as "($ & H & $)".
188
  by iApply "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
189 190
Qed.

191
Lemma wp_bind_inv K `{!LanguageCtx K} E e Φ :
192 193 194 195 196 197 198 199 200 201 202 203 204
  WP K e @ E {{ Φ }}  WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}.
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.
  { eauto using reducible_fill. }
  iNext; iIntros (e2 σ2 efs Hstep).
  iMod ("H" $! (K e2) σ2 efs with "[]") as "($ & H & $)"; eauto using fill_step.
  by iApply "IH".
Qed.

205
(** * Derived rules *)
206
Lemma wp_mono E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
207 208
Proof.
  iIntros (HΦ) "H"; iApply (wp_strong_mono E E); auto.
209
  iIntros "{$H}" (v) "?". by iApply HΦ.
210 211 212
Qed.
Lemma wp_mask_mono E1 E2 e Φ : E1  E2  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Φ }}.
Proof. iIntros (?) "H"; iApply (wp_strong_mono E1 E2); auto. iFrame; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
Global Instance wp_mono' E e :
214
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
215
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
216

217
Lemma wp_value E Φ e v `{!IntoVal e v} : Φ v  WP e @ E {{ Φ }}.
218
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
219 220
Lemma wp_value_fupd' E Φ v : (|={E}=> Φ v)  WP of_val v @ E {{ Φ }}.
Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
221
Lemma wp_value_fupd E Φ e v `{!IntoVal e v} : (|={E}=> Φ v)  WP e @ E {{ Φ }}.
222
Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
223

224
Lemma wp_frame_l E e Φ R : R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
225
Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
226
Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }}  R  WP e @ E {{ v, Φ v  R }}.
227 228
Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.

229 230 231 232
Lemma wp_frame_step_l E1 E2 e Φ R :
  to_val e = None  E2  E1 
  (|={E1,E2}=> R)  WP e @ E2 {{ Φ }}  WP e @ E1 {{ v, R  Φ v }}.
Proof.
233
  iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
234 235
  iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
Qed.
236 237
Lemma wp_frame_step_r E1 E2 e Φ R :
  to_val e = None  E2  E1 
238
  WP e @ E2 {{ Φ }}  (|={E1,E2}=> R)  WP e @ E1 {{ v, Φ v  R }}.
Ralf Jung's avatar
Ralf Jung committed
239
Proof.
240
  rewrite [(WP _ @ _ {{ _ }}  _)%I]comm; setoid_rewrite (comm _ _ R).
241
  apply wp_frame_step_l.
Ralf Jung's avatar
Ralf Jung committed
242 243
Qed.
Lemma wp_frame_step_l' E e Φ R :
244
  to_val e = None   R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
245 246
Proof. iIntros (?) "[??]". iApply (wp_frame_step_l E E); try iFrame; eauto. Qed.
Lemma wp_frame_step_r' E e Φ R :
247
  to_val e = None  WP e @ E {{ Φ }}   R  WP e @ E {{ v, Φ v  R }}.
248 249
Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
250
Lemma wp_wand E e Φ Ψ :
251
  WP e @ E {{ Φ }} - ( v, Φ v - Ψ v) - WP e @ E {{ Ψ }}.
252
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
  iIntros "Hwp H". iApply (wp_strong_mono E); auto.
254
  iIntros "{$Hwp}" (?) "?". by iApply "H".
255
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256 257 258
Lemma wp_wand_l E e Φ Ψ :
  ( v, Φ v - Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
259
Lemma wp_wand_r E e Φ Ψ :
260
  WP e @ E {{ Φ }}  ( v, Φ v - Ψ v)  WP e @ E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
262
End wp.
263 264 265 266 267 268 269

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

270 271
  Global Instance frame_wp p E e R Φ Ψ :
    ( v, Frame p R (Φ v) (Ψ v))  Frame p R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
272 273
  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.

274 275
  Global Instance is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).
  Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
276

277 278 279
  Global Instance elim_modal_bupd_wp E e P Φ :
    ElimModal (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
  Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
280

281 282 283
  Global Instance elim_modal_fupd_wp E e P Φ :
    ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
284

285
  (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
286
  Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
287
    Atomic e 
288
    ElimModal (|={E1,E2}=> P) P
289
            (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
290
  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
291
End proofmode_classes.