The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 21 Oct 2009, Robbert Krebbers wrote:

> Unfortunately this does not work, the system gives the following error:
>
> Error:
> Recursive definition of trm_rec2 is ill-formed
> ...
> Recursive call to avar_rec2 has principal argument equal to "a"
> instead of a subterm of t

I have a simlar problem on a more complex data structure.  Below I present 
what I hope is a simple (but silly) example that captures the problem I am 
having.

Require Import List.

Inductive tree (A:Type) :=
 node : A -> list (tree A) -> tree A.

Section Foo.

Variables (A:Type) (P : tree A -> Prop) (Q: list (tree A) -> list (tree A) 
->  Prop).

Hypotheses
 (H:forall (a:A) (l m:list (tree A)), Q l m -> P (node A a l))
 (H0: forall l, Q nil l)
 (H0': forall l, Q l nil)
 (H1: forall t, P t -> forall s, P s -> forall l m, Q l m -> Q (cons t l) 
(cons s m)).

Section Z.

Hypothesis (tree_ind0 : forall t, P t).

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.
   *)

End Foo.

Essentially I have two lists as substructures of my structure (lists that 
contain further members of my structure (my structure is simply 
s-expressions)) that are to be processed in parallel to create the output.

When passing one list, the nested recursion works fine; however to process 
two lists in parallel I do recursion on one list, and decompose the other 
list as I go.  However Coq doesn't seem to recognise that decompostion of 
the second list is a substructure.

Anyone have a solution to this type of problem?

For what it's worth, it seems that Agda can handle this case without 
difficulty.  I've attached the Agda code.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''module tree2 where

data list (A : Set) : Set where
 nil : list A
 cons : A -> list A -> list A

data tree (A : Set) : Set where
 node : A -> list (tree A) -> tree A

module Foo (A : Set)
           (P : tree A -> Set)
           (Q : list (tree A) -> list (tree A) -> Set)
           (H : (a : A) -> (l m : list (tree A)) -> Q l m -> P (node a l))
           (H0 : (l : list (tree A)) -> Q nil l)
           (H0' : (l : list (tree A)) -> Q l nil)
           (H1 : (t : tree A) -> P t -> (s : tree A) -> P s ->
                 (l m : list (tree A)) -> Q l m -> Q (cons t l) (cons s m))
           where
 mutual 
  treeInd : (t : tree A) -> P t
  treeInd (node y y') = H y y' y' (Z y' y')
 
  Z : (l m : list (tree A)) -> Q l m
  Z nil m = H0 m
  Z (cons y y') nil = H0' ((cons y y'))
  Z (cons y y') (cons y0 y1) = H1 y (treeInd y) y0 (treeInd y0) y' y1 (Z y' 
y1)