Commit 21652cac authored by Robbert Krebbers's avatar Robbert Krebbers

Eliminate redundant tp_bind_helper_constr.

parent e7cc3560
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment