@@ -169,3 +169,37 @@ One observation is that the easiest (as well as the most numerous) tactics to wr

...

@@ -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.

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.

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 φ.

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