total_ectx_lifting.v 3.65 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12
(** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language.
From iris.program_logic Require Export total_weakestpre total_lifting.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

Section wp.
Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
13
Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step head_reducible_no_obs_reducible.
14 15 16

Lemma twp_lift_head_step {s E Φ} e1 :
  to_val e1 = None 
17
  ( σ1 κs, state_interp σ1 κs ={E,}=
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
18 19 20 21
    head_reducible_no_obs e1 σ1 
     κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,E}=
      ⌜κ = None  state_interp σ2 κs 
      WP e2 @ s; E [{ Φ }]  [ list] ef  efs, WP ef @ s;  [{ _, True }])
22 23
   WP e1 @ s; E [{ Φ }].
Proof.
24
  iIntros (?) "H". iApply (twp_lift_step _ E)=>//. iIntros (σ1 κs) "Hσ".
25
  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
26
  iSplit; [destruct s; auto|]. iIntros (κ e2 σ2 efs Hstep).
27 28 29 30
  iApply "H". by eauto.
Qed.

Lemma twp_lift_pure_head_step {s E Φ} e1 :
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
31
  ( σ1, head_reducible_no_obs e1 σ1) 
32
  ( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs  κ = None  σ1 = σ2) 
33
  (|={E}=>  κ e2 efs σ, head_step e1 σ κ e2 σ efs 
34 35 36 37
    WP e2 @ s; E [{ Φ }]  [ list] ef  efs, WP ef @ s;  [{ _, True }])
   WP e1 @ s; E [{ Φ }].
Proof using Hinh.
  iIntros (??) ">H". iApply twp_lift_pure_step; eauto.
38
  iIntros "!>" (?????). iApply "H"; eauto.
39 40 41 42
Qed.

Lemma twp_lift_atomic_head_step {s E Φ} e1 :
  to_val e1 = None 
43
  ( σ1 κs, state_interp σ1 κs ={E}=
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
44 45 46
    head_reducible_no_obs e1 σ1 
     κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E}=
      ⌜κ = None  state_interp σ2 κs 
Ralf Jung's avatar
Ralf Jung committed
47
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  [{ _, True }])
48 49 50
   WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
51
  iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
52
  iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs Hstep). iApply "H"; eauto.
53 54 55 56
Qed.

Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
  to_val e1 = None 
57
  ( σ1 κs, state_interp σ1 κs ={E}=
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
58 59 60
    head_reducible_no_obs e1 σ1 
     κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E}=
      ⌜κ = None  efs = []  state_interp σ2 κs  from_option Φ False (to_val e2))
61 62 63
   WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
64
  iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
65 66
  iIntros (κ v2 σ2 efs Hstep).
  iMod ("H" with "[# //]") as "($ & % & $ & $)"; subst; auto.
67 68 69
Qed.

Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
70
  ( σ1, head_reducible_no_obs e1 σ1) 
71
  ( σ1 κ e2' σ2 efs',
72
    head_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  efs = efs') 
73 74
  (|={E}=> WP e2 @ s; E [{ Φ }]  [ list] ef  efs, WP ef @ s;  [{ _, True }])
   WP e1 @ s; E [{ Φ }].
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
75
Proof using Hinh. eauto 10 using twp_lift_pure_det_step. Qed.
76 77 78

Lemma twp_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
  to_val e1 = None 
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
79
  ( σ1, head_reducible_no_obs e1 σ1) 
80
  ( σ1 κ e2' σ2 efs',
81
    head_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  [] = efs') 
82 83 84 85 86
  WP e2 @ s; E [{ Φ }]  WP e1 @ s; E [{ Φ }].
Proof using Hinh.
  intros. rewrite -(twp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
Qed.
End wp.