ectx_lifting.v 3.52 KB
Newer Older
1
(** Some derived lemmas for ectx-based languages *)
2 3
From iris.program_logic Require Export ectx_language weakestpre lifting.
From iris.program_logic Require Import ownership.
4
From iris.proofmode Require Import weakestpre.
5 6

Section wp.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
8 9 10
Context `{irisG (ectx_lang expr) Σ}.
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 e} K Φ :
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 20 21
Lemma wp_lift_head_step E Φ e1 :
  to_val e1 = None 
  (|={E,}=>  σ1,  head_reducible e1 σ1   ownP σ1 
22
      e2 σ2 efs,  head_step e1 σ1 e2 σ2 efs  ownP σ2
23
          ={,E}= WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
24
   WP e1 @ E {{ Φ }}.
25
Proof.
26 27
  iIntros (?) "H". iApply (wp_lift_step E); try done.
  iVs "H" as (σ1) "(%&Hσ1&Hwp)". iVsIntro. iExists σ1.
28
  iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "[% ?]".
29
  iApply "Hwp". by eauto.
30
Qed.
31

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

44
Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
45 46
  atomic e1 
  head_reducible e1 σ1 
47
   ownP σ1   ( v2 σ2 efs,
48 49
   head_step e1 σ1 (of_val v2) σ2 efs  ownP σ2 -
    (|={E}=> Φ v2)  [ list] ef  efs, WP ef {{ _, True }})
50
   WP e1 @ E {{ Φ }}.
51
Proof.
52 53
  iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
  iIntros (???) "[% ?]". iApply "H". eauto.
54
Qed.
55

56
Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
57 58
  atomic e1 
  head_reducible e1 σ1 
59 60
  ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' 
    σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
61 62 63
   ownP σ1   (ownP σ2 -
    (|={E}=> Φ v2)  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Proof. eauto using wp_lift_atomic_det_step. Qed.
65

66 67 68 69 70 71 72 73 74 75 76
Lemma wp_lift_atomic_det_head_step' {E Φ e1} σ1 v2 σ2 :
  atomic e1 
  head_reducible e1 σ1 
  ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' 
    σ2 = σ2'  to_val e2' = Some v2  [] = efs') 
   ownP σ1   (ownP σ2 ={E}= Φ v2)  WP e1 @ E {{ Φ }}.
Proof.
  intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 [])
    ?big_sepL_nil ?right_id; eauto.
Qed.

77
Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
78 79
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
80 81 82
  ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs') 
   (WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Proof. eauto using wp_lift_pure_det_step. Qed.
84 85 86 87 88 89 90 91 92

Lemma wp_lift_pure_det_head_step' {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.
  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
Qed.
93
End wp.