The Coq mailing list

[Peter Gammie <peteg42 AT gmail.com>]

Keiko: at the risk of exposing my almost-complete ignorance of Coq and  
providing you with a non-answer, what you are asking for sounds like a  
variant of the "take lemma" from functional programming. You can ask  
Google about it; the classical reference is Bird and Wadler's textbook  
I think, and Graham Hutton and Jeremy Gibbons have written a paper on  
a generalisation they call the approx lemma. Isabelle/HOLCF has this  
mechanised. Their foundation is domain theory.

This is assuming P is essentially an equality. As Pierre points out  
your P may inductively characterise essentially infinite objects, in  
which case I don't know what you have in mind. Richard Bird has a  
theory of prefix-closed predicates over lists, etc. - again, Google is  
your friend.

cheers
peter

On 20/01/2009, at 8:20 PM, Keiko Nakata wrote:

> Hello.
>
> At the risk of exposing my ignorance...
>
> 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?
>
> With best regards,
> Keiko
>
>
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--
http://peteg.org/