The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

I suspect that your question is related to continuity.

Streams over A are (extensionally) isomorphic to (Nat -> Nat). Any  
function of type (Nat -> Nat) -> Nat can only access a finite segment  
of its input. This is known as "local continuity" or formally

forall f:Nat -> Nat, exists n:Nat, forall g,h : Nat, -> Nat,(forall  
i:Nat,i < n -> g i = h i) -> f g = f h

This is is not provable in Coq but it could be added as an axiom.

Cheers,
Thorsten

On 20 Jan 2009, at 04:20, 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


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.