Warming up on eliminator refinement [01KS]
Now that higher-order goal matching is in reasonably good shape, it is possible for me to begin considering the implementation of Epigram-style eliminator refinement. The goal would to be able to write code like this:
paste (A : Type) (u v w : A) (p : u = v) (q : v = w) : u = w where
paste A u v w p q <= elim p
paste A u u w refl q => q
This would elaborate to something very complicated involving a severely generalised induction motive, cut down to size in the methods by several uses of based path induction. For the first version, I do not plan to support the full elimination of dependent pattern matching, and I will be focusing only the solution rule. To undersatnd what this rule does, let us walk through how paste should be elaborated to an instance of the J eliminator. Conor Titania Mc Bride’s “basic analysis” of elim p in this scenario leads to the following identification induction motive:
x0 : A, x1 : A, x01 : x0 = x1 |-
(u v w : A) (p : u = v) (q : v = w)
-> (x0, x1, x01) =* (u, v, p)
-> <paste A u v w p q : u = w>
In the above, =* is short for telescopic identity, which unravels to something very complicated involving a lot of transports. If we apply the J eliminator targeting (u,v,w) with such a generalised motive, we can further instantiate the result by A, u, v, w, p, q, (refl, refl, refl).
In the base case for this induction, we must solve the following goal:
x : A |-
(u v w : A) (p : u = v) (q : v = w)
-> (x, x, refl) = (u, v, p)
-> <paste A u v w p q : u = w>
It is at this point that Mc Bride’s rules simplification rules come into play (or, to be precise, the proof-relevant ones described by Jesper Cockx). In the above, the variables A,u,v,w,p,q are considered “flexible” and we want to successively apply elimination rules to the components of the telescopic identification (x, x, refl) = (u, v, p). Although it is not easy to write out the full expansion of this telescopic identification, we know that its first component is an identification hu : x = u. If we proceed by identification induction on hu, then the telescopic identification that remains is (hv : x = v) (hp : transport (x =_) hv refl = p). If we do identification induction on hv, then what remains is (hp : refl = p), which we may dispatch finally using identification induction. All that remains of the goal is the following, which the user-written match clause explains how to solve:
x : A |- (w : A) (q : x = w) -> <paste A x x w refl q : x = w>
Of course, the explanation above in some sense misses the hard part: identification induction can only really reduce the telescope when we have a segment like (u : A) (p : t = u), where the flexible variable is directly adjacent to its defining path. This means we must somehow re-order the telescope, but that requires strengthening, which is notoriously difficult to handle in a way that respects definitional equality (if you see a call to freeVars, they blew it!). I can’t say for sure, but I do see that Agda’s implementation is looking at the free variables set, and this must account for at least some user-facing unreliability or instability.
In a subsequent post, I will suggest what I think is a reasonable way to handle strengthening in a semantic way, taking advantage of other infrastructure I have built.