The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

Hi,

Coq'Art, section 14.3.3, gives the following example of an inductive  
datatype for which the default induction principle is useless and for  
which the Scheme command also does not help.

(* *************** *)
Require Import List.

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

Check ltree_ind.
(*
ltree_ind
     : forall (A : Set) (P : ltree A -> Prop),
       (forall (a : A) (l : list (ltree A)), P (lnode A a l)) ->
       forall l : ltree A, P l
*)
(* *************** *)

ltree_ind overlooks the fact that the list in lnode may have ltree  
subterms that deserve induction hypotheses.  One solution to this  
problem is to build the induction principle by hand using Fixpoint.

My question is: with the release of Coq 8.1gamma, is there any  
automatic support for generating the "correct" induction principle  
for datatypes such as ltree?  Is such support being worked on?  I  
didn't see anything in the CHANGES file, but it's possible I missed  
something.

Thanks,
Brian