The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hi Keiko,

The following definition corresponds to the predicate "eventually P" on
an infinite list of events encoded using LList:

Inductive eventually : LList nat -> Prop :=
| PHoldsHere      : forall x s, P x -> eventually (LCons x s)
| PHoldsFurhterOn : forall x s, eventually s -> eventually (LCons x s).

Naive rationale: as your predicate is inductive, it only contains proofs
built up from the application of the above constructors a finite number
of times. Therefore, you will eventually stop using PHoldsFurhterOn and
have to apply PHoldsHere, providing a proof that there is a reachable
object in the infinite list for which P holds.

You may find other examples and considerations on this kind of
definition in my PhD thesis "A Calculus of Infinite Constructions and
its application to communicating systems". Please notice that the
document is more than 10 years old and was written for the version V5.10
of Coq, but all the theoretical considerations in it should remain valid
for the current version of Coq.

Kind regards,
Eduardo.


Keiko Nakata escribió:
> 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
>