lifting.v 3.32 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
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E,}=
17
    reducible e1 σ1 
18
      e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
19 20 21
      state_interp σ2  WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
Proof. by rewrite wp_unfold /wp_pre=> ->. Qed.
22

23
(** Derived lifting lemmas. *)
24 25
Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 :
  ( σ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 29
    WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
   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
Lemma wp_lift_atomic_step {E Φ} e1 :
43 44
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E}=
45
    reducible e1 σ1 
46 47
      e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E}=
      state_interp σ2 
48 49
      default False (to_val e2) Φ  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
50
Proof.
51
  iIntros (?) "H". iApply (wp_lift_step E _ e1)=>//; iIntros (σ1) "Hσ1".
52 53 54 55
  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 61
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E E' Φ} e1 e2 efs :
  ( σ1, reducible e1 σ1) 
62
  ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
63 64
  (|={E,E'}=> WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
65
Proof.
66
  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
67
  { by intros; eapply Hpuredet. }
68
  iApply (step_fupd_wand with "H"); iIntros "H".
69
  by iIntros (e' efs' σ (_&->&->)%Hpuredet).
70
Qed.
Dan Frumin's avatar
Dan Frumin committed
71

72
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} E E' e1 e2 φ Φ :
Dan Frumin's avatar
Dan Frumin committed
73 74
  PureExec φ e1 e2 
  φ 
75
  (|={E,E'}=> WP e2 @ E {{ Φ }})  WP e1 @ E {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
76 77
Proof.
  iIntros ([??] Hφ) "HWP".
78 79
  iApply (wp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|].
  rewrite big_sepL_nil right_id //.
Dan Frumin's avatar
Dan Frumin committed
80 81
Qed.

82
Lemma wp_pure_step_later `{Inhabited (state Λ)} E e1 e2 φ Φ :
Dan Frumin's avatar
Dan Frumin committed
83 84
  PureExec φ e1 e2 
  φ 
85
   WP e2 @ E {{ Φ }}  WP e1 @ E {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
86 87 88
Proof.
  intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
End lifting.