ectx_lifting.v 2.74 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
8
Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
Context {Σ : iFunctor}.
9
10
Implicit Types P : iProp (ectx_lang expr) Σ.
Implicit Types Φ : val  iProp (ectx_lang expr) Σ.
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
16
17

Notation wp_fork ef := (default True ef (flip (wp ) (λ _, True)))%I.

Lemma wp_ectx_bind {E e} K Φ :
18
  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
19
20
Proof. apply: weakestpre.wp_bind. Qed.

21
Lemma wp_lift_head_step E1 E2 Φ e1 :
22
  E2  E1  to_val e1 = None 
23
24
25
  (|={E1,E2}=>  σ1,  head_reducible e1 σ1 
        ownP σ1    e2 σ2 ef, ( head_step e1 σ1 e2 σ2 ef  ownP σ2)
                                 ={E2,E1}= WP e2 @ E1 {{ Φ }}  wp_fork ef)
26
   WP e1 @ E1 {{ Φ }}.
27
Proof.
28
29
30
31
  iIntros {??} "H". iApply (wp_lift_step E1 E2); try done.
  iPvs "H" as {σ1} "(%&Hσ1&Hwp)". set_solver. iPvsIntro. iExists σ1.
  iSplit; first by eauto. iFrame. iNext. iIntros {e2 σ2 ef} "[% ?]".
  iApply "Hwp". by eauto.
32
Qed.
33

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

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

Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
  atomic e1 
  head_reducible e1 σ1 
  ( e2' σ2' ef', head_step e1 σ1 e2' σ2' ef' 
    σ2 = σ2'  to_val e2' = Some v2  ef = ef') 
61
   ownP σ1   (ownP σ2 - (|={E}=> Φ v2)  wp_fork ef)  WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Proof. eauto using wp_lift_atomic_det_step. Qed.
63
64
65
66
67
68

Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 ef :
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
  ( σ1 e2' σ2 ef', head_step e1 σ1 e2' σ2 ef'  σ1 = σ2  e2 = e2'  ef = ef')
   (WP e2 @ E {{ Φ }}  wp_fork ef)  WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Proof. eauto using wp_lift_pure_det_step. Qed.
70
End wp.