ectx_lifting.v 3.95 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
Lemma wp_ectx_bind {E Φ} K e :
16
  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
Lemma wp_lift_head_step {E Φ} e1 :
20 21 22 23 24
  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  WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
25
   WP e1 @ E {{ Φ }}.
26
Proof.
27 28 29 30
  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.
31
Qed.
32

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

45 46 47 48 49 50 51
Lemma wp_lift_atomic_head_step {E Φ} e1 :
  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 
      default False (to_val e2) Φ  [ list] ef  efs, WP ef {{ _, True }})
52
   WP e1 @ E {{ Φ }}.
53
Proof.
54 55 56
  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
  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.
57
Qed.
58

59 60 61 62 63 64
Lemma wp_lift_atomic_head_step_no_fork {E Φ} e1 :
  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) Φ)
65 66
   WP e1 @ E {{ Φ }}.
Proof.
67 68 69
  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) "%".
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst.
  by iApply big_sepL_nil.
72 73
Qed.

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

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

Lemma wp_lift_pure_det_head_step_no_fork' {E Φ} e1 e2 :
  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') 
   WP e2 @ E {{ Φ }}  WP e1 @ E {{ Φ }}.
Proof using Hinh.
  intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
  rewrite -step_fupd_intro //.
Qed.
102
End wp.