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

[Brent Yorgey]

On Thu, Jun 19, 2014 at 11:01:53PM +0100, Peter Hancock wrote:
> 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.)

It seems to me that is essentially the pattern already being used by
the code I linked.  Of course it is not exactly the same but I am not
sure which of the various differences you might have in mind as the
essential one.

-Brent