lifting.v 2.8 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
From iris.base_logic Require Export big_op.
3
From iris.proofmode Require Import tactics.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6

Section lifting.
7
Context `{irisG Λ Σ}.
8 9 10
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
11 12
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

14
Lemma wp_lift_step E Φ e1 :
15 16 17 18 19
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E,}=
    reducible e1 σ1 
      e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
      state_interp σ2  WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
20
   WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Proof. by rewrite wp_unfold /wp_pre=> ->. Qed.
22

23
(** Derived lifting lemmas. *)
24
Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 :
25
  ( σ1, reducible e1 σ1) 
26
  ( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
27
  (|={E,E'}=>  e2 efs σ, prim_step e1 σ e2 σ efs 
28
    WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
29
   WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Proof.
31 32
  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
  { eapply reducible_not_val, (Hsafe inhabitant). }
Ralf Jung's avatar
Ralf Jung committed
33
  iIntros (σ1) "Hσ". iMod "H".
34 35
  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
  iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
36
  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
Ralf Jung's avatar
Ralf Jung committed
37
  iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
Qed.
39

40 41
(* Atomic steps don't need any mask-changing business here, one can
   use the generic lemmas here. *)
42 43 44 45 46 47 48
Lemma wp_lift_atomic_step {E Φ} e1 :
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E}=
    reducible e1 σ1 
      e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E}=
      state_interp σ2 
      default False (to_val e2) Φ  [ list] ef  efs, WP ef {{ _, True }})
49
   WP e1 @ E {{ Φ }}.
50
Proof.
51 52 53 54 55
  iIntros (?) "H". iApply (wp_lift_step E _ e1)=>//; iIntros (σ1) "Hσ1".
  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
  iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
  iModIntro; iNext; iIntros (e2 σ2 efs) "%". iMod "Hclose" as "_".
  iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
56
  destruct (to_val e2) eqn:?; last by iExFalso.
57
  by iApply wp_value.
58 59
Qed.

60
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E E' Φ} e1 e2 efs :
61
  ( σ1, reducible e1 σ1) 
62
  ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
63
  (|={E,E'}=> WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
64
   WP e1 @ E {{ Φ }}.
65
Proof.
66 67
  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
  { by intros; eapply Hpuredet. }
68
  iApply (step_fupd_wand with "H"); iIntros "H".
69
  by iIntros (e' efs' σ (_&->&->)%Hpuredet).
70
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
End lifting.