Commit e13439ec authored by Dan Frumin's avatar Dan Frumin

Rewrite the rel_rec_r tactic to pick up the correct reduct

We have to call tac_rel_rec_r in reshape_expr because reshape_expr
just decomposes the expression into a `(K',e')` without guaranteeing
that `e` is actually head-reducible. Because of that it might be the
case that `e` is `K[App (Rec f x e1) e2]`, but `e2` is not a value.
parent 5179b6c8
......@@ -28,7 +28,7 @@ Lemma tac_rel_bind_r `{heapIG Σ, !cfgSG Σ} t' K Δ E1 E2 Γ e t τ :
(Δ bin_log_related E1 E2 Γ e t τ).
Proof. intros. eapply tac_rel_bind_gen; eauto. Qed.
Local Ltac tac_bind_helper :=
Ltac tac_bind_helper :=
rewrite ?fill_app /=;
lazymatch goal with
| |- fill ?K ?e = fill _ ?efoc =>
......@@ -42,6 +42,15 @@ Local Ltac tac_bind_helper :=
replace e with (fill K' e') by (by rewrite ?fill_app))
end; reflexivity.
Ltac rel_reshape_cont_r tac :=
lazymatch goal with
| |- _ bin_log_related _ _ _ _ (fill ?K ?e) _ =>
reshape_expr e ltac:(fun K' e' =>
tac (K' ++ K) e')
| |- _ bin_log_related _ _ _ _ ?e _ =>
reshape_expr e ltac:(fun K' e' => tac K' e')
end.
Tactic Notation "rel_bind_l" open_constr(efoc) :=
iStartProof;
eapply (tac_rel_bind_l efoc);
......@@ -203,14 +212,18 @@ Qed.
Tactic Notation "rel_rec_r" :=
iStartProof;
eapply (tac_rel_rec_r);
[solve_ndisj || fail "rel_rec_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' _ *)
|simpl; fast_done
|solve_closed
|try fast_done (* to_val e' = Some v *)
|try fast_done (* eres = subst ... *)
|simpl; rewrite ?Closed_subst_id (* new goal *)].
rel_reshape_cont_r ltac:(fun K e' =>
match eval hnf in e' with App ?e1 ?e2 =>
eapply (tac_rel_rec_r _ _ _ _ _ _ _ _ e1 e2);
[solve_ndisj || fail "rel_rec_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' _ *)
|simpl; fast_done
|solve_closed
|fast_done (* to_val e' = Some v *)
|try fast_done (* eres = subst ... *)
|simpl; rewrite ?Closed_subst_id (* new goal *)]
end)
|| fail "rel_rec_r: cannot find '(λx.e) ..'".
Tactic Notation "rel_seq_r" := rel_rec_r.
Tactic Notation "rel_let_r" := rel_rec_r.
......
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