The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Some tricks on this precise problem are given in
theories/Logic/ConstructiveEpsilon.v

Best regards,

Jean-Francois

On Mon, May 16, 2011 at 09:35:02AM +0200, Fabian Schmitthenner wrote:
> Hi list,
> 
> I've been playing around with coq for a while now and the following problem 
> came to me.
> 
> Consider the following:
> 
> Section MySection.
>  Variable P: nat -> Prop.
>  Axiom decP: forall n: nat, {P n}+{~P n}.
>  Axiom existsP: exists n, P n.
> 
> 
>  (* How to construct a function which gets the lowest value n, for which P 
> n 
> holds? *)
>  Definition lowest: nat.
>   (* ... ? ... *)
>  Defined.
> 
>  Lemma lowestIsRight: P lowest /\ forall n: nat, n < lowest -> ~P n.
>   (* ... *)
>  Qed.
> End MySection.
> 
> 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). 
> 
> Any help would be appreciated.
> 
> Thanks in advance.
> 
> Fabian
> 
> 

-- 
Jean-Francois Monin
LIAMA Project FORMES, CNRS  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
 +86 10 6264 7458