ectx_lifting.v 6.7 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.
7
Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
8
Implicit Types s : stuckness.
9
Implicit Types P : iProp Σ.
10 11 12
Implicit Types Φ : val Λ  iProp Σ.
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
Hint Resolve (reducible_not_val _ inhabitant).
15
Hint Resolve head_stuck_stuck.
16

17
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
18
  to_val e1 = None 
19
  ( σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,}=
20
    head_reducible e1 σ1 
21 22
     e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,,E}=
      state_interp σ2 κs  WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
23
   WP e1 @ s; E {{ Φ }}.
24
Proof.
25
  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs) "Hσ".
26
  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
27
  iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs Hstep).
28
  iApply "H"; eauto.
29 30
Qed.

31 32
Lemma wp_lift_head_step {s E Φ} e1 :
  to_val e1 = None 
33
  ( σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,}=
34
    head_reducible e1 σ1 
35 36
      e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,E}=
      state_interp σ2 κs  WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
37 38
   WP e1 @ s; E {{ Φ }}.
Proof.
39 40
  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (???) "?".
  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
41 42
Qed.

43 44
Lemma wp_lift_head_stuck E Φ e :
  to_val e = None 
45
  sub_redexes_are_values e 
46
  ( σ κs, state_interp σ κs ={E,}= head_stuck e σ⌝)
47 48
   WP e @ E ?{{ Φ }}.
Proof.
49
  iIntros (??) "H". iApply wp_lift_stuck; first done.
50
  iIntros (σ κs) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
51 52 53
Qed.

Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
54
  ( σ1, head_reducible e1 σ1) 
55
  ( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs  κ = None  σ1 = σ2) 
56
  (|={E,E'}=>  κ e2 efs σ, head_step e1 σ κ e2 σ efs 
57 58
    WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
59
Proof using Hinh.
60
  iIntros (??) "H". iApply wp_lift_pure_step; [|by eauto|].
61
  { by destruct s; auto. }
62
  iApply (step_fupd_wand with "H"); iIntros "H".
63
  iIntros (?????). iApply "H"; eauto.
64
Qed.
65

66 67
Lemma wp_lift_pure_head_stuck E Φ e :
  to_val e = None 
68 69
  sub_redexes_are_values e 
  ( σ, head_stuck e σ) 
70 71
  WP e @ E ?{{ Φ }}%I.
Proof using Hinh.
72
  iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
73
  iIntros (σ κs) "_". iMod (fupd_intro_mask' E ) as "_"; first set_solver.
74
  by auto.
75 76
Qed.

77 78
Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
  to_val e1 = None 
79
  ( σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=
80
    head_reducible e1 σ1 
81 82
     e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E1,E2}=
      state_interp σ2 κs 
83 84 85 86
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E1 {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
87 88
  iIntros (σ1 κ κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by destruct s; auto. iIntros (e2 σ2 efs Hstep).
89
  iApply "H"; eauto.
90 91
Qed.

92
Lemma wp_lift_atomic_head_step {s E Φ} e1 :
93
  to_val e1 = None 
94
  ( σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=
95
    head_reducible e1 σ1 
96 97
      e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E}=
      state_interp σ2 κs 
Ralf Jung's avatar
Ralf Jung committed
98
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
99
   WP e1 @ s; E {{ Φ }}.
100 101
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
102 103
  iIntros (σ1 κ κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs Hstep).
104
  iApply "H"; eauto.
105 106
Qed.

107
Lemma wp_lift_atomic__head_step_no_fork_fupd {s E1 E2 Φ} e1 :
108
  to_val e1 = None 
109
  ( σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=
110
    head_reducible e1 σ1 
111 112
     e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E1,E2}=
      efs = []  state_interp σ2 κs  from_option Φ False (to_val e2))
113 114 115
   WP e1 @ s; E1 {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
116 117 118
  iIntros (σ1 κ κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
  iIntros (v2 σ2 efs Hstep).
  iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
119 120 121
  iIntros "!> !>". iMod "H" as "(% & $ & $)"; subst; auto.
Qed.

122
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
123
  to_val e1 = None 
124
  ( σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=
125
    head_reducible e1 σ1 
126 127
      e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E}=
      efs = []  state_interp σ2 κs  from_option Φ False (to_val e2))
128
   WP e1 @ s; E {{ Φ }}.
129
Proof.
130
  iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
131 132 133
  iIntros (σ1 κ κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
  iNext; iIntros (v2 σ2 efs Hstep).
  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)". subst; auto.
134 135
Qed.

136
Lemma wp_lift_pure_det_head_step {s E E' Φ} e1 e2 efs :
137
  ( σ1, head_reducible e1 σ1) 
138
  ( σ1 κ e2' σ2 efs',
139
    head_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  efs = efs') 
140 141 142 143 144 145
  (|={E,E'}=> WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
  intros. rewrite -(wp_lift_pure_det_step e1 e2 efs); eauto.
  destruct s; by auto.
Qed.
146

147
Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
148 149
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
150
  ( σ1 κ e2' σ2 efs',
151
    head_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  [] = efs') 
152
  (|={E,E'}=> WP e2 @ s; E {{ Φ }})  WP e1 @ s; E {{ Φ }}.
153
Proof using Hinh.
154
  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
155
  destruct s; by auto.
156
Qed.
157

158
Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
159 160
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
161
  ( σ1 κ e2' σ2 efs',
162
    head_step e1 σ1 κ e2' σ2 efs'  κ = None   σ1 = σ2  e2 = e2'  [] = efs') 
163
   WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
164
Proof using Hinh.
165
  intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
166 167
  rewrite -step_fupd_intro //.
Qed.
168
End wp.