lifting.v 2.62 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 {{ Φ }}.
21
Proof. iIntros (?) "H". rewrite wp_unfold /wp_pre; auto. Qed.
22

23
(** Derived lifting lemmas. *)
24
Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
25
  ( σ1, reducible e1 σ1) 
26
  ( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
Ralf Jung's avatar
Ralf Jung committed
27
  (  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). }
33 34
  iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
  iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
35
  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
36
  iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
Qed.
38

39 40 41 42 43 44 45
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 }})
46
   WP e1 @ E {{ Φ }}.
47
Proof.
48 49 50 51 52
  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.
53
  destruct (to_val e2) eqn:?; last by iExFalso.
54
  by iApply wp_value.
55 56
Qed.

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