Commit 875e7747 authored by Ralf Jung's avatar Ralf Jung

proof style nits

parent c6d98043
Pipeline #28213 passed with stage
in 33 minutes and 29 seconds
......@@ -98,7 +98,7 @@ Proof.
as %[EQB2%to_borUR_included _]%auth_both_valid.
iAssert j1 j2%I with "[#]" as %Hj1j2.
{ iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
iPureIntro. iIntros (->). (* FIXME this used to work without iPureIntro. *)
iIntros (->).
exfalso. revert Hj1j2. rewrite /= singleton_op singleton_valid.
by intros [[]]. }
iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
......
......@@ -184,13 +184,13 @@ Section borrow.
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']"; first solve_ndisj.
iApply (wp_step_fupd _ _ (__) with "[Hown Htok2]"); try done.
- iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
- iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose''" with "Htok2") as "Htok2".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
rewrite tctx_interp_singleton tctx_hasty_val' //.
by iApply (ty_shr_mono with "Hincl' Hshr").
{ iApply ("Hown" with "[%] Htok2"); first solve_ndisj. }
iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
iMod ("Hclose''" with "Htok2") as "Htok2".
iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
rewrite tctx_interp_singleton tctx_hasty_val' //.
by iApply (ty_shr_mono with "Hincl' Hshr").
Qed.
Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :
......
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