非空有限集中的最小值

Question

用下面的定义我想证明引理without_P

Variable n : nat.
Definition mnnat := {m : nat | m < n}.
Variable f : mnnat -> nat.

Lemma without_P : (exists x : mnnat, True) -> (exists x, forall y, f x <= f y).

引理without_P的意思是：如果你知道（有限）集mnnat不为空，那么mnnat中一定存在一个元素，它是所有元素中最小的, 在将 f 映射到 mnnat.
之后我们知道 mnnat 是有限的，因为其中有 n-1 个数字，并且在证明 without_P 的上下文中我们也知道 mnnat 不是空的，因为前提(exists x : mnnat, True).
现在 mnnat 是非空的并且有限 "naturally/intuitively" 有一些最小的元素（在其所有元素上应用 f 之后）。

目前我被困在下面的点上，我想在 n 上进行归纳，这是不允许的。

1 subgoal  
n : nat  
f : mnnat -> nat  
x : nat  
H' : x < n  
______________________________________(1/1)  

exists (y : nat) (H0 : y < n),
  forall (y0 : nat) (H1 : y0 < n),
  f (exist (fun m : nat => m < n) y H0) <= f (exist (fun m : nat => m < n) y0 H1)

我这里唯一的想法是像这样断言函数 f' : nat -> nat 的存在：exists (f' : nat -> nat), forall (x : nat) (H0: x < n), f' (exist (fun m : nat => m < n) x H0) = f x，在解决这个断言之后，我通过对 n 的归纳法证明了引理。 我如何证明这个论断？

有没有办法更直接地证明"non-empty, finite sets (after applying f to each element) have a minimum"？我目前的道路似乎对我的 Coq 技能来说太难了。

Answer 1

Require Import Psatz Arith.  (* use lia to solve the linear integer arithmetic. *)

Variable f : nat -> nat.

下面这基本上是您的目标，将语句模打包为某种依赖类型。（它没有说 mi < n，但您可以扩展证明语句以也包含它。）

Goal forall n, exists mi, forall i, i < n -> f mi <= f i.

  induction n; intros.
  - now exists 0; inversion 1. (* n cant be zero *)
  - destruct IHn as [mi IHn].  (* get the smallest pos mi, which is < n *)
    (* Is f mi still smallest, or is f n the smallest? *)    
    (* If f mi < f n then mi is the position of the 
       smallest value, otherwise n is that position,
       so consider those two cases. *)
    destruct (lt_dec (f mi) (f n));
      [ exists mi |  exists n];
      intros.

    + destruct (eq_nat_dec i n).
      subst; lia.
      apply IHn; lia.

    + destruct (eq_nat_dec i n).
      subst; lia.
      apply le_trans with(f mi).
      lia.
      apply IHn.
      lia.
Qed.

Answer 2

您的问题是更一般结果的一个特定实例，该结果已在 math-comp 中得到证明。在那里，你甚至有一个表示 "the minimal x such that it meets P" 的符号，其中 P 必须是一个可判定的谓词。

无需过多调整您的陈述，我们得到：

From mathcomp Require Import all_ssreflect.

Variable n : nat.
Variable f : 'I_n.+1 -> nat.

Lemma without_P : exists x, forall y, f x <= f y.
Proof.
have/(_ ord0)[] := arg_minP (P:=xpredT) f erefl => i _ P.
by exists i => ?; apply/P.
Qed.

Answer 3

我通过用引理 f'exists 证明了类似的断言 (exists (f' : nat -> nat), forall x : mnnat, f x = f' (proj1_sig x)). 找到了我的断言 (exists (f' : nat -> nat), forall (x : nat) (H0: x < n), f (exist (fun m : nat => m < n) x H0) = f' x). 的证明。然后第一个断言几乎是微不足道的。
在我证明了这个断言之后，我可以对用户 larsr 做一个类似的证明，来证明 Lemma without_P。

除了 n = 0 的基本情况外，我使用 mod 函数将任何 nat 转换为比 n 更小的 nat。

Lemma mod_mnnat : forall m,
  n > 0 -> m mod n < n.
Proof.
  intros.
  apply PeanoNat.Nat.mod_upper_bound.
  intuition.
Qed.

Lemma mod_mnnat' : forall m,
  m < n -> m mod n = m.
Proof.
  intros.
  apply PeanoNat.Nat.mod_small.
  auto.
Qed.

Lemma f_proj1_sig : forall x y,
  proj1_sig x = proj1_sig y -> f x = f y.
Proof.
  intros.
  rewrite (sig_eta x).
  rewrite (sig_eta y).
  destruct x. destruct y as [y H0].
  simpl in *.
  subst.
  assert (l = H0).
  apply proof_irrelevance. (* This was tricky to find. 
    It means two proofs of the same thing are equal themselves. 
    This makes (exist a b c) (exist a b d) equal, 
    if c and d prove the same thing. *)
  subst.
  intuition.
Qed.


(* Main Lemma *)
Lemma f'exists :
  exists (ff : nat -> nat), forall x : mnnat, f x = ff (proj1_sig x).
Proof.
  assert (n = 0 \/ n > 0).
  induction n.
  auto.
  intuition.
  destruct H.
  exists (fun m : nat => m).
  intuition. destruct x. assert (l' := l). rewrite H in l'. inversion l'.
  unfold mnnat in *.

  (* I am using the mod-function to map (m : nat) -> {m | m < n} *)
  exists (fun m : nat => f (exist (ltn n) (m mod n) (mod_mnnat m H))).
  intros.
  destruct x.
  simpl.
  unfold ltn.
  assert (l' := l).
  apply mod_mnnat' in l'.

  assert (proj1_sig (exist (fun m : nat => m < n) x l) = proj1_sig (exist (fun m : nat => m < n) (x mod n) (mod_mnnat x H))).
  simpl. rewrite l'.
  auto.
  apply f_proj1_sig in H0.
  auto.
Qed.

非空有限集中的最小值

Minimum in non-empty, finite set

minimum

coq