Skip to content
Snippets Groups Projects
Commit baa59834 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Simplify its proof.

parent 4605684c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 7 deletions
perm_incl.v
+ 2
− 7
View file @ baa59834
...@@ -230,15 +230,10 @@ Section props. ...@@ -230,15 +230,10 @@ Section props.
iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'. iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
iVs (lft_borrow_create with "Hκ Hown") as "[Hbor Hextract]". done. iVs (lft_borrow_create with "Hκ Hown") as "[Hbor Hextract]". done.
iSplitL "Hbor". by simpl; eauto. iSplitL "Hbor". by simpl; eauto.
assert ((Some #l ◁ own q ty)%P tid ⊣⊢
▷ †{q}l…ty_size ty ★ ▷ l ↦★: ty_own ty tid) as ->.
{ iSplit; iIntros "H/=".
- iDestruct "H" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
by iFrame.
- iExists _. eauto. }
iVs (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done. iVs (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
iVs (lft_extract_combine with "[-]"). done. by iFrame. iVs (lft_extract_combine with "[-]"). done. by iFrame.
iVsIntro. iApply lft_extract_mono; last done. by iDestruct 1 as "[$$]". iVsIntro. iApply lft_extract_mono; last done.
iIntros "H/=". iExists _. iSplit. done. by iDestruct "H" as "[$$]".
Qed. Qed.
Lemma reborrow_uniq_borrowing κ κ' v ty : Lemma reborrow_uniq_borrowing κ κ' v ty :
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment