ectx_lifting.v 3.41 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
5

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

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

18
19
Lemma wp_lift_head_step E Φ e1 :
  (|={E,}=>  σ1,  head_reducible e1 σ1   ownP σ1 
20
      e2 σ2 efs,  head_step e1 σ1 e2 σ2 efs  ownP σ2
21
          ={,E}= WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
22
   WP e1 @ E {{ Φ }}.
23
Proof.
24
  iIntros "H". iApply (wp_lift_step E); try done.
25
  iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
26
  iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "[% ?]".
27
  iApply "Hwp". by eauto.
28
Qed.
29

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

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

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

63
64
65
66
67
68
69
70
71
72
73
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.

74
Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
75
  ( σ1, head_reducible e1 σ1) 
76
77
78
  ( σ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
79
Proof. eauto using wp_lift_pure_det_step. Qed.
80
81
82
83
84
85
86
87
88

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.
89
End wp.