The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

roconnor AT theorem.ca
 wrote:
> Fixpoint Z (l : list (tree A)) (m:list (tree A)) : Q l m :=
> match l as l return Q l m with
> | nil => H0 m
> | cons t l0 =>
>   match m as m return Q (cons t l0) m with
>   | nil => H0' (cons t l0)
>   | cons s m0 => H1 t (tree_ind0 t) s (tree_ind0 s) l0 m0 (Z l0 m0)
>   end
> end.
>
> End Z.
>
> Fixpoint tree_ind0 (t:tree A) : P t :=
>  match t as x return P x with
>   (* Here I pass the same list twice to Z, but in my real
>      problem my "tree" type has two separate lists that
>      are processed in parallel *)
>  | node a l => H a l l (Z tree_ind0 l l)
>  end.
>
> (* This Fixpoint definition fails with the message:
>    Recursive call to tree_ind0 has principal argument equal to "s"
>    instead of one of the following variables: l l0 t0 l1.
>    *)

It's not surprising that this fails.  Even though you don't need to 
write a termination annotation in the definition of [Z], Coq infers one 
for you.  It has to pick one or the other of the two arguments.  
Whichever one it picks, the matching call to [tree_ind0] isn't 
structurally recursive.  I think this comes down to the fundamental 
limitation that [Fixpoint] needs a termination argument based on just a 
single input.  You could perhaps get around this by changing [Z] to take 
a pair as input, possibly also switching to [Function] instead of 
[Fixpoint].