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.
Ralf Jung's avatar
Ralf Jung committed
41
  iMod "H". iModIntro. iNext. iMod "H". iModIntro.
42
  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 70 71
  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) "%".
  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.