The Coq mailing list

[Benjamin GREGOIRE <Benjamin.Gregoire AT inria.fr>]

Amy Felty wrote:

> 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.
Try this:

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

Inductive forall [P:Tree->Prop] : (list Tree) -> Prop :=
 | FA_n : (forall P (nil ?))
 | FA_c : (t:Tree) (P t) ->
        (l:(list Tree))(forall P l) -> (forall P (cons t l)).

Lemma Tree_ind2:
   (P:(Tree->Prop))
       ((l:(list nat); l0:(list Tree))(forall P l0) ->
     (P (Node l l0)))->(t:Tree)(P t).
Intros P H.
Fix 1.
Intros t; Case t.
Intros.
Apply H.
Elim l0.
Constructor.

Intros; Constructor.
Apply Tree_ind2.

Trivial.
Qed.

Then you can use Tree_ind2 as follow:
Elim t using Tree_ind2.

Benjamin Gregoire