The Coq mailing list

[Amy Felty <afelty AT site.uottawa.ca>]

The following example is given in the Coq manual for mutually inductive
types and it is followed by the comment below:

  Coq < Variables A,B:Set.

  Coq < Inductive tree : Set :=  node : A -> forest -> tree
  Coq < with forest : Set :=
  Coq <    | leaf : B -> forest
  Coq <    | cons : tree -> forest -> forest.

  This declaration generates automatically six induction
  principles. They are respectively called tree_rec, tree_ind,
  tree_rect, forest_rec, forest_ind, forest_rect. These ones are not
  the most general ones but are just the induction principles
  corresponding to each inductive part seen as a single inductive
  definition.

It is possible to get the more general induction principles?

The reason I ask is because I have the following definition of a tree
where the label at each node is a list of integers:

Inductive Tree : Set :=
  Node : (list nat) -> (list Tree) -> Tree.

It doesn't use mutual induction, but it also does not give me an
induction principle as general as I need.  I get a warning "Ignoring
recursive call", and the induction principle Tree_ind is:

Tree_ind
     : (P:(Tree->Prop))
        ((l:(list nat); l0:(list Tree))(P (Node l l0)))->(t:Tree)(P t)

I'd like the induction principle that assumes P for each tree in l0.

Thank you in advance for any information.

Amy Felty