The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Christian Doczkal wrote:
> I have the following setup (which follows no intuition but is a
> simplified version of the original inductive type reproducing the
> effect)
>
> Section T.
> Variables (X: Type) (x:X) (A : X ->  Prop) (f : forall (x:X), A x ->  X ->  
> X).
>
> Inductive AllList X  (P : X ->  Prop) : list X ->  Prop :=
>    empty : AllList _ P nil
> | acons : forall x xs , P x ->  AllList _ P xs ->  AllList _ P (x::xs).
>
> Inductive R : X ->  Prop :=
> | intro0 : forall x x' a , R (f x a x') ->  R x'
> | intro1 : forall xs x', AllList _ (fun x =>  { a : A x | R (f x a x')} ) xs 
> ->  R x'
> | intro2 : R x.
>
> On entering R i get: "Warning: Ignoring recursive call"
>
> 1. Question: What does this warning mean and does it have any
> consequences on the consistency of the system?
>    

The warning is just about the heuristic attempts to generate a useful 
induction principle.  Nested inductive types (like your [AllList] use 
here) call for some cleverness to build the right inductive case schemas.

> If I remove either intro0 or intro1 (intro2 is just added to not make it
> a single constructor inductive proposition) the warning disappears.
>
> 2. Question: The above shows that being well-formed (in the sense of no
> warnings being issued) is not a property that can be verified in a
> rule-by-rule fashion. Can someone explain this?

Since Coq ignores nested inductive types in generating induction 
principles, it interprets "R minus intro0" as a non-recursive type.  
Therefore, the "induction principle" is not recursive, so there is no 
recursive call to ignore.  Just removing "intro1" leads to a 
nesting-free type, for which the most natural induction principle is 
easily generated.

In case you decide you want a nice induction principle for [R], you 
might be interested in Section 3.7 of CPDT:
    http://adam.chlipala.net/cpdt/