ectx_lifting.v 4.08 KB
Newer Older
1
(** Some derived lemmas for ectx-based languages *)
2
From iris.program_logic Require Export ectx_language weakestpre lifting.
3
From iris.proofmode Require Import tactics.
4
Set Default Proof Using "Type".
5 6

Section wp.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
8
Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
9 10
Implicit Types P : iProp Σ.
Implicit Types Φ : val  iProp Σ.
11 12
Implicit Types v : val.
Implicit Types e : expr.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
Hint Resolve head_prim_reducible head_reducible_prim_step.
14

15 16
Lemma wp_ectx_bind {E Φ} K e :
  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
17 18
Proof. apply: weakestpre.wp_bind. Qed.

19 20
Lemma wp_ectx_bind_inv {E Φ} K e :
  WP fill K e @ E {{ Φ }}  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}.
21 22
Proof. apply: weakestpre.wp_bind_inv. Qed.

23
Lemma wp_lift_head_step {E Φ} e1 :
24 25 26 27
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E,}=
    head_reducible e1 σ1 
      e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={,E}=
28 29
      state_interp σ2  WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
30
Proof.
31 32 33 34
  iIntros (?) "H". iApply (wp_lift_step E)=>//. iIntros (σ1) "Hσ".
  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%".
  iApply "H". by eauto.
35 36
Qed.

37
Lemma wp_lift_pure_head_step {E E' Φ} e1 :
38
  ( σ1, head_reducible e1 σ1) 
39
  ( σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
40
  (|={E,E'}=>  e2 efs σ, head_step e1 σ e2 σ efs 
41 42
    WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
43
Proof using Hinh.
44
  iIntros (??) "H". iApply wp_lift_pure_step; eauto.
45 46
  iApply (step_fupd_wand with "H"); iIntros "H".
  iIntros (????). iApply "H"; eauto.
47
Qed.
48

49
Lemma wp_lift_atomic_head_step {E Φ} e1 :
50 51 52 53 54
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E}=
    head_reducible e1 σ1 
      e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}=
      state_interp σ2 
55 56
      default False (to_val e2) Φ  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
57 58
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
59 60
  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%". iApply "H"; auto.
61 62
Qed.

63
Lemma wp_lift_atomic_head_step_no_fork {E Φ} e1 :
64 65 66 67 68
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E}=
    head_reducible e1 σ1 
      e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}=
      efs = []  state_interp σ2  default False (to_val e2) Φ)
69
   WP e1 @ E {{ Φ }}.
70
Proof.
71 72 73
  iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
  iNext; iIntros (v2 σ2 efs) "%".
74
  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
75 76
Qed.

77
Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 efs :
78
  ( σ1, head_reducible e1 σ1) 
79 80
  ( σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs') 
81 82 83
  (|={E,E'}=> WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
84

85
Lemma wp_lift_pure_det_head_step_no_fork {E E' Φ} e1 e2 :
86 87
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
88 89
  ( σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  [] = efs') 
90
  (|={E,E'}=> WP e2 @ E {{ Φ }})  WP e1 @ E {{ Φ }}.
91
Proof using Hinh.
92
  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
93
Qed.
94

95
Lemma wp_lift_pure_det_head_step_no_fork' {E Φ} e1 e2 :
96 97 98 99
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
  ( σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  [] = efs') 
100
   WP e2 @ E {{ Φ }}  WP e1 @ E {{ Φ }}.
101
Proof using Hinh.
102
  intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
103 104
  rewrite -step_fupd_intro //.
Qed.
105
End wp.