The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

On 20 mai 2012, at 12:55, Adam Chlipala wrote:

> S3 wrote:
>> How do you have induction over a data structure
>> that contains a list?
> 
> This is a genuine Frequently Asked Question, and it's addressed in Section 
> 3.8 of CPDT:
>    http://adam.chlipala.net/cpdt/

For those not comfortable with writing directly proof principles, 
another solution is to write a depth function and 
do proofs by strong induction over the depth of the tree (Wf_nat.lt_wf_ind).

Fixpoint depth (t:BlueTree) : nat :=
  match t with
    | BlueLeaf | RedLeaf  => O
    | Branch l => S (List.fold_right (fun x y => max  (depth x) y) O l)
  end.

--
Frédéric