# A correct induction principle for lists of trees

We define a type of trees based on lists of trees. In this type, an
node can have an arbitrary (but finite) number of children, grouped in a list.

Inductive ltree (A:Set) : Set :=
lnode : A -> list (ltree A)-> ltree A.

For this type, the induction principles that are generated by default or
by the `Scheme` command are un suitable, but we can construct a
suitable with the following script.

Section correct_ltree_ind.
Variables
(A : Set)(P : ltree A -> Prop)(Q : list (ltree A)-> Prop).
Hypotheses
(H : forall (a:A)(l:list (ltree A)), Q l -> P (lnode A a l))
(H0 : Q nil)
(H1 : forall t:ltree A, P t ->
forall l:list (ltree A), Q l -> Q (cons t l)).
Fixpoint ltree_ind2 (t:ltree A) : P t :=
match t as x return P x with
| lnode a l =>
H a l
(((fix l_ind (l':list (ltree A)) : Q l' :=
match l' as x return Q x with
| nil => H0
| cons t1 tl => H1 t1 (ltree_ind2 t1) tl (l_ind tl)
end)) l)
end.
End correct_ltree_ind.

Prove a suitable induction principle for lists of trees of
type `ltree A`.

## Solution

Look at this file

Going home

Pierre Castéran