total_weakestpre.v 12.9 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
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
12
  | None =>  σ1 κs,
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
13 14 15 16
     state_interp σ1 κs ={E,}= if s is NotStuck then reducible_no_obs e1 σ1 else True 
      κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={,E}=
       ⌜κ = None  state_interp σ2 κs 
       wp E e2 Φ  [ list] ef  efs, wp  ef (λ _, True)
17 18 19 20 21 22 23 24 25
  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.
26
  iIntros (σ1 κs) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
27 28 29
  iIntros (κ e2 σ2 efs) "Hstep".
  iMod ("Hwp" with "Hstep") as "($ & $ & Hwp & Hfork)"; iModIntro.
  iSplitL "Hwp".
30 31 32 33 34 35 36 37 38 39 40
  - 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.

41
Local Instance twp_pre_mono' `{irisG Λ Σ} s : BiMonoPred (twp_pre' s).
42 43 44 45 46 47
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/=.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
48
    rewrite /uncurry3 /twp_pre. do 22 (f_equiv || done). by apply pair_ne.
49 50 51 52
Qed.

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

Section twp.
Context `{irisG Λ Σ}.
60
Implicit Types s : stuckness.
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
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 :
85
  Proper (pointwise_relation _ (dist n) ==> dist n) (twp (PROP:=iProp Σ) s E e).
86 87 88 89
Proof.
  intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
Qed.
Global Instance twp_proper s E e :
90
  Proper (pointwise_relation _ () ==> ()) (twp (PROP:=iProp Σ) s E e).
91 92 93 94 95 96
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.
97
Lemma twp_value_inv' s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}= Φ v.
98 99 100 101 102 103 104 105 106 107 108
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 _). }
109
  iIntros (σ1 κs) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
110
  iMod ("IH" with "[$]") as "[% IH]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
111 112
  iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
  iMod ("IH" with "[//]") as "($ & $ & IH & IHefs)"; auto.
113 114 115 116 117 118
  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.

119
Lemma fupd_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) - WP e @ s; E [{ Φ }].
120 121 122
Proof.
  rewrite twp_unfold /twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
  { by iMod "H". }
123
  iIntros (σ1 κs) "Hσ1". iMod "H". by iApply "H".
124 125 126 127 128 129 130 131 132 133
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 ">>> $". }
134
  iIntros (σ1 κs) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
135 136
  iModIntro. iIntros (κ e2 σ2 efs Hstep).
  iMod ("H" with "[//]") as "(% & Hphy & H & $)". destruct s.
137 138
  - rewrite !twp_unfold /twp_pre. destruct (to_val e2) as [v2|] eqn:He2.
    + iDestruct "H" as ">> $". by iFrame.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
139
    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
140 141
      by edestruct (atomic _ _ _ _ _ Hstep).
  - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
142 143
    iMod (twp_value_inv' with "H") as ">H". iModIntro. iSplit; first done.
    iFrame "Hphy". by iApply twp_value'.
144 145 146 147 148 149 150 151 152 153 154
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.
155
  { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
156
  rewrite twp_unfold /twp_pre fill_not_val //.
157
  iIntros (σ1 κs) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
158
  { iPureIntro. unfold reducible_no_obs in *.
159
    destruct s; naive_solver eauto using fill_step. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
160
  iIntros (κ e2 σ2 efs Hstep).
161
  destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
162
  iMod ("IH" $! κ e2' σ2 efs with "[//]") as "($ & $ & IH & IHfork)".
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
  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 //.
178
  iIntros (σ1 κs) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
179 180 181
  { destruct s; eauto using reducible_no_obs_fill. }
  iIntros (κ e2 σ2 efs Hstep).
  iMod ("IH" $! κ (K e2) σ2 efs with "[]") as "($ & $ & IH & IHfork)"; eauto using fill_step.
182 183 184 185 186 187 188 189 190
  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|]=>//.
191
  iIntros (σ1 κ κs) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
192
  { destruct s; last done. eauto using reducible_no_obs_reducible. }
193
  iIntros (e2 σ2 efs Hstep). iMod ("H" $! _ _ _ _ Hstep) as "(% & Hst & H & Hfork)".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
194
  subst κ. iFrame "Hst".
195
  iApply step_fupd_intro; [set_solver+|]. iNext.
196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
  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 :
217
  Proper (pointwise_relation _ () ==> ()) (twp (PROP:=iProp Σ) s E e).
218 219
Proof. by intros Φ Φ' ?; apply twp_mono. Qed.

220 221
Lemma twp_value s E Φ e v : IntoVal e v  Φ v - WP e @ s; E [{ Φ }].
Proof. intros <-. by apply twp_value'. Qed.
222 223
Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) - WP of_val v @ s; E [{ Φ }].
Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
224 225 226 227
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.
Lemma twp_value_inv s E Φ e v : IntoVal e v  WP e @ s; E [{ Φ }] ={E}= Φ v.
Proof. intros <-. by apply twp_value_inv'. Qed.
228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254

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 Φ Ψ :
255
    ( v, Frame p R (Φ v) (Ψ v)) 
256 257
    Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
  Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
258 259

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

262 263 264 265 266 267
  Global Instance elim_modal_bupd_twp 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_twp.
  Qed.
268

269 270 271 272 273 274
  Global Instance elim_modal_fupd_twp 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_twp.
  Qed.
275

276
  Global Instance elim_modal_fupd_twp_atomic p s E1 E2 e P Φ :
277
    Atomic (stuckness_to_atomicity s) e 
278
    ElimModal True p false (|={E1,E2}=> P) P
279
            (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I.
280 281 282 283
  Proof.
    intros. by rewrite /ElimModal intuitionistically_if_elim
      fupd_frame_r wand_elim_r twp_atomic.
  Qed.
284 285 286 287

  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.
288
End proofmode_classes.