Finish the tp_ family of tactics for F_mu_ref_conc

F_mu_ref_conc/tactics.v

@@ -90,6 +90,16 @@ Proof.
   rewrite right_id. rewrite H1. by rewrite uPred.wand_elim_r.
 Qed.
 
+Lemma tac_tp_norm `{heapIG Σ, !cfgSG Σ} j Δ Δ' i p (e : expr) Q :
+  envs_lookup i Δ = Some (p, j ⤇ e)%I →
+  envs_simple_replace i p (Esnoc Enil i (j ⤇ fill [] e)) Δ = Some Δ' →
+  (Δ' ⊢ Q) →
+  (Δ ⊢ Q).
+Proof.
+  simpl. intros. rewrite envs_simple_replace_sound //. simpl.
+  rewrite right_id. rewrite H2. by rewrite uPred.wand_elim_r.
+Qed.
+
 Ltac tp_bind_helper :=
   lazymatch goal with
   | |- fill ?K ?e = fill _ ?efoc =>
@@ -126,14 +136,20 @@ Lemma fill_nil e : fill [] e = e.
 Proof. by compute. Qed.
 (* TODO: if the proposition is of the form 
 [j ⤇ e], rewrite it to [j ⤇ fill [] e] using fill_nil above
+TODO: this is quite slow
 *)
 Tactic Notation "tp_normalise" constr(j) :=
   iStartProof;
-  eapply (tac_tp_bind j);
+  (eapply (tac_tp_bind j);
     [iAssumptionCore (* prove the lookup *)
-    |by (rewrite ?fill_app); simpl (* do actual work *)
+    |by (simpl; rewrite ?fill_app); simpl (* do actual work *)
     |env_cbv; reflexivity
-    |(* new goal *)].
+    |(* new goal *)]).
+   (* || (eapply (tac_tp_norm j); *)
+   (*    [iAssumptionCore (* prove the lookup *) *)
+   (*    |env_cbv; reflexivity *)
+   (*    |(* new goal *)]). *)
+
 
 (* TODO: figure out why the envs_simple_replace_sound lemma is not
 strong enough. Try to see whether you could generalize it
@@ -817,12 +833,69 @@ Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
     |tp_bind_helper
     |env_cbv; reflexivity || fail "tp_fork: this should not happen"
     |(iIntros (j') || fail 1 "tp_fork: " j' " not fresh ");
-     (iIntros H || fail 1 "tp_fork: " H " not fresh")
+     (iIntros H || fail 1 "tp_fork: " H " not fresh");
+     try (tp_normalise j')
     (* new goal *)]; try (tp_normalise j).
 
 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 :
+  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') →
+  to_val e' = Some v →
+  (Δ2 ⊢ (∀ (l : loc), (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 (assoc _ (spec_ctx ρ) (j ⤇ _)%I).
+  rewrite step_alloc //.
+  rewrite -(fupd_trans E1 E1 E2).
+  rewrite fupd_frame_r. 
+  apply fupd_mono. 
+  rewrite uPred.sep_exist_r.
+  apply uPred.exist_elim. intros l.
+  rewrite (comm _ (j ⤇ _)%I (l ↦ₛ _)%I).
+  rewrite HQ.
+  rewrite (comm _ (l ↦ₛ _)%I).
+  rewrite -assoc.
+  rewrite (uPred.forall_elim l).
+  rewrite uPred.sep_elim_r.
+  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 " ⤇ ?'" 
+    |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).
+
+Tactic Notation "tp_alloc" constr(j) "as" ident(j') :=
+  let H := iFresh in tp_alloc j as j' H.
 
 Section test.
 Context `{heapIG Σ, !cfgSG Σ}.
@@ -831,6 +904,18 @@ 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 ρ : 
+  nclose specN ⊆ E →
+  j ⤇ fill K (App (Lam (Store (Var 0) (#n (n + 10)))) (Alloc (#n n))) -∗
+  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".
+  done.
+Qed.
+
 Lemma test1 E1 j K l n ρ :
   nclose specN ⊆ E1 →
   j ⤇ fill K (App (Lam (Store (Loc l) (BinOp Add (Nat 1) (Var 0)))) (Load (Loc l))) -∗
@@ -858,9 +943,8 @@ Proof.
   iIntros (?) "Hj #? Hl".
   tp_fork j as i "Hi". Undo.
   tp_fork j as i. Undo.
-  tp_fork j. iIntros (i) "Hi".  
-  rewrite -(fill_nil (Fork _)). 
-  tp_fork i as k "Hk". rewrite -(fill_nil (App _ _)). 
+  tp_fork j. iIntros (i) "Hi". rewrite -(fill_nil (Fork _)). 
+  tp_fork i as k "Hk". rewrite -(fill_nil (App _ _)).
   tp_cas_suc k.  (* TODO: tp_normalise fails here, as fill [...] e reduces to an expression without an outer context *)
   rewrite /= -(fill_nil (App _ _)). 
   tp_if_true k. rewrite /= -(fill_nil (App _ _)).