The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael Shulman wrote:
> The following code (a simplification) defines a family of list types
> indexed by the natural numbers (the index has nothing to do with the
> length of the list or anything else).  My attempt to define a function
> which decrements the list index is refused by the termination checker.
> Why is it confused, and what can I do to persuade it that the function
> does terminate?
>    

Nested patterns (like [mycons (S n) x xs']) don't add all of the type 
equalities you would expect.  A small change gets around this by 
unnesting the pattern explicitly.  It's also helpful to take the 
generalized type you put in a [return] annotation and make that the 
official type of the recursive function.

  Fixpoint declabel (n:nat) (xs : mylist n) : mylist (pred n) :=
    match xs with
      | mynil _ => mynil _
      | mycons n x xs' =>
        match n return mylist (pred n) -> mylist (pred n) with
          | O => fun _ => mynil _
          | S n' => mycons x
        end (declabel xs')
    end.

  Definition declabel' n (xs : mylist (S n)) : mylist n := declabel xs.