функция, которая получает минимум множества в 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

Ли-Яо прав, что в целом это невозможно из-за проблем с вычислимостью.Однако этот минимум можно найти в случае, когда предложение 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.

Answer 2

Это невозможно.Если бы мы могли определить min_point, то мы могли бы определить любое свойство Q : Prop, определив P как P n := if n = 0 then Q else True, а H верно для n := 1.Тогда мы получим доказательство Q тогда и только тогда, когда min_point = 0, а в противном случае получим ~Q.