diff --git a/F_mu_ref_conc/tactics.v b/F_mu_ref_conc/tactics.v index 52e646cc05fade9aa324e9d5217d83e0172bddda..c2e01c65951803ba34979f8348a82c63aa5b0bcf 100644 --- a/F_mu_ref_conc/tactics.v +++ b/F_mu_ref_conc/tactics.v @@ -31,7 +31,9 @@ Ltac reshape_val e tac := Ltac reshape_expr e tac := let rec go K e := match e with - | _ => tac (reverse K) e + | _ => + let Krev := eval cbn[reverse rev_append] in (reverse K) in + tac Krev e | App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2) | App ?e1 ?e2 => go (AppLCtx e2 :: K) e1 | BinOp ?op ?e1 ?e2 => @@ -90,7 +92,7 @@ Proof. rewrite right_id. rewrite H1. by rewrite uPred.wand_elim_r. Qed. -Lemma tac_tp_bind `{heapIG Σ, !cfgSG Σ} j Δ Δ' i p K' e e' Q : +Lemma tac_tp_bind `{heapIG Σ, !cfgSG Σ} j e' Δ Δ' i p K' e Q : envs_lookup i Δ = Some (p, j ⤇ e)%I → e = fill K' e' → envs_simple_replace i p (Esnoc Enil i (j ⤇ fill K' e')) Δ = Some Δ' → @@ -105,39 +107,18 @@ Ltac tp_bind_helper := lazymatch goal with | |- fill ?K ?e = fill _ ?efoc => reshape_expr e ltac:(fun K' e' => - unify e' efoc; - lazymatch eval cbn in (K ++ K') with - | ?K'' => - replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app) - end) + unify e' efoc; + let K'' := eval cbn[app] in (K ++ K') in + replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app)) | |- ?e = fill _ ?efoc => reshape_expr e ltac:(fun K' e' => - unify e' efoc; - replace e with (fill K' e') by (by rewrite ?fill_app)) + unify e' efoc; + replace e with (fill K' e') by (by rewrite ?fill_app)) end; reflexivity. -Ltac tp_bind_helper_constr efoc := - rewrite ?fill_app /=; - lazymatch goal with - | |- fill ?K ?e%I = fill _ _ => - reshape_expr e ltac:(fun K' e' => - unify e' efoc; - lazymatch eval cbn in (K ++ K') with - | ?K'' => - replace (fill K e) - with (fill K'' e') - by (rewrite ?fill_app; reflexivity) - end) - | |- ?e = fill _ _ => - reshape_expr e ltac:(fun K' e' => - unify e' efoc; - replace e with (fill K' e') by reflexivity) - end; reflexivity. - -(* TODO: this is quite slow *) Tactic Notation "tp_normalise" constr(j) := iStartProof; - (eapply (tac_tp_bind_gen j); + eapply (tac_tp_bind_gen j); [iAssumptionCore (* prove the lookup *) | lazymatch goal with | |- fill ?K ?e = _ => @@ -146,13 +127,13 @@ Tactic Notation "tp_normalise" constr(j) := idtac "nice" end |env_cbv; reflexivity - |(* new goal *)]). + |(* new goal *)]. Tactic Notation "tp_bind" constr(j) open_constr(efoc) := iStartProof; - eapply (tac_tp_bind j); + eapply (tac_tp_bind j efoc); [iAssumptionCore (* prove the lookup *) - |tp_bind_helper_constr efoc (* do actual work *) + |tp_bind_helper (* do actual work *) |env_cbv; reflexivity |(* new goal *)]. @@ -905,7 +886,7 @@ 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))) -∗ spec_ctx ρ -∗ - l ↦ₛ (NatV n) ={E1}=∗ True. + l ↦ₛ (NatV n) ={E1}=∗ True. Proof. iIntros (?) "Hj #? Hl". tp_load j. @@ -929,9 +910,10 @@ Proof. tp_fork j as i "Hi". Undo. tp_fork j as i. Undo. tp_fork j. iIntros (i) "Hi". - tp_fork i as k "Hk". tp_normalise i. tp_normalise j. + tp_fork i as k "Hk". tp_normalise i. + tp_normalise j. tp_cas_suc k. tp_normalise k. - tp_if_true k. + tp_if_true k. tp_normalise k. tp_rec k. asimpl. tp_fst k. done.