diff --git a/F_mu_ref_conc/tactics.v b/F_mu_ref_conc/tactics.v index f252764cec368261413a54596f0081c5b97fddc2..a336530af4a85897af20712ab3cb9a4d5bfc868a 100644 --- a/F_mu_ref_conc/tactics.v +++ b/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.