The Coq mailing list

["Eelis van der Weegen" <coq-club AT contacts.eelis.net>]

Greetings. Given the following inductive definition:

  Inductive Tree (A: Set): Set :=
    | Leaf: A -> Tree A
    | Node: list (Tree A) -> Tree A.

Coq rejects the following:

  Fixpoint f A (l: list (Tree A)): unit :=
    match l with
    | Node x :: y => f A x
    | _ => tt
    end.
      (* error: Recursive call to f has principal argument equal to "x"
instead of y *)

First question: Since x is obviously a subterm of l, should Coq not easily be
able to conclude that the recursive call is safe? If not, is there some
theoretical limitation here?

The following workaround works:

  Inductive Tree (A: Set): Set :=
    | Leaf: A -> Tree A
    | Node: MyList A -> Tree A
  with MyList (A: Set): Set :=
    | Nil
    | Cons: Tree A -> MyList A -> MyList A.

  Fixpoint f A (l: MyList (Tree A)): unit :=
    match l with
    | Cons (Node x) y => f A x
    | _ => tt
    end.
      (* Ok. *)

Second question: Is there a less annoying workaround that doesn't require me
to duplicate lots of existing functions and theorems operating on lists?

Regards,

Eelis

P.S. In the above, f is obviously a silly function. However, this is only an
isolated testcase; in my actual development I'm trying to define a monadic
bind operation for Tree.