The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le lundi 16 mai 2011 à 09:35 +0200, Fabian Schmitthenner a écrit :

>  (* How to construct a function which gets the lowest value n, for which P 
> n 
> holds? *)
>  Definition lowest: nat.
>   (* ... ? ... *)
>  Defined.

> It's somehow clear from this, that the procedure of sequentially testing O, 
> S 
> O, ... until P n holds should work, but how to proof that this algorithm 
> ends 
> (which follows from existsP, but since it's in Prop, I clearly can't do a 
> destruct on it). 

Actually, you can do a destruct existP, as long as the result is used
only in Prop. And the accessibility predicate (Acc) happens to live in
Prop due to its stucture. In other words, you can define an order, which
you prove to be well-founded thanks to existsP, and then you just have
to write a fixpoint that will be inductively defined on the
corresponding accessibility predicate.

Best regards,

Guillaume