Recursive definitions over an inductive type with nested components
What works

If you nest the definition of the fixpoint on lists inside the definition of the fixpoint on trees, the result is well-typed. This is a general principle when you have nested recursion in an inductive type, i.e. when the recursion goes through a constructor like list.

Fixpoint size (t : LTree) : nat :=
  let size_l := (fix size_l (l : list LTree) : nat :=
                  match l with
                    | nil =&gt; 0
                    | h::r =&gt; size h + size_l r
                  end) in
  match t with Node l =&gt;
    1 + size_l l
  end.


Or if you prefer to write this more tersely:

Fixpoint size (t : LTree) : nat :=
  match t with Node l =&gt;
    1 + (fix size_l (l : list LTree) : nat :=
          match l with
            | nil =&gt; 0
            | h::r =&gt; size h + size_l r
          end) l
  end.


(I have no idea who I heard it from first; this was certainly discovered independently many times.)

A general recursion predicate

More generally, you can define the “proper” induction principle on LTree manually. The automatically generated induction principle LTree_rect omits the hypothesis on the list, because the induction principle generator only understand non-nested strictly positive occurences of the inductive type. 

LTree_rect = 
fun (P : LTree -&gt; Type) (f : forall l : list LTree, P (Node l)) (l : LTree) =&gt;
match l as l0 return (P l0) with
| Node x =&gt; f x
end
     : forall P : LTree -&gt; Type,
       (forall l : list LTree, P (Node l)) -&gt; forall l : LTree, P l


Let's add the induction hypothesis on lists. To fulfill it in the recursive call, we call the list induction principle and pass it the tree induction principle on the smaller tree inside the list.

Fixpoint LTree_rect_nest (P : LTree -&gt; Type) (Q : list LTree -&gt; Type)
                         (f : forall l, Q l -&gt; P (Node l))
                         (g : Q nil) (h : forall t l, P t -&gt; Q l -&gt; Q (cons t l))
                         (t : LTree) :=
  match t as t0 return (P t0) with
    | Node l =&gt; f l (list_rect Q g (fun u r =&gt; h u r (LTree_rect_nest P Q f g h u)) l)
  end.


Why

The answer to why lies in the precise rules for accepting recursive functions. These rules are perforce subtle, because there is a delicate balance between allowing complex cases (such as this one, with nested recursion in the datatype) and unsoundness. The Coq reference manual introduces the language (the calculus of inductive constructions, which is the proof language of Coq), mostly with formally precise definitions, but if you want the exact rules regarding induction and coinduction you'll need go to the research papers, on this topic Eduardo Giménez's [1].

Starting with the Coq manual, in the notation of the Fix rule, we have the fixpoint definition of $\mathsf{Fix} f_i \, \{ f_1 : A_1 := t_1 \; ; \;\; f_2 : A_2 := t_2 \}$ where:

$$\begin{align*}
  \Gamma_1 &amp;= (x : \mathtt{LTree}) &amp;
  A_1 &amp;= \mathrm{nat} &amp;
  t_1 &amp;= \mathsf{case}(x, \mathtt{LTree}, \lambda y. g_1 (f_2 y)) \\
  \Gamma_2 &amp;= (l : \mathtt{list}\;\mathtt{LTree}) &amp;
  A_2 &amp;= \mathrm{nat} &amp;
  t_2 &amp;= \mathsf{case}(l, \mathtt{list \: LTree}, \lambda h \: r. g_2 (f_1 h) (f_2 r)) \\
\end{align*}$$

In order for the fixpoint definition to be accepted, “if $f_j$ occurs [in $t_i$] then … the argument should be syntactically recognized as structurally smaller than [the argument passed to $f_i$]” (simplifying because the functions have a single argument). Here, we need to check that 


$i=1$, $j=2$: l must be structurally smaller than t in size, ok.
$i=2$, $j=1$: h must be structurally smaller than l in size_l, looks ok but isn't!
$i=2$, $j=2$: r must be structurally smaller than l in size_l, ok.


The reason why h is not structurally smaller than l according to the Coq interpreter is not clear to me. As far as I understand from discussions on the Coq-club list [1] [2], this is a restriction in the interpreter, which could in principle be lifted, but very carefully to avoid introducing an inconsistency.

References

Cocorico, the nonterminating Coq wiki: Mutual Induction

Coq-Club mailing list:


[1] Thread “Meta theory: induction over terms with abstract variables”; first message by Robbert Krebbers on 2009-10-21; explanation by Adam Chlipala; counterexample by Bruno Barras; reply by Hugo Herbelin.
[2] Thread “Termination checking with nested recursion”; first message by Gert Smolka; reply by Hugo Herbelin.


The Coq Development Team. The Coq Proof Assistant: Reference Manual. Version 8.3 (2010). [web] ch. 4.

Eduardo Giménez. Codifying guarded definitions with recursive schemes. In Types'94: Types for Proofs and Programs, LNCS 996. Springer-Verlag, 1994. doi:10.1007/3-540-60579-7_3 [Springer]

Eduardo Giménez. Structural Recursive Definitions in Type Theory. In ICALP'98: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag, 1998. [PDF]