[Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?

[Peter Hancock]

On 19/06/2014 17:24, Brent Yorgey wrote, about lifting decidability of equality on X to
equality of lists of X's:

> ...  can someone suggest a way
> to rewrite the code so it will pass the termination checker?

I've one suggestion.  The issue as it seems to me is that one should not
try to do too much all in one go, or expect too much cleverness of the termination checker.
(After all, much as we'd like one, we know that there cannot be a perfect termination checker;
so a dumb but obviously correct one is to be preferred, at least that's my opinion.)

First, consider natural numbers.  The most transparently correct way to define
equality between natural numbers is something like this (apologies for not writing
formal Agda -- it never sticks in my mind):

0 = n   =_def  case n of { 0  |-> tt ;  S m |-> ff }
S m = n =_def  case n of { 0  |-> ff ;  S k |-> m = k }

So that's a primitive recursion on the left-hand-argument, defining a
function of type Nat -> Bool.  In the second clause one defines (Sm =) in terms
of (m =).

Equality between lists of X's is a slight elaboration:

[] = xs     =_def case xs of { [] |-> tt ;  (y:ys) |-> ff }
(x:xs) = ys =_def case ys of { [] |-> ff ;  (z:zs) |-> x = z && xs = zs }

It has more-or-less the same pattern.

Since the functions are Boolean-valued, that more-or-less proves that decidability lifts.
(Yes, there's a bit more to do, but use the same pattern.)

Hank