# haskell - Structural induction for multi-way (rose) trees

Since multi-way trees can be defined as a recursive type:

``data RoseTree a = Node {leaf :: a, subTrees :: [RoseTree a]}``

is there a corresponding principle for performing structural induction on this type?

To state that property `P` holds for all (*) rose trees, you have to prove that

• if `l :: [RoseTree]` is a list of rose trees whose elements satisfy `P`, and `x :: a` is arbitrary, then `Note x l` satisfies `P`

The part about `P` holding on the elements of `l` is the induction hypothesis, which you can use to prove `P(Node x l)`.

There is no explicit base case here: this is because there's no explicit base case constructor. Yet, `Node x []` acts as an implicit base case for the trees, and indeed when `l` is empty we get a base case for induction implicitly. Concretely, the hypothesis "all the elements of `l` satisfy `P`" becomes vacuously true when `l` is empty, so we get `P(Node x [])` from the induction principle above.

(*) More precisely, this principle proves `P` for every finite-depth rose tree. If you really have to consider infinite-depth ones (e.g. circular trees), you need coinduction.