WIP type_sum fixed

theories/typing/type_sum.v

@@ -16,7 +16,7 @@ Section case.
       typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) e) tyl el →
     typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
   Proof.
-    iIntros (Hel tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
     iDestruct "Hp" as "[H↦ Hf]". iDestruct "H↦" as (vl) "[H↦ Hown]".
@@ -30,7 +30,7 @@ Section case.
     destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
     edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
     wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
-    destruct Hety as [Hety|Hety]; iApply (Hety with "LFT Hna HE HL HC");
+    destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
     - iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
       iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
@@ -61,7 +61,7 @@ Section case.
       typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) e) tyl el →
     typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) (case: !p of el).
   Proof.
-    iIntros (Halive Hel tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
@@ -85,16 +85,16 @@ Section case.
         iFrame. iExists _, _, _. iSplit. by auto.
         rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
       { iExists vl'. iFrame. }
-      iMod ("Hclose" with "Htok") as "[HE HL]".
-      iApply (Hety with "LFT Hna HE HL HC").
+      iMod ("Hclose" with "Htok") as "HL".
+      iApply (Hety with "LFT HE Hna HL HC").
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
     - iMod ("Hclose'" with "[] [H↦i H↦vl' H↦vl'' Hown]") as "[Hb Htok]";
         [by iIntros "!>$"| |].
       { iExists (#i::vl'++vl'').
         rewrite heap_mapsto_vec_cons heap_mapsto_vec_app /= -EQlen. iFrame. iNext.
         iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
-      iMod ("Hclose" with "Htok") as "[HE HL]".
-      iApply (Hety with "LFT Hna HE HL HC").
+      iMod ("Hclose" with "Htok") as "HL".
+      iApply (Hety with "LFT HE Hna HL HC").
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
   Qed.
 
@@ -114,7 +114,7 @@ Section case.
       typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) e) tyl el →
     typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) (case: !p of el).
   Proof.
-    iIntros (Halive Hel tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
     iDestruct "Hp" as (i) "[#Hb Hshr]".
@@ -125,8 +125,8 @@ Section case.
     edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
     wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
     iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
-    iMod ("Hclose" with "Htok") as "[HE HL]".
-    destruct Hety as [Hety|Hety]; iApply (Hety with "LFT Hna HE HL HC");
+    iMod ("Hclose" with "Htok") as "HL".
+    destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame.
     iExists _. rewrite ->nth_lookup, EQty. auto.
   Qed.
@@ -146,7 +146,7 @@ Section case.
     typed_write E L ty1 (sum tyl) ty2 →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]%TC).
   Proof.
-    iIntros (Hty Hw tid qE) "#LFT $ HE HL Hp".
+    iIntros (Hty Hw tid) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
@@ -186,7 +186,7 @@ Section case.
     typed_write E L ty1 (sum tyl) ty2 →
     typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]%TC).
   Proof.
-    iIntros (Hty Hw tid qE) "#LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
     iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
     simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
@@ -217,17 +217,17 @@ Section case.
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
                (p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
-    iIntros (Hty Hw Hr tid qE) "#LFT Htl [HE1 HE2] [HL1 HL2] Hp".
+    iIntros (Hty Hw Hr tid) "#LFT #HE Htl [HL1 HL2] Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
     iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
-    iMod (Hw with "[] LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
+    iMod (Hw with "[] LFT HE HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
     destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
     wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
     wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
-    iMod (Hr with "[] LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=.
+    iMod (Hr with "[] LFT HE Htl HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=.
     subst. assert (ty.(ty_size) ≤ length vl1).
     { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
       - intros [= ->]. lia.
@@ -239,7 +239,7 @@ Section case.
     { rewrite take_length. lia. }
     iNext; iIntros "[H↦vl1 H↦2]".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
-    iMod ("Hr" with "H↦2") as "($ & $ & $ & $)". iApply "Hw". iNext.
+    iMod ("Hr" with "H↦2") as "($ & $ & $)". iApply "Hw". iNext.
     rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
     iSplitL "H↦pad".
     - rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.