diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index c8fb1519ecbfe401bc474a51dafd013155736920..08ebdf3d373e88830b7dadebccfb043f5d36ee3a 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -1338,11 +1338,12 @@ Section arc.
as "[tok1 tok2]"; first by rewrite Qp.div_2.
iModIntro. iSplitR "WA W' tok1 R1 WU1 HP2 tokM SW SM SD".
+ rewrite /Q Pos2Z.id /WeakTok. iFrame "SDA Wt".
- iExists _. iFrame "Wt' tok2 R2 WU2".
- + iExists (None, Some $ Cinl ((q' + q'' / 2)%Qp, (n + 1)%positive)).
- iSplitL ""; [done|]. iFrame "WA W' HP2 tokM SW SM".
- iSplitR "SD"; [|by iExists _].
- iExists (q''/2)%Qp, Ut'. iFrame "tok1 R1 WU1 SeenU".
+ iFrame "Wt' tok2 R2 WU2".
+ + iIntros "!>".
+ iExists (None, Some $ Cinl ((q' + q'' / 2)%Qp, (n + 1)%positive)).
+ iSplitL ""; [done|]. iFrame "WA W' HP2 SW SM".
+ iSplitR "SD tokM"; [|iFrame].
+ iExists (q'' / 2)%Qp, Ut'. iFrame "tok1 R1 WU1 SeenU".
iPureIntro. by rewrite -Qp.add_assoc Qp.div_2. }
(* finally done with the CAS *)
@@ -1704,16 +1705,15 @@ Section arc.
{ iExists (None,None). by iFrame "WA". }
iSplitL "SDA"; [by iExists _|]. simpl. rewrite Eq''.
iDestruct (GPS_SWSharedReader_Reader with "R'") as "#RR".
- iFrame "W' R' HP tokS SW SM".
- iSplitL "tok'". { iExists _. by iFrame "tok'". }
- iSplitR "SD"; [iExists _; iFrame "WU SeenU'"|]. by iExists _.
+ iFrame "W' R' HP SW SM".
+ iSplitL "tok'"; by iFrame.
+ iSplitL "SDA". { rewrite /Q Pos2Z.id decide_False; [|done].
iSplitR ""; [by iExists _|done]. }
rewrite decide_False; last first. { by destruct n; try lia. }
iDestruct "WA" as (q2 Eq2) "WA".
iExists (None, Some $ Cinl (q2, Pos.pred n)). iSplitL "".
{ iPureIntro. f_equal. by rewrite Z.sub_1_r -Pos2Z.inj_pred. }
- iFrame "WA W' HP tokS SW SM". subst q'. iSplitR "SD"; [|by iExists _].
+ iFrame "WA W' HP SW SM". subst q'. iSplitR "SD tokS"; [|by iFrame].
iExists (q + q'')%Qp, _.
iCombine "tok" "tok'" as "tok". rewrite -Qp.div_add_distr.
iFrame "R' tok WU SeenU'". by rewrite assoc_L (comm_L _ q2). }
@@ -1912,9 +1912,9 @@ Section arc.
iDestruct "WR'" as "(tok'' & R'' & WR')".
iDestruct (GPS_SWSharedWriter_Reader_update with "W' R''") as "[W' R'']".
rewrite decide_False; last by (simpl; lia).
- iFrame "WA W' HP2 tok SW".
+ iFrame "WA W' HP2 SW".
iSplitL "tok'' R'' WR'". { iExists q'',_. iFrame (Eq'') "tok'' R'' WR'". }
- iSplitL "SM"; by iExists _.
+ iFrame.
- (* no weak arcs left, take out everything *)
simpl. iDestruct "WI" as "(Eqs & $ & WI)". iDestruct "Eqs" as %?. subst qs.
iModIntro. iExists (). iSplitL""; [done|]. iIntros (t'' Lt'') "W'".
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 2653421e3727610321c797bb71dfddf8b8c9f874..45e7db0cfc43eb75e9f7a97e186316e5d555a722 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -27,7 +27,7 @@ Proof.
{ apply auth_update. eapply singleton_local_update.
- by rewrite lookup_fmap EQB.
- by apply (exclusive_local_update _ (Excl (Bor_open q Vtok V'))). }
- iExists V'. rewrite -fmap_insert. iFrame "∗%". iExists _. iFrame.
+ iExists V'. rewrite -fmap_insert. iFrame "∗%".
rewrite -insert_delete_insert big_sepM_insert ?lookup_delete // big_sepM_delete //=.
iIntros "/= !>". iNext. iDestruct "HB" as "[?$]". iFrame.
Qed.
@@ -270,7 +270,7 @@ Proof.
iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iExists _. iFrame "%". iLeft. rewrite lft_inv_alive_unfold. iExists _, _. iFrame. }
- iExists κ''. iFrame "#". iModIntro. iIntros (Q) "HvsQ HQ". clear -HE HVV0.
+ iExists κ''. iFrame "Hle". iModIntro. iIntros (Q) "HvsQ HQ". clear -HE HVV0.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
rewrite big_sepS_later big_sepS_delete //.
@@ -302,7 +302,7 @@ Proof.
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iCombine "HV HQ HvsQ" as "HH".
iDestruct (monPred_in_intro with "HH") as (V') "(#HV' & % & HQ & HvsQ)".
- iMod (bor_close_internal with "Hs' [Hbox Hown HB] Hbor [HQ]")
+ iMod (bor_close_internal _ _ with "Hs' [Hbox Hown HB] Hbor [HQ]")
as "(Halive & Hbor & Htok)". { solve_ndisj. } { done. }
{ rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ (Bor_open q' V V0))
/lft_bor_alive. iExists _. iFrame "Hbox Hown".
@@ -322,7 +322,7 @@ Proof.
by iApply ame_lft_inv. }
iDestruct (monPred_in_elim with "HV' Htok") as "Htok".
iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
- iSplit; first by iApply lft_incl_refl. iExists j.
+ iSplit; first by iApply lft_incl_refl.
iDestruct (monPred_in_elim with "[] Hbor") as "$".
{ rewrite (_ : V' ⊔ V0 ⊑ V') //. solve_lat. }
iExists _. iFrame "Hs'". by rewrite -bi.iff_refl.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 6bb73e53428e9d465b7b3753d0c7cac63b5eb400..07f91861647025f26a98cdf7c63de922674c5663 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -23,7 +23,7 @@ Proof.
iMod (raw_bor_fake with "[Hdead]") as "[Hdead Hbor]"; [solve_ndisj|by iNext|].
iFrame. iMod ("Hclose" with "[-]"); [|done]. iExists _, _. iFrame.
rewrite big_sepS_later /lft_inv. iApply "Hclose'". iNext. iExists _.
- iFrame "%". iRight. rewrite /lft_inv_dead. iFrame "∗%". iExists _, _. by iFrame. }
+ iFrame "%". iRight. rewrite /lft_inv_dead. iFrame "∗%". }
rewrite {1}lft_inv_alive_unfold;
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
rewrite /lft_bor_alive; iDestruct "Halive" as (B) "[[HboxB >HownB] HB]".
@@ -46,7 +46,7 @@ Proof.
iExists (P' ∗ Pb)%I, (P' ∗ Pi)%I.
iFrame "Hinh".
rewrite -(bi.wand_entails _ _ (lft_vs_frame _ _ _ _)) /lft_bor_alive.
- iFrame. iExists _.
+ iFrame "Hvs". iExists _.
iFrame "HboxB HBâ—". rewrite big_sepM_insert /=; [|by destruct (B !! γB)].
iFrame. auto with lat. }
iMod ("Hclose" with "[HA HI Hclose']") as "_".
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 745794077cccb73174a28f29d5a23695880fbc33..bc1ac5b43a84abec97881eb94b808d4921988c84 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -147,7 +147,7 @@ Proof.
iMod (raw_bor_fake with "[Hdead]") as "[Hdead Hbor]"; [solve_ndisj|by iNext|].
iMod ("Hclose" with "[-Hbor]") as "_".
{ iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
- iExists _. iFrame "%". iRight. iFrame "%". iExists _, _. iNext. by iFrame. }
+ iFrame "%". iRight. iFrame "%". iNext. by iFrame. }
unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2"). }
rewrite ->lft_inv_alive_unfold. unfold lft_bor_alive.
iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
@@ -188,7 +188,7 @@ Proof.
by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
iMod ("Hclose" with "[-]"); [|done]. iExists A, I. iFrame. rewrite big_sepS_later.
iApply "Hclose'". iExists _. iSplit; [done|]. iLeft. iSplit; [|done].
- rewrite lft_inv_alive_unfold /lft_bor_alive. iExists Pb, Pi. iFrame. iExists _.
+ rewrite lft_inv_alive_unfold /lft_bor_alive. iExists Pb, Pi. iFrame "Hvs Hinh".
rewrite -!fmap_delete -!fmap_insert. iFrame "Hâ—".
rewrite !fmap_insert !fmap_delete /=. iFrame "Hbox".
rewrite !big_sepM_insert /=; last first.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 62b7420b92376499310bd90324f99b85f48f8531..ae335b908b530785fd2aeefffe2e65335e81b668 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -132,7 +132,7 @@ Proof.
{ by iNext. }
iFrame. iMod ("Hclose" with "[-]"); [|done]. iExists A', I'. iFrame. iNext.
iApply "Hclose'". rewrite /lft_inv /lft_inv_dead. iExists Vκ.
- iFrame "%". iRight. iFrame "∗%". iExists _, _. by iSplit.
+ iFrame "%". iRight. iFrame "∗%".
Qed.
Lemma bor_fake E κ P :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index e9f6bbd238bd6326668807a2a5df65dd980d9979..8801035c6188ceb4af22d8998aac7f8331f2f58d 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -425,7 +425,7 @@ Proof.
rewrite /bor /raw_bor /idx_bor /bor_idx /=. iSplit.
- iDestruct 1 as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
iExists (κ', s). by iFrame.
- - iDestruct 1 as ([κ' s]) "[[??]?]". iExists κ'. iFrame. iExists s. by iFrame.
+ - iDestruct 1 as ([κ' s]) "[[??]?]". iExists κ'. iFrame.
Qed.
Lemma idx_bor_shorten κ κ' i P : κ ⊑ κ' -∗ &{κ',i}P -∗ &{κ,i}P.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index ac1c65d02d4ad5c72a5eb442beea2bf14764b086..02b61e6208607512c5a14a7c940c7b74175fb045 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -166,8 +166,8 @@ Proof.
iMod (raw_bor_fake with "[Hbordead]") as "[Hbordead $]"; [solve_ndisj|by iNext|].
iMod ("Hclose" with "[-]"); [|done]. iExists _, _. iFrame.
rewrite (big_sepS_delete _ (dom _) κ') //. iFrame.
- rewrite /lft_inv /lft_inv_dead. iExists _. iFrame "%". iRight. iFrame "%".
- iExists _, _. iFrame "∗%". by iNext. }
+ rewrite /lft_inv /lft_inv_dead. iExists _. iFrame "%". iRight.
+ iFrame "∗%". by iNext. }
rewrite {1}/raw_bor. iDestruct "Hraw" as (i') "[Hbor H]".
iDestruct "H" as (P') "[#HP' #Hs']".
rewrite lft_inv_alive_unfold /lft_bor_alive.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 8cd1ecb56f26899cddcd6dc5eb3f17994ddf7457..2ae109f2994a3fa526bd8af45f5c709dd232a36c 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -434,11 +434,11 @@ Section arc.
iIntros "[Hrcbox↦2 Hx↦]". wp_seq. wp_write.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lrc â— box (arc ty)]
- with "[] LFT HE Hna HL Hk [>-]"); last first.
+ with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
- iSplitL "Hx↦"; first by iExists _; rewrite ->uninit_own; auto.
+ iSplitL ""; first done.
iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
- rewrite freeable_sz_full_S. iFrame. iExists _. by iFrame. }
+ rewrite freeable_sz_full_S. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -479,7 +479,7 @@ Section arc.
iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
with "Hrcbox↦0 Hrcbox↦1 [-]") as (γi γs γw γsw t q) "[Ha Htok]".
- { rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
+ { rewrite freeable_sz_full_S. iFrame.
by rewrite vec_to_list_length. }
iExists γi, γs, γw, γsw, ν, t, q. iFrame. iSplitL; first by auto.
iIntros "!>!>!> Hν". iDestruct (lft_tok_dead with "Hν H†") as "[]". }
@@ -896,8 +896,8 @@ Section arc.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx â— box (uninit 1); r â— box (option ty) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
- by rewrite tctx_hasty_val. }
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
+ rewrite tctx_hasty_val. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -932,8 +932,8 @@ Section arc.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx â— box (uninit 1); r â— box (uninit 0) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
- by rewrite tctx_hasty_val. }
+ { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
+ rewrite tctx_hasty_val. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -1001,7 +1001,7 @@ Section arc.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
iFrame. iCombine "Hr1" "Hr2" as "Hr1". iCombine "Hr0" "Hr1" as "Hr".
rewrite -[in _ +â‚— ty.(ty_size)]Hlen -heap_pointsto_vec_app
- -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
+ -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame.
iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
rewrite app_length drop_length. lia. }
iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 52971aaf3299543a5459b6286d7002a928b7e381..43378de2ace7ad5b23bc686e302d54cadfb4a193 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -204,10 +204,7 @@ Section typing.
iSplitR; first done.
simpl.
rewrite freeable_sz_full.
- iFrame.
- iExists 0%nat.
- iSplitL; last done.
- iExists γ; iSplitR; by eauto. }
+ by iFrame "#∗". }
iMod ("Hn'" with "[%]") as (α) "[Hn Htok]"; [solve_typing..|].
wp_let.
iMod (lctx_lft_alive_tok Ï with "HE HL")
@@ -405,11 +402,7 @@ Section typing.
iMod ("Hclose'" with "[H↦ Hidx Hown]") as "[Hn Hβ]".
{ iExists (#(n+1)::nil).
rewrite heap_pointsto_vec_singleton.
- iFrame "∗".
- iIntros "!>".
- iExists (n + 1)%nat.
- iSplitL; last by (iPureIntro; do 3 f_equal; lia).
- iExists γ. by iFrame.
+ iFrame "#∗". iPureIntro; do 3 f_equal; lia.
}
iMod ("Hclose" with "Hβ HL") as "HL".
iApply (type_type _ _ _ [ r â— box (uninit 1); #n â— brandidx _]
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 4bcf5adf008d9faff39a804f020a3172df3644b5..0cc58f097057b21bd8f0c399d3ef6de1b7e4f411 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -218,8 +218,8 @@ Section typing.
with "[] LFT HE Htl HL HC"); last first.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
- - iFrame. iExists _. iFrame. iNext. iApply uninit_own. done.
- - iFrame. iExists _. iFrame. }
+ - iFrame. iNext. iApply uninit_own. done.
+ - iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 7102dfbfc34901e798af801314673c517e828677..b6346ca3e5d0367ce783606007d71e1e03b2ef67 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -156,8 +156,8 @@ Section code.
with "[] LFT HE Hna HL Hk"); last first.
(* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
- iFrame. iSplitL "Hx".
- - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
+ iFrame. iSplitL "".
+ - by rewrite uninit_own vec_to_list_length.
- iExists (#false :: vl). rewrite heap_pointsto_vec_cons.
iFrame "∗ HINV". eauto. }
iApply type_delete; [solve_typing..|].
@@ -195,10 +195,9 @@ Section code.
with "[] LFT HE Hna HL Hk"); last first.
(* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
- iFrame. iSplitR "Hm0 Hm".
- - iExists _. iFrame.
- - iExists (_ :: _). rewrite heap_pointsto_vec_cons. iFrame.
- rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
+ iFrame.
+ iExists (_ :: _). rewrite heap_pointsto_vec_cons. iFrame.
+ rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index e9304df74d5e7c693e877e56fc87d1969d023aac..69b1c180133ebcc9c51fc97079b092c6c48d5880 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -178,7 +178,7 @@ Section code.
(* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
unlock. iFrame. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame "Hg".
- iExists _. iFrame "#∗". iExists _. iFrame "#". }
+ iExists _. iFrame "#∗". }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index eaf6cc423d8cf871b4713f4d9eec0ce69698b033..23c277657e809153466d2973441005e0248f000b 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -330,7 +330,7 @@ Section code.
iSplitL "Hty".
{ iDestruct "Hty" as (vy) "[H Hty]". iExists vy. iFrame.
by iApply "Hinclo". }
- iIntros "!> H". iApply ("Hclose" with "[>-]"). iFrame. iExists _.
+ iIntros "!> H". iApply ("Hclose" with "[>-]").
iFrame. rewrite Hincls /= !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
by iFrame.
* iIntros "Hl1".
@@ -383,7 +383,7 @@ Section code.
{ apply auth_update_dealloc.
rewrite pair_op Cinl_op Some_op -{1}(left_id 0%nat _ weak) pair_op.
apply (cancel_local_update_unit _ (_, _)). }
- iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
+ iApply "Hclose". iFrame "Hna Hst". iExists (q+q'')%Qp. iFrame.
iSplitL; first last.
{ rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
@@ -544,10 +544,9 @@ Section code.
iApply (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lrc â— box (rc ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
- iSplitL "Hx↦".
- { iExists _. rewrite uninit_own. auto. }
+ iSplitR; first done.
iNext. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
- rewrite freeable_sz_full_S. iFrame. iExists _. iFrame. }
+ rewrite freeable_sz_full_S. iFrame. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -1090,8 +1089,8 @@ Section code.
iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
iSplitR; first by iApply type_incl_refl.
iMod (ty_share with "LFT Hb Hν1") as "[Hty Hν]"=>//.
- iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _. do 2 iFrame.
- iExists _. iFrame. by rewrite Qp.div_2. }
+ iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _.
+ do 2 iFrame. by rewrite Qp.div_2. }
iDestruct "Hty" as (ty') "#(Hty'ty & Hinv & Hs & Hν†)".
iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
wp_bind (of_val clone). iApply (wp_wand with "[Hna]").
@@ -1132,7 +1131,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
!tctx_hasty_val' //. unlock. iFrame. iRight. iExists γ, ν, _.
- unfold rc_persist, tc_opaque. iFrame "∗#". eauto. }
+ unfold rc_persist, tc_opaque. iFrame "∗#". }
iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
iApply type_let. { apply rc_drop_type. } { solve_typing. } iIntros (drop). simpl_subst.
iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 35fbe7be394d1cbf1ac1c350a316459b07ef266e..8700a8580b00fdfbfd6b104a049df804c049934b 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -411,18 +411,16 @@ Section code.
destruct st as [[[q'' strong]| |]|]; try done.
- iExists _. iDestruct "Hrcst" as (q0) "(Hlw & >$ & Hrcst)". iRight.
iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
- iExists _. iFrame. iExists _. iFrame.
by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
- iExists _. iDestruct "Hrcst" as "[Hlw >$]". iRight.
iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
- iExists _. iFrame. simpl.
by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
- iExists _. iDestruct "Hrcst" as "(>Hlw & >$ & >H†& >H)". destruct weakc.
+ iLeft. iSplitR; first done. iMod ("Hclose" with "[$Hna Hrcâ—]") as "$".
{ iExists _. iFrame. }
rewrite Hszeq. auto with iFrame.
+ iRight. iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose".
- iFrame. iExists _. iFrame.
+ iFrame.
by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l. }
- subst. wp_read. wp_let. wp_op. wp_if.
iApply (type_type _ _ _ [ w â— box (uninit 1); #lw â— box (uninit (2 + ty.(ty_size))) ]
@@ -480,7 +478,7 @@ Section code.
iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
iExists _. iFrame. rewrite freeable_sz_full_S shift_loc_assoc. iFrame.
- iExists _. iFrame. rewrite vec_to_list_length. auto. }
+ rewrite vec_to_list_length. auto. }
iApply type_jump; solve_typing.
Qed.
End code.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index c3db62218ec057ad0fa7355de1fd8e0d878aca02..a4e4c60cb6deba7d61fb820ee1f0ebf3099fb67b 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -81,7 +81,7 @@ Section ref_functions.
iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
iMod ("Hcloseδ" with "[H↦lrc H◠Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
{ iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
- iFrame. iExists _. iFrame.
+ iFrame.
rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
@@ -89,8 +89,7 @@ Section ref_functions.
[ x ◠box (&shr{α}(ref β ty)); #lr ◠box(ref β ty)]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
- rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. simpl.
- iExists _, _, _, _, _. iFrame "∗#". }
+ rewrite /= freeable_sz_full. iFrame "∗#". simpl. iFrame "∗#". }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -170,7 +169,7 @@ Section ref_functions.
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
apply cancel_local_update_unit, _. }
iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
+ - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame "Hshr H†".
iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "$".
{ rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
by rewrite Pos.add_1_l Pos.pred_succ. }
@@ -349,7 +348,7 @@ Section ref_functions.
rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
iMod ("Hclosena" with "[H↦lrc H◠Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
{ iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
- iFrame. iExists _. iFrame.
+ iFrame.
rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ [_] _ [ #lrefs ◠box (Π[ref α ty1; ref α ty2]) ]
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index f71cc56329bfd0a3d2ea377da3bece1d88a77aa0..cd904e2a4f32ea7d0b1f5dc5051030ea7c5138ac 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -35,9 +35,8 @@ Section refcell_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lr â— box (refcell ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=.
- iFrame. iSplitL "Hx↦".
- - iExists _. rewrite uninit_own. auto.
- - simpl. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame=>//=. }
+ iFrame. iSplitR; first done.
+ simpl. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame=>//=. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -69,10 +68,8 @@ Section refcell_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit (S (ty_size ty))); #lr â— box ty]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
- iSplitR "Hr↦ Hx".
- - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
- rewrite /= vec_to_list_length. auto.
- - iExists vl. iFrame. }
+ iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
+ by rewrite /= vec_to_list_length. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -108,8 +105,7 @@ Section refcell_functions.
iApply (type_type _ _ _
[ #lx ◠box (uninit 1); #(lx' +ₗ 1) ◠&uniq{α}ty]
with "[] LFT HE Hna HL HC [-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
- iNext. iExists _. rewrite uninit_own. iFrame. }
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame. }
iApply type_assign; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -188,7 +184,7 @@ Section refcell_functions.
- done. }
iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
rewrite [_ â‹… _]comm -Some_op -!pair_op agree_idemp. iFrame.
- iExists _. iFrame. rewrite -(assoc Qp.add) Qp.div_2 //.
+ rewrite -(assoc Qp.add) Qp.div_2 //.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". { done. }
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_stR (1/2)%Qp ν)).
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index dc3cc2e95bf2d322cfdbe6c41717da97595dd796..7ac9c7e56a13da0e1ae0a3fc3c70528f6af30b94 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -147,7 +147,7 @@ Section refmut_functions.
apply (cancel_local_update_unit (writing_stR q _)), _. }
iDestruct "INV" as "(H†& Hq & _)".
rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
- last (rewrite pos_op_add; lia). iFrame.
+ last (rewrite pos_op_add; lia). iFrame "H↦lrc H†".
iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
rewrite assoc (comm _ q'' q) //. }
@@ -324,7 +324,7 @@ Section refmut_functions.
iMod ("Hclosena" with "[Hlrc H◠Hν1 H†] Hna") as "[Hβ Hna]".
{ iExists (Some (_, true, _, _)).
rewrite -Some_op -!pair_op agree_idemp /= (comm _ xH _).
- iFrame. iSplitL; [|done]. iExists _. iFrame.
+ iFrame.
rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
iApply (type_type _ [_] _ [ #lrefmuts ◠box (Π[refmut α ty1; refmut α ty2]) ]
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 6a816a428d96bba8a38d39f7b90eec91319e90eb..a0885def2fd43e71904a15ffbce686136ad8592a 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -53,9 +53,8 @@ Section rwlock_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit (ty_size ty)); #lr â— box (rwlock ty)]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
- iSplitL "Hx↦".
- - iExists _. rewrite uninit_own. auto.
- - iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. simpl. iFrame. auto. }
+ iSplitR; first done.
+ iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. simpl. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -88,9 +87,7 @@ Section rwlock_functions.
iApply (type_type _ _ _ [ #lx â— box (uninit (S (ty_size ty))); #lr â— box ty]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
- iSplitR "Hr↦ Hx".
- - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own -Hsz. iFrame. auto.
- - iExists vl. iFrame. }
+ iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own -Hsz. iFrame. auto. }
iApply type_delete; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
@@ -125,8 +122,7 @@ Section rwlock_functions.
iApply (type_type _ _ _
[ #lx ◠box (uninit 1); #(lx' +ₗ 1) ◠&uniq{α}ty]
with "[] LFT HE Hna HL HC [-]"); last first.
- { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
- iNext. iExists _. rewrite uninit_own. iFrame. }
+ { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame. }
iApply type_assign; [solve_typing..|].
iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 906d5a1818c3b4ba33a0f6cda193581e8ea4ee37..65d1bb409e0c0bf9a5d6f48c1d23e37bf8b66bfc 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -43,7 +43,7 @@ Section code.
iApply (type_call_iris _ [Ï] () [_; _]
with "LFT HE Hna [HÏ] Hf' [Henv Htl Htl†Hx'vl]"); [solve_typing| | |].
{ by rewrite /= (right_id static). }
- { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. iExists _. iFrame. }
+ { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. }
(* Prove the continuation of the function call. *)
iIntros (r) "Hna HÏ Hr". simpl.
iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
@@ -59,7 +59,7 @@ Section code.
iApply (type_type _ _ _ [ x â— _; #lr â— box (uninit ty.(ty_size)) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
- unlock. iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
+ unlock. iFrame. rewrite uninit_own. auto using vec_to_list_length. }
iApply type_delete; [solve_typing..|].
iApply type_delete; [solve_typing..|].
iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 30dc609d51b88db2f48fba3f1a134a6badeadc79..b7c458dc7d555bcea94536138fc5d6510a441080 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -197,7 +197,7 @@ Section util.
iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_pointsto_ty_own.
iDestruct "Hown" as (vl) "[??]". eauto with iFrame.
- iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v.
- iFrame. iExists _. iFrame.
+ iFrame.
Qed.
Lemma ownptr_uninit_own n m tid v :
@@ -234,8 +234,7 @@ Section typing.
rewrite typed_read_eq. iIntros (Hsz) "!>".
iIntros ([[]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
- iExists _, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
- iExists _. auto.
+ iExists _, _, _. iFrame "∗#". iSplitR; first done. by iIntros "!> $".
Qed.
Lemma read_own_move E L ty n :
@@ -258,7 +257,7 @@ Section typing.
iApply wp_new; try done. iModIntro.
iIntros (l) "(H†& Hlft & Hmeta)". rewrite tctx_interp_singleton tctx_hasty_val.
iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
- iExists (repeat #☠(Z.to_nat n)). iFrame. by rewrite /= repeat_length.
+ by rewrite /= repeat_length.
Qed.
Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 696d302c813f53e3228cf2b90832a4f7514fa8c2..e3ed62510e33c924cda2b5f92d3f14b9781c26b1 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -48,7 +48,7 @@ Section product.
- iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]".
iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2).
rewrite heap_pointsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
- iFrame. iExists _, _. by iFrame.
+ by iFrame.
Qed.
Program Definition product2 (ty1 ty2 : type) :=
@@ -205,10 +205,10 @@ Section typing.
iSplit; first by rewrite /= assoc. iSplit; iIntros "!> *"; iSplit; iIntros "H".
- iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
- iExists _, _. iSplit. { by rewrite assoc. } iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit. { by rewrite assoc. } by iFrame.
- iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
- iExists _, _. iSplit. { by rewrite -assoc. } iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit. { by rewrite -assoc. } by iFrame.
- iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
by iFrame.
- iDestruct "H" as "[[Hs1 Hs2] Hs3]". rewrite /= shift_loc_assoc_nat.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 7242ba715ab6b97e6fbcc3b30c7fae440ee8321d..1ce733098b5ff91fc1994aec5f46fc496f980776 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -78,8 +78,7 @@ Section product_split.
rewrite Nat.add_comm -hasty_ptr_offsets_offset //. }
iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
last by rewrite tctx_interp_singleton.
- rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
- iExists #l. iSplit; done.
+ rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. by iFrame.
Qed.
(** Owned pointers *)
@@ -96,9 +95,9 @@ Section product_split.
iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
iDestruct (ty_size_eq with "H1") as "#>EQ".
iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
- + iExists _. iFrame "#∗". iExists _. by iFrame.
+ + iExists _. by iFrame "#∗".
+ iExists _. iSplitR; first (by simpl; iDestruct "Hp" as %->).
- rewrite Nat2Z.id. iFrame. iExists _. by iFrame.
+ rewrite Nat2Z.id. by iFrame.
Qed.
Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
@@ -113,7 +112,7 @@ Section product_split.
rewrite HÏ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
iExists #_. iSplitR; first done. rewrite /= -freeable_sz_split Nat2Z.id. iFrame.
iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
- iExists (vl1 ++ vl2). rewrite heap_pointsto_vec_app. iFrame.
+ iExists (vl1 ++ vl2). rewrite heap_pointsto_vec_app.
iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
rewrite {3}/ty_own /=. auto 10 with iFrame.
Qed.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 10ed7a06aa2c70b1fb1f0c973d0733449c85d09d..e4cbb68e0a2c21f7f0c295c58cc1ad45248876a6 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -48,7 +48,7 @@ Section sum.
iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
iExists (#i::vl'++vl'').
rewrite heap_pointsto_vec_cons heap_pointsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
- iFrame. iExists i, vl', vl''. iSplit; first done. iFrame. iPureIntro.
+ iFrame. iExists vl''. iSplit; first done. iFrame. iPureIntro.
simpl. f_equal. by rewrite app_length Hvl'.
Qed.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index ad3f4e0a59b4d8e688f97ac7b76eb8b3243a1531..66551ab11ef9b510e4fd31092f60ce480cd0bcab 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -39,7 +39,7 @@ Section case.
iFrame. auto.
+ eauto with iFrame.
+ rewrite -EQlen app_length Nat.add_comm Nat.add_sub shift_loc_assoc Nat2Z.id.
- iFrame. iExists _. iFrame. auto.
+ by iFrame.
- rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
iExists (#i :: vl' ++ vl''). iNext. rewrite heap_pointsto_vec_cons heap_pointsto_vec_app.
iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=. auto.
@@ -264,7 +264,7 @@ Section case.
iMod ("Hw" with "[-HLclose HL1]") as "[HL $]"; last first.
{ iApply "HLclose". by iFrame. }
iNext.
- rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
+ rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame "H↦0".
iSplitL "H↦pad".
- rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.
iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.