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.
  (A : Set)(P : ltree A -> Prop)(Q : list (ltree A)-> Prop).

 (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 correct_ltree_ind.

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


Look at this file

Going home
Pierre Castéran