Skip to content
Snippets Groups Projects
Commit 97b304a0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak a proof.

parent 00d7fbc1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/fancy_updates.v
+ 4
− 5
View file @ 97b304a0
...@@ -63,11 +63,10 @@ Lemma step_fupdN_soundness `{invPreG Σ} φ n : ...@@ -63,11 +63,10 @@ Lemma step_fupdN_soundness `{invPreG Σ} φ n :
(∀ `{Hinv: invG Σ}, (|={⊤, ∅}▷=>^n |={⊤, ∅}=> ⌜ φ ⌝ : iProp Σ)%I) → (∀ `{Hinv: invG Σ}, (|={⊤, ∅}▷=>^n |={⊤, ∅}=> ⌜ φ ⌝ : iProp Σ)%I) →
φ. φ.
Proof. Proof.
iIntros (Hiter). intros Hiter.
eapply (soundness (M:=iResUR Σ) _ (S (S n))). apply (soundness (M:=iResUR Σ) _ (S (S n))); simpl.
eapply (fupd_plain_soundness ⊤); first by apply _. apply (fupd_plain_soundness ⊤ _).
intros Hinv. rewrite -/sbi_laterN. intros Hinv. iPoseProof (Hiter Hinv) as "H".
iPoseProof (Hiter Hinv) as "H".
destruct n as [|n]. destruct n as [|n].
- rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'". - rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'".
do 2 iMod "H'"; iModIntro; auto. do 2 iMod "H'"; iModIntro; auto.
......
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