The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 12 Oct 2010, Stéphane Lescuyer wrote:

> > I need to use a theorem like this:
> > Lemma nat_well_ordered: forall (P:nat -> Prop),
> >  (exists n:nat, P n) -> (exists m:nat, P m /\
> >    forall k:nat, P k -> k >= m).
>
> Consider the fact that Coq's logic is intuitionistic, and try to think
> of this theorem of yours in a constructive manner. If you're given an
> n for which P is true, then how are you gonna compute the smallest k
> for which P is true?
> Indeed, you need to be able to decide if P is true on a given m to
> write such a function.  This is why you need the decidability of P to
> prove this theorem.
>
> If you're not interested in constructive logic, just assume the
> excluded middle and using it you can use prove your theorem by a
> simple induction on n.

Or alternatively you can avoid using axioms and instead use the weak 
(classical) existential:

Definition existsW (A:Type) (B : A -> Prop) : Prop := ~(forall x:A, ~ B x)

Lemma nat_well_ordered: forall (P:nat -> Prop),
  (forall n, ~~P n -> P n) ->
  (existsW P) -> existsW (fun m:nat => P m /\
   forall k:nat, P k -> k >= m).

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''