total_weakestpre.v 12.7 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
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).
56 57 58

Section twp.
Context `{irisG Λ Σ}.
59
Implicit Types s : stuckness.
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
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 :
84
  Proper (pointwise_relation _ (dist n) ==> dist n) (twp (PROP:=iProp Σ) s E e).
85 86 87 88
Proof.
  intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
Qed.
Global Instance twp_proper s E e :
89
  Proper (pointwise_relation _ () ==> ()) (twp (PROP:=iProp Σ) s E e).
90 91 92 93 94 95
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.
96
Lemma twp_value_inv' s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}= Φ v.
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
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.

118
Lemma fupd_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) - WP e @ s; E [{ Φ }].
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
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].
141
    iMod (twp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
142 143 144 145 146 147 148 149 150 151 152
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.
153
  { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
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
  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|]=>//.
189 190 191
  iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iIntros "!>".
  iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as "($ & H & Hfork)".
  iApply step_fupd_intro; [set_solver+|]. iNext.
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212
  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 :
213
  Proper (pointwise_relation _ () ==> ()) (twp (PROP:=iProp Σ) s E e).
214 215 216 217 218 219 220 221
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.
222 223
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.
224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250

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

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

258 259 260 261 262 263
  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.
264

265 266 267 268 269 270
  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.
271

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

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