Fix [tp_alloc]

Previously [tp_alloc] would just delete [j \Mapsto fill K (Alloc e)]
from the context without a replacement.

F_mu_ref_conc/tactics.v

@@ -790,59 +790,51 @@ Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
 Tactic Notation "tp_fork" constr(j) "as" ident(j') :=
   let H := iFresh in tp_fork j as j' H.
 
-Lemma tac_tp_alloc `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e' v Q :
+Lemma tac_tp_alloc `{heapIG Σ, !cfgSG Σ} j Δ1 E1 E2 ρ i1 i2 p K' e e' v Q :
   nclose specN ⊆ E1 →
   envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
-  envs_lookup_delete i2 Δ1 = Some (false, j ⤇ fill K e, Δ2)%I →
-  fill K e = fill K' (Alloc e') →
+  envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
+  e = fill K' (Alloc e') →
   to_val e' = Some v →
-  (Δ2 ⊢ (∀ (l : loc), (l ↦ₛ v) -∗ |={E1,E2}=> Q)%I) →
+  (∀ l, ∃ Δ2,
+    envs_simple_replace i2 false
+       (Esnoc Enil i2 (j ⤇ fill K' (Loc l))) Δ1 = Some Δ2 ∧
+    (Δ2 ⊢ (l ↦ₛ v) -∗ |={E1,E2}=> Q)%I) →
   (Δ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_lookup_delete_sound'. 2: exact H2.
-  rewrite Hfill.
-  (* (S (spec_ctx ρ) (S (j => fill) (S (l ↦ v) ..))) *)
+  rewrite (envs_lookup_sound' Δ1 _). 2: exact H2.
   rewrite (assoc _ (spec_ctx ρ) (j ⤇ _)%I).
+  rewrite Hfill.
   rewrite step_alloc //.
   rewrite -(fupd_trans E1 E1 E2).
-  rewrite fupd_frame_r. 
-  apply fupd_mono. 
+  rewrite fupd_frame_r.
+  apply fupd_mono.
   rewrite uPred.sep_exist_r.
-  apply uPred.exist_elim. intros l.
+  apply uPred.exist_elim=> l.
+  destruct (HQ l) as [Δ2 [HΔ2 HQ']].
+  rewrite (envs_simple_replace_sound' _ _ i2 _ _ HΔ2).
+  simpl. rewrite right_id.
   rewrite (comm _ (j ⤇ _)%I (l ↦ₛ _)%I).
-  rewrite HQ.
-  rewrite (comm _ (l ↦ₛ _)%I).
-  rewrite -assoc.
-  rewrite (uPred.forall_elim l).
-  rewrite uPred.sep_elim_r.
+  rewrite -assoc. 
+  rewrite uPred.wand_elim_r.
+  rewrite HQ'.
   by rewrite uPred.wand_elim_r.
 Qed.
 
-Tactic Notation "tp_alloc" constr(j) :=
-  iStartProof;
-  eapply (tac_tp_alloc j);
-    [solve_ndisj || fail "tp_alloc: cannot prove 'nclose specN ⊆ ?'"
-    |iAssumptionCore || fail "tp_alloc: cannot find spec_ctx" (* spec_ctx *)
-    |iAssumptionCore || fail "tp_alloc: cannot find '" j " ⤇ ?'" 
-    |tp_bind_helper
-    |fast_done || fail "tp_alloc: not a value"
-    |(* new goal *)]; try (tp_normalise j).
-
 Tactic Notation "tp_alloc" constr(j) "as" ident(j') constr(H) :=
   iStartProof;
   eapply (tac_tp_alloc j);
     [solve_ndisj || fail "tp_alloc: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_alloc: cannot find spec_ctx" (* spec_ctx *)
-    |iAssumptionCore || fail "tp_alloc: cannot find '" j " ⤇ ?'" 
+    |iAssumptionCore || fail "tp_alloc: cannot find '" j " ⤇ ?'"
     |tp_bind_helper
-    |fast_done || fail "tp_alloc: not a value"
-    |(iIntros (j') || fail 1 "tp_alloc: " j' " not fresh ");
-     (iIntros H || fail 1 "tp_alloc: " H " not fresh")
-    (* new goal *)]; try (tp_normalise j).
+    |try fast_done
+    |intros j'; eexists; split; [by env_cbv; reflexivity| iIntros H]
+    (* new goal *)].
 
 Tactic Notation "tp_alloc" constr(j) "as" ident(j') :=
   let H := iFresh in tp_alloc j as j' H.
@@ -854,15 +846,14 @@ Definition bot := App (TApp (TLam (Rec (App (Var 0) (Var 1))))) Unit.
 Notation Lam e := (Rec (e.[ren (+1)])).
 Notation LamV e := (RecV (e.[ren (+1)])).
 
-Lemma alloc_test E K j n ρ : 
+Lemma alloc_test E K j n ρ :
   nclose specN ⊆ E →
   j ⤇ fill K (App (Lam (Store (Var 0) (#n (n + 10)))) (Alloc (#n n))) -∗
-  spec_ctx ρ ={E}=∗ True.                        
+  spec_ctx ρ ={E}=∗ True.
 Proof.
   iIntros (?) "Hj #?".
-  tp_alloc j. iIntros (l) "Hl". Undo. Undo.
   tp_alloc j as l. Undo.
-  tp_alloc j as l "Hl".
+  tp_alloc j as l "Hl". tp_normalise j.
   done.
 Qed.