Commit c8379abc authored by Ralf Jung's avatar Ralf Jung

fupd_plain_soundness works for all masks

parent 5f53a267
...@@ -59,11 +59,12 @@ Proof. ...@@ -59,11 +59,12 @@ Proof.
by iFrame. by iFrame.
Qed. Qed.
Lemma fupd_plain_soundness `{!invPreG Σ} E (P: iProp Σ) `{!Plain P}: Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
( `{Hinv: !invG Σ}, (|={,E}=> P)%I) ( P)%I. ( `{Hinv: !invG Σ}, (|={E1,E2}=> P)%I) ( P)%I.
Proof. Proof.
iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]". iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
iPoseProof (Hfupd Hinv) as "H". iAssert (|={,E2}=> P)%I as "H".
{ iMod fupd_intro_mask'; last iApply Hfupd. done. }
rewrite uPred_fupd_eq /uPred_fupd_def. rewrite uPred_fupd_eq /uPred_fupd_def.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame. iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed. Qed.
...@@ -74,7 +75,7 @@ Lemma step_fupdN_soundness `{!invPreG Σ} φ n : ...@@ -74,7 +75,7 @@ Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
Proof. Proof.
intros Hiter. intros Hiter.
apply (soundness (M:=iResUR Σ) _ (S (S n))); simpl. apply (soundness (M:=iResUR Σ) _ (S (S n))); simpl.
apply (fupd_plain_soundness _)=> Hinv. apply (fupd_plain_soundness _)=> Hinv.
iPoseProof (Hiter Hinv) as "H". clear Hiter. iPoseProof (Hiter Hinv) as "H". clear Hiter.
destruct n as [|n]. destruct n as [|n].
- iApply fupd_plainly_mask_empty. iMod "H" as %?; auto. - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
......
...@@ -124,7 +124,7 @@ Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ : ...@@ -124,7 +124,7 @@ Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *) sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
Proof. Proof.
intros Hwp. apply (soundness (M:=iResUR Σ) _ 2); simpl. intros Hwp. apply (soundness (M:=iResUR Σ) _ 2); simpl.
apply (fupd_plain_soundness _)=> Hinv. apply (fupd_plain_soundness _)=> Hinv.
iMod (Hwp) as (stateI fork_post) "[Hσ H]". iMod (Hwp) as (stateI fork_post) "[Hσ H]".
iApply (@twptp_total _ _ (IrisG _ _ Hinv stateI fork_post) with "Hσ"). iApply (@twptp_total _ _ (IrisG _ _ Hinv stateI fork_post) with "Hσ").
by iApply (@twp_twptp _ _ (IrisG _ _ Hinv stateI fork_post)). by iApply (@twp_twptp _ _ (IrisG _ _ Hinv stateI fork_post)).
......
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