The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

This definition is correct but not well supported by Coq, this is why
we encourage people to use the alternative equivalent mutual inductive
definition.

When defining an inductive definition X then X should occur positively
in the arguments of its constructors, which means that this argument
can be of the form (J t1 .. tk) with J another inductive type
with parameters such that X occurs positively in the types of the
arguments of the constructors of J when instantiated with the
parameters t1 .. tn.
For instance X is positive in X/\A X+A but also (list X)...
The point is that the automatically generated induction scheme do not
perform induction inside these types 
(this is why you get the message 
> Warning: Ignoring recursive call)
In your case tree_ind performs pattern-matching but not recursion.
In the case J is not an inductive type (it is a product, sum, ..)
Then you can yourself derive the apropriate induction principal

But in case of a recursive inductive definition (like yours with (list
tree)) then the checking of guard condition for fixpoints 
is too weak and you will not be able to do the proof you expect ..

So I strongly recommend you to introduce a mutual inductive definition
tree with ltree
the it should be able to prove the isomorphism between ltree and (list
tree) and derive powerful induction principles, while keeping the
possibility to use predefined notions on lists.

Hope it helps,
Christine Paulin.


In his message of Thu May 28, 1998, Cuihtlauac ALVARADO writes: 
> Hello,
> 
> We, at Bordeaux, are a bit surprized by the following session :
> 
> Welcome to Coq V6.2 (January 1998)
> 
> Coq < Require PolyList.  
> [Reinterning PolyList ...done]
> [Reinterning Le ...done]
> 
> Coq < Inductive tree : Set :=
> Coq < leaf : tree
> Coq < | root : (list tree)->tree.
> Warning: Ignoring recursive call
> tree_ind is defined
> tree_rec is defined
> tree_rect is defined
> tree is defined
> 
> First, I would have expected (following Coq's RM, p76) something like :
> 
> Error: Non positive Occurrence in (list tree)->tree
> 
> But P. Casteran pointed me that this definition of trees might be seen
> as well-founded (and it must be, it's ok).
> 
> So, what ? :)
>       
> What is the difference between this definition and the classical one
> (with mutual inductive types).
> 
> What is the exact meaning of the warning ?
> 
> What should I expect of an object of such a type ?
> 
> how/why/when should I prefer to choose such a definition instead of the
> mutual inductive one ?
> 
> Best regards,
> 
> -- 
> Cuihtlauac ALVARADO
-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 55 70       fax : (+33) (0)1 39 63 56 84
  Tatoo tel : 06 04 24 44 75 
   message numerique +1(pas urgent)-3(tres urgent) ou * + message vocal