Commit 3c064dd6 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'swasey/invariance' into 'master'

Make it possible to apply the observational view shift lemmas.

See merge request !40
parents ab23831f 471b2121
...@@ -187,11 +187,11 @@ Proof. ...@@ -187,11 +187,11 @@ Proof.
iFrame. by iApply big_sepL_nil. iFrame. by iApply big_sepL_nil.
Qed. Qed.
Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ Φ : Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
( `{Hinv : invG Σ}, ( `{Hinv : invG Σ},
True ={}= stateI : state Λ iProp Σ, True ={}= stateI : state Λ iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
stateI σ1 WP e {{ Φ }} (stateI σ2 ={,}= ⌜φ⌝)) stateI σ1 WP e {{ _, True }} (stateI σ2 ={,}= ⌜φ⌝))
rtc step ([e], σ1) (t2, σ2) rtc step ([e], σ1) (t2, σ2)
φ. φ.
Proof. Proof.
......
...@@ -50,13 +50,13 @@ Proof. ...@@ -50,13 +50,13 @@ Proof.
iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP. iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
Qed. Qed.
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ Φ : Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ :
( `{ownPG Λ Σ}, ( `{ownPG Λ Σ},
ownP σ1 ={}= WP e {{ Φ }} |={,}=> σ', ownP σ' ⌜φ σ'⌝) ownP σ1 ={}= WP e {{ _, True }} |={,}=> σ', ownP σ' ⌜φ σ'⌝)
rtc step ([e], σ1) (t2, σ2) rtc step ([e], σ1) (t2, σ2)
φ σ2. φ σ2.
Proof. Proof.
intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _ Φ)=> //. intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _)=> //.
iIntros (?) "". iMod (own_alloc ( (Excl' (σ1 : leibnizC _)) (Excl' σ1))) iIntros (?) "". iMod (own_alloc ( (Excl' (σ1 : leibnizC _)) (Excl' σ1)))
as (γσ) "[Hσ Hσf]"; first done. as (γσ) "[Hσ Hσf]"; first done.
iExists (λ σ, own γσ ( (Excl' (σ:leibnizC _)))). iFrame "Hσ". iExists (λ σ, own γσ ( (Excl' (σ:leibnizC _)))). iFrame "Hσ".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment