ectx_lifting.v 4.74 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 15
Hint Resolve (reducible_not_val _ inhabitant).
Hint Resolve progressive_head_progressive.
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 33 34 35 36 37 38 39 40
Lemma wp_lift_head_stuck E Φ e :
  to_val e = None 
  ( σ, state_interp σ ={E,}= ¬ head_progressive e σ⌝)
   WP e @ E ?{{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_stuck; first done.
  iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto. 
Qed.

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

53 54 55 56 57 58 59 60 61 62 63 64
Lemma wp_lift_pure_head_stuck E Φ e :
  to_val e = None 
  ( K e1 σ1 e2 σ2 efs, e = fill K e1  ¬ head_step e1 σ1 e2 σ2 efs) 
  WP e @ E ?{{ Φ }}%I.
Proof using Hinh.
  iIntros (Hnv Hnstep). iApply wp_lift_head_stuck; first done.
  iIntros (σ) "_". iMod (fupd_intro_mask' E ) as "_"; first set_solver.
  iModIntro. iPureIntro. case; first by rewrite Hnv; case.
  move=>[] K [] e1 [] Hfill [] e2 [] σ2 [] efs /= Hstep. exact: Hnstep.
Qed.

Lemma wp_lift_atomic_head_step {s E Φ} e1 :
65 66 67 68 69
  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 
70 71
      default False (to_val e2) Φ  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
72 73
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
74 75 76
  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.
77 78
Qed.

79
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
80 81 82 83 84
  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) Φ)
85
   WP e1 @ s; E {{ Φ }}.
86
Proof.
87 88 89
  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) "%".
90
  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
91 92
Qed.

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

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

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