diff --git a/F_mu_ref_conc/tactics.v b/F_mu_ref_conc/tactics.v index 940502321ed2f1c58a410d0f7c9a389a20fa8819..15b34c6b446ba645baf172843328c3d56f26dcac 100644 --- a/F_mu_ref_conc/tactics.v +++ b/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 _ _)).