在 coq 中获取集合最小值的函数

Question

我们知道 nat 的每个子集都有一个最小数。我能够证明这样的事情：

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.

但是我如何定义一个像 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 是对的，由于可计算性问题，通常这是不可能的。然而，在命题P可判定的情况下，有可能找到这个最小值。在数学组件库具有的这一事实证明ssrnat所谓的ex_minn; 我在此处包含纯 Coq 的翻译以供参考。

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.