The Coq mailing list

[Fabian Schmitthenner <fabian1024 AT googlemail.com>]

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