diff --git a/comments.org b/comments.org index fe2789ed7be90f84dc42cf822eab69add8e4216a..715379669aabf065bf608997c33429591455fb22 100644 --- a/comments.org +++ b/comments.org @@ -169,3 +169,37 @@ One observation is that the easiest (as well as the most numerous) tactics to wr To that extent we would like to have one generic "pure symbolic reduction" tactic/tactic lemma per level. This is achieved by writing "open ended" tactic lemmas that are parameterized over a typeclass of pure reductions. The typeclass ~PureExec φ e1 e2~ says that there is a pure (and deterministic) reduction from ~e1~ to ~e2~ in the language under some (pure) assumption φ. +Using this typeclass and typeclass resolution we can write tactic lemmas that are easy to apply: +#+BEGIN_SRC +Lemma tac_rel_pure_r `{logrelG Σ} K e1 ℶ E1 E2 Δ Γ e e2 eres ϕ t τ : + e = fill K e1 → + PureExec ϕ e1 e2 → + ϕ → + nclose specN ⊆ E1 → + eres = fill K e2 → + (ℶ ⊢ {E1,E2;Δ;Γ} t ≤log≤ (fill K e2) : τ) → + (ℶ ⊢ {E1,E2;Δ;Γ} t ≤log≤ e : τ). +#+END_SRC +When ~tac_rel_pure~ is applied, it tries to solve the first goal ~e = fill K e1~ by decomposing expression ~e~ in all the possible ways +and trying to unify it with ~e1~. After that it searches for an appropriate ~PureExec~ instance. +The whole process is implemented in the following tactic +#+BEGIN_SRC +Tactic Notation "rel_pure_r" open_constr(ef) := + iStartProof; + rel_reshape_cont_r ltac:(fun K e' => + unify e' ef; + simple eapply (tac_rel_pure_r K e'); + [tac_bind_helper (* e = fill K e1 *) + |apply _ (* PureExec ϕ e1 e2 *) + |try (exact I || reflexivity || tac_rel_done) (* φ *) + |solve_ndisj (* ↑specN ⊆ E1 *) + |simpl; reflexivity (* eres = fill K e2 *) + |simpl_subst/= (* new goal *)]) + || fail "rel_pure_r: cannot find the reduct". +#+END_SRC +Ignoring the "fail" part, we can see from the outline what is going on in the tactic: +- It tries to reshape the expression on the right hand side in the relational interpretation, until the tactic succeeds. +- It only proceeds with the specific decomposition if ~e = K[e']~ and ~e'~ unifies with ~ef~. +- After that, it applies the tactic lemma and tries to discharge the proof obligations in order +- Sometimes, the dependency ~φ~ in ~PureExec φ e1 e2~ can be discharged trivially by ~reflexivity~ or ~tac_rel_done~. +- We simplify the substitutions in the new goal, in case we do a beta-reduction