The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Thank you for the reply, Pierre.

> > Is it correct that:
> >
> > Suppose P is a predicate on possibly infinite lists, e.g. LList in 
> > CoqArt, 
> > and (P x) holds for some x.
> > If the definition of P only "involves" induction, 
> > then there is a finite prefix x' of x such that (P x') holds.
> >
> > Assuming it correct, what would "involves" precisely mean?
> > And how I might be able to state it in Coq?

> The problem is truely what notion of "involves" you mean.

Indeed, I want to abstract over P. That is, I want to prove something like

forall P, inductively_defined P ->
forall s, P s ->
exists s', "s' is a finite prefix of s such that P s' holds"

But I have no idea how I could define the "inductively_defined" predicate. 

I was thinking maybe there is type system support.

Kind regards,
Keiko