Add the tp tactic to F_mu_ref_conc

F_mu_ref_conc/fundamental_binary.v

@@ -317,28 +317,26 @@ Section fundamental.
     iDestruct "Hv" as ([w w']) "[% #Hτi]"; simplify_eq/=.
     iDestruct "Hτi" as (τi) "[% #Hτi]"; simplify_eq/=.
     iApply wp_pack; eauto. iNext.
-    iMod (step_Pack _ _ j K with "[-]") as "Hz"; eauto. 
+    iApply fupd_wp. 
+    tp_pack j; eauto. tp_normalise j. iModIntro.
     iApply wp_wand_r. iSplitL.
     iDestruct (interp_env_length with "HΓ") as "%".
     replace (e2.[up (env_subst (vvs.*1))].[of_val w/])
-       with (e2.[(env_subst (((w,w')::vvs).*1))]); eauto.
+       with (e2.[(env_subst (((w,w')::vvs).*1))]); last first.
+    { asimpl. erewrite typed_subst_head_simpl; eauto.
+      simpl. repeat rewrite fmap_length; eauto. }    
     replace (e2'.[up (env_subst (vvs.*2))].[of_val w'/])
-       with (e2'.[(env_subst (((w,w')::vvs).*2))]); eauto.
+       with (e2'.[(env_subst (((w,w')::vvs).*2))]); last first.
+    { asimpl. erewrite typed_subst_head_simpl; eauto.
+      simpl. repeat rewrite fmap_length; eauto. }
     iApply ('IHHtyped2 (τi :: Δ) _ _ j K).
-    { iFrame. iFrame "Hs".
+    { iFrame. iFrame "Hs". 
       iApply interp_env_cons; auto.
       rewrite interp_env_ren. iFrame "HΓ". iFrame "Hτi". }
-    Focus 3.
     iIntros (v) "Hv'". iDestruct "Hv'" as (v') "[Hv Hτ2]".
     iExists v'.
     replace (⟦ τ2 ⟧ Δ) with (⟦ τ2 ⟧ ([] ++ Δ)); eauto.
     rewrite (interp_weaken [] [τi] Δ τ2). iFrame.
-
-    asimpl. erewrite typed_subst_head_simpl; eauto.
-    simpl. repeat rewrite fmap_length; eauto.
-
-    asimpl. erewrite typed_subst_head_simpl; eauto.
-    simpl. repeat rewrite fmap_length; eauto.
   Qed.
   
   Lemma bin_log_related_fork Γ e e'

F_mu_ref_conc/tactics.v

@@ -24,6 +24,7 @@ Ltac reshape_val e tac :=
   | InjL ?e => let v := go e in constr:(InjLV v)
   | InjR ?e => let v := go e in constr:(InjRV v)
   | Fold ?e => let v := go e in constr:(FoldV v)
+  | Pack ?e => let v := go e in constr:(PackV v)
   | Loc ?l => constr:(LocV l)
   end in let v := go e in tac v.
 
@@ -47,6 +48,8 @@ Ltac reshape_expr e tac :=
   | Fold ?e => go (FoldCtx :: K) e
   | Unfold ?e => go (UnfoldCtx :: K) e
   | TApp ?e => go (TAppCtx :: K) e
+  | Pack ?e => go (PackCtx :: K) e 
+  | Unpack ?e1 ?e2 => go (UnpackLCtx e2 :: K) e 
   | Alloc ?e => go (AllocCtx :: K) e
   | Load ?e => go (LoadCtx :: K) e
   | Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
@@ -512,6 +515,43 @@ Tactic Notation "tp_fold" constr(j) :=
     |env_cbv; reflexivity || fail "tp_fold: this should not happen"
     |(* new goal *)].
 
+Lemma tac_tp_pack `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e1 e2 v Q :
+  nclose specN ⊆ E1 →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
+  e = fill K' (Unpack (Pack e1) e2) →
+  to_val e1 = Some v →
+  envs_simple_replace i2 false 
+    (Esnoc Enil i2 (j ⤇ fill K' (e2.[e1/]))) Δ1 = Some Δ2 →
+  (Δ2 ⊢ |={E1,E2}=> Q) →
+  (Δ1 ⊢ |={E1,E2}=> Q).
+Proof.
+  intros ??? Hfill ?? HQ.
+  rewrite -(idemp uPred_and Δ1).
+  rewrite {2}(envs_lookup_sound' Δ1 _). 2: exact H1.
+  rewrite uPred.sep_elim_l uPred.always_and_sep_r comm.
+  rewrite (envs_simple_replace_sound Δ1 Δ2 i2) //; simpl.
+  rewrite right_id. rewrite Hfill.
+  (* (S (spec_ctx ρ) (S (j => fill) (S (l ↦ v) ..))) *)
+  rewrite (assoc _ (spec_ctx ρ) (j ⤇ _)%I).
+  rewrite step_Pack //.
+  rewrite -(fupd_trans E1 E1 E2).
+  rewrite fupd_frame_r. 
+  apply fupd_mono. rewrite uPred.wand_elim_r.
+  done.
+Qed.
+
+Tactic Notation "tp_pack" constr(j) :=
+  iStartProof;
+  eapply (tac_tp_pack j);
+    [solve_ndisj || fail "tp_pack: cannot prove 'nclose specN ⊆ ?'"
+    |iAssumptionCore || fail "tp_pack: cannot find spec_ctx" (* spec_ctx *)
+    |iAssumptionCore || fail "tp_pack: cannot find '" j " ⤇ ?'" 
+    |tp_bind_helper
+    |try fast_done
+    |env_cbv; reflexivity || fail "tp_pack: this should not happen"
+    |(* new goal *)].
+
 
 Lemma tac_tp_fst `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e1 e2 v1 v2 Q :
   nclose specN ⊆ E1 →