The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Keiko Nakata a écrit :
> 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. 
>   
Keiko,

I think that my counter-example shows that your definition of
"inductively defined" would be extremely restrictive.
It would be an inductive definition without any reference to infinite
types or terms. So (I believe that) if you can only use inductive 
definition on
finitely generalted LList, your predicate can only characterize finite 
lists.



> I was thinking maybe there is type system support.
>
> Kind 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
>