a function that get the minimum of a set in coq

Question

We know every subset of nat has a minimum number. I am able to proof something like this:

Variable P : nat -> Prop.
Hypothesis H : (exists n : nat , P n).

Theorem well_ordering : exists m : nat , P m /\ forall x : nat , x<m -> ~ P x.

But how i can define a function like min_point?

Variable P : nat -> Prop.
Hypothesis H : (exists n : nat , P n).

Definition min_point : nat.

Theorem min_point_def : P min_point /\ forall x : nat , x<min_point -> ~ P x. 

Answer 1

Li-yao is right that in general this is not possible because of computability issues. However, it is possible to find this minimum in the case where the proposition P is decidable. The Mathematical Components library has a proof of this fact in ssrnat called ex_minn; I am including a translation here in pure Coq for reference.

Require Import Omega.

Section Minimum.

Variable P : nat -> bool.
Hypothesis exP : exists n, P n = true.

Inductive acc_nat i : Prop :=
| AccNat0 : P i = true -> acc_nat i
| AccNatS : acc_nat (S i) -> acc_nat i.

Lemma find_ex_minn : {m | P m = true & forall n, P n = true -> n >= m}.
Proof.
assert (H1 : forall n, P n = true -> n >= 0).
{ intros n. omega. }
assert (H2 : acc_nat 0).
{ destruct exP as [n Hn].
  rewrite <- (Nat.add_0_r n) in Hn.
  revert Hn.
  generalize 0.
  induction n as [|n IHn].
  - intros j Hj. now constructor.
  - intros j. rewrite Nat.add_succ_l, <- Nat.add_succ_r; right.
    now apply IHn. }
revert H2 H1.
generalize 0.
fix find_ex_minn 2.
intros m IHm m_lb.
destruct (P m) eqn:Pm.
- now exists m.
- apply (find_ex_minn (S m)).
  + destruct IHm; trivial.
    now rewrite H in Pm.
  + intros n Pn.
    specialize (m_lb n Pn).
    assert (H : n >= S m \/ n = m) by omega.
    destruct H as [? | H]; trivial.
    congruence.
Qed.

Definition ex_minn := let (m, _, _) := find_ex_minn in m.

Lemma ex_minnP : P ex_minn = true /\ forall n, P n = true -> n >= ex_minn.
Proof.
unfold ex_minn.
destruct find_ex_minn as [m H1 H2].
auto.
Qed.

End Minimum.

Answer 2

It's not possible. If we could define min_point, then we could decide any property Q : Prop by defining P as P n := if n = 0 then Q else True, and H holds for n := 1. Then we get a proof of Q if and only if min_point = 0, and otherwise we get ~Q.