ectx_lifting.v 2.6 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
23
      e2 σ2 efs,  head_step e1 σ1 e2 σ2 efs  ownP σ2
          ={,E}= WP e2 @ E {{ Φ }}  wp_fork efs)
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
36
  ( σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
  (  e2 efs σ,  head_step e1 σ e2 σ efs  WP e2 @ E {{ Φ }}  wp_fork efs)
37
38
   WP e1 @ E {{ Φ }}.
Proof.
39
40
  iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
  iIntros (????). iApply "H". eauto.
41
Qed.
42

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

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

62
Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
63
64
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
65
66
  ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
   (WP e2 @ E {{ Φ }}  wp_fork efs)  WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Proof. eauto using wp_lift_pure_det_step. Qed.
68
End wp.