Commit 471b2121 authored by David Swasey's avatar David Swasey Committed by Ralf Jung

Make it possible to apply the observational view shift lemmas.

parent ab23831f
......@@ -187,11 +187,11 @@ Proof.
iFrame. by iApply big_sepL_nil.
Qed.
Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ Φ :
Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
( `{Hinv : invG Σ},
True ={}= stateI : state Λ iProp Σ,
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)
φ.
Proof.
......
......@@ -50,13 +50,13 @@ Proof.
iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
Qed.
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ Φ :
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ :
( `{ownPG Λ Σ},
ownP σ1 ={}= WP e {{ Φ }} |={,}=> σ', ownP σ' ⌜φ σ')
ownP σ1 ={}= WP e {{ _, True }} |={,}=> σ', ownP σ' ⌜φ σ')
rtc step ([e], σ1) (t2, σ2)
φ σ2.
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)))
as (γσ) "[Hσ Hσf]"; first done.
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