From ebd06e136d54b1d8e47329609efb3cb552249ee7 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 13 Nov 2023 11:39:32 +0100
Subject: [PATCH] =?UTF-8?q?Patch=20now=20that=20frame=20=E2=88=83=20looks?=
=?UTF-8?q?=20beneath=20definitions=20again?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
theories/lang/lib/arc.v | 2 +-
theories/typing/lib/arc.v | 8 ++++----
theories/typing/lib/brandedvec.v | 11 ++---------
theories/typing/lib/rc/rc.v | 6 +++---
theories/typing/lib/rc/weak.v | 6 +++---
theories/typing/lib/rwlock/rwlock.v | 2 +-
theories/typing/lib/rwlock/rwlock_code.v | 10 +++++-----
theories/typing/product.v | 4 ++--
theories/typing/product_split.v | 3 +--
9 files changed, 22 insertions(+), 30 deletions(-)
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index e6111801..c50a56d4 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -407,7 +407,7 @@ Section arc.
split; last by rewrite /= left_id; apply Hv. split=>[|//].
apply frac_valid. rewrite /= -Heq comm_L.
by apply Qp.add_le_mono_l, Qp.div_le. }
- iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
+ iFrame. iApply "Hclose1". iExists _. iFrame.
rewrite /= [xH â‹… _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
Qp.div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 8524692a..4712bfc6 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -792,8 +792,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.
@@ -827,8 +827,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.
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index b7938974..ce5730cb 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -200,10 +200,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")
@@ -398,11 +395,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 γ. eauto with 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/rc/rc.v b/theories/typing/lib/rc/rc.v
index 53e8bc63..f2af7f3a 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -321,8 +321,8 @@ Section code.
iSplitL "Hty".
{ iDestruct "Hty" as (vy) "[H Hty]". iExists vy. iFrame.
by iApply "Hinclo". }
- iIntros "!> H". iApply ("Hclose" with "[>-]"). iFrame. iExists _.
- iFrame. rewrite Hincls /= !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+ iIntros "!> H". iApply ("Hclose" with "[>-]"). iFrame.
+ rewrite Hincls /= !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
by iFrame.
* iIntros "Hl1".
iMod (own_update_2 with "Hst Htok") as "[Hst Htok]".
@@ -374,7 +374,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 "Hst". iExists (q+q'')%Qp. iFrame.
+ iApply "Hclose". iFrame "Hst Hl2 Hl†Hna Hν†". 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.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 4c688331..9a1c5996 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -406,16 +406,16 @@ Section code.
destruct st as [[[q'' strong]| |]|]; [..|done|].
- iExists _. iDestruct "Hrcst" as (q0) "(Hlw & >$ & Hrcst)". iRight.
iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
- iExists _. iFrame. by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+ 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. by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+ 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))) ]
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 24bb5841..9676e30c 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -164,7 +164,7 @@ Section rwlock.
rewrite Qp.div_2. iSplitL; last by auto.
iIntros "!> !> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]".
- iMod (own_alloc (◠writing_st)) as (γ) "Hst". { by apply auth_auth_valid. }
- iFrame. iExists _, _. eauto with iFrame.
+ by iFrame.
Qed.
Next Obligation.
iIntros (?????) "#Hκ H". iDestruct "H" as (α γ) "[#??]".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index bd42d400..9e7068bb 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -192,8 +192,8 @@ Section rwlock_functions.
- apply frac_valid. rewrite /= -Hqq' comm_L.
by apply Qp.add_le_mono_l, Qp.div_le.
- done. }
- iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _.
- iFrame "∗#". iSplitR; first by rewrite /= Hag agree_idemp.
+ iFrame "∗#". rewrite Z.add_comm /=. iFrame.
+ iSplitR; first by rewrite /= Hag agree_idemp.
rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first solve_ndisj.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
@@ -215,8 +215,8 @@ Section rwlock_functions.
#lx ◠rwlockreadguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
- tctx_hasty_val' //. iFrame.
- iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
+ tctx_hasty_val' //. iFrame "∗#".
+ iApply ty_shr_mono; last done.
iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
simpl. iApply type_jump; solve_typing.
@@ -290,7 +290,7 @@ Section rwlock_functions.
#lx ◠rwlockwriteguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
- tctx_hasty_val' //. iFrame. iExists _, _, _. iFrame "∗#". }
+ tctx_hasty_val' //. iFrame "∗#". }
iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
simpl. iApply type_jump; solve_typing.
Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index fe940a21..f647f477 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -201,10 +201,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; first by rewrite assoc. iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit; first by rewrite assoc. by iFrame.
- iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
- iExists _, _. iSplit; first by rewrite -assoc. iFrame. iExists _, _. by iFrame.
+ iExists _, _. iSplit; first 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 a545e555..f575e1aa 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 *)
--
GitLab