ectx_lifting.v 4.61 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 {s E Φ} e1 :
18 19 20 21
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E,}=
    head_reducible e1 σ1 
      e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={,E}=
22 23
      state_interp σ2  WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
24
Proof.
25 26 27 28
  iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
  iSplit; first by destruct s; eauto. iNext. iIntros (e2 σ2 efs) "%".
  iApply "H"; eauto.
29 30
Qed.

31 32
Lemma wp_lift_head_stuck E Φ e :
  to_val e = None 
33 34
  sub_redexes_are_values e 
  ( σ, state_interp σ ={E,}= head_stuck e σ⌝)
35 36
   WP e @ E ?{{ Φ }}.
Proof.
37 38
  iIntros (??) "H". iApply wp_lift_stuck; first done.
  iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
39 40 41
Qed.

Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
42
  ( σ1, head_reducible e1 σ1) 
43
  ( σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
44
  (|={E,E'}=>  e2 efs σ, head_step e1 σ e2 σ efs 
45 46
    WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
47
Proof using Hinh.
48
  iIntros (??) "H". iApply wp_lift_pure_step; eauto.
49
  { by destruct s; auto. }
50 51
  iApply (step_fupd_wand with "H"); iIntros "H".
  iIntros (????). iApply "H"; eauto.
52
Qed.
53

54 55
Lemma wp_lift_pure_head_stuck E Φ e :
  to_val e = None 
56 57
  sub_redexes_are_values e 
  ( σ, head_stuck e σ) 
58 59
  WP e @ E ?{{ Φ }}%I.
Proof using Hinh.
60
  iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
61
  iIntros (σ) "_". iMod (fupd_intro_mask' E ) as "_"; first set_solver.
62
  by auto.
63 64 65
Qed.

Lemma wp_lift_atomic_head_step {s E Φ} e1 :
66 67 68 69 70
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E}=
    head_reducible e1 σ1 
      e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}=
      state_interp σ2 
71 72
      default False (to_val e2) Φ  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
73 74
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
75 76 77
  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs) "%".
  iApply "H"; auto.
78 79
Qed.

80
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
81 82 83 84 85
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E}=
    head_reducible e1 σ1 
      e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E}=
      efs = []  state_interp σ2  default False (to_val e2) Φ)
86
   WP e1 @ s; E {{ Φ }}.
87
Proof.
88 89 90
  iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
  iNext; iIntros (v2 σ2 efs) "%".
91
  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
92 93
Qed.

94
Lemma wp_lift_pure_det_head_step {s E E' Φ} e1 e2 efs :
95
  ( σ1, head_reducible e1 σ1) 
96 97
  ( σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs') 
98 99 100 101 102 103
  (|={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.
104

105
Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
106 107
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
108 109
  ( σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  [] = efs') 
110
  (|={E,E'}=> WP e2 @ s; E {{ Φ }})  WP e1 @ s; E {{ Φ }}.
111
Proof using Hinh.
112
  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
113
  destruct s; by auto.
114
Qed.
115

116
Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
117 118 119 120
  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') 
121
   WP e2 @ E {{ Φ }}  WP e1 @ E {{ Φ }}.
122
Proof using Hinh.
123
  intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
124 125
  rewrite -step_fupd_intro //.
Qed.
126
End wp.