Coq中证明非空有限集映射后存在最小值的技术问询

Hey there! Let's work through this Coq proof problem together. Your lemma states that if the set mnnat (which represents natural numbers less than n) is non-empty, then any function from mnnat to nat must have a minimal element—this makes sense because we're dealing with finite (or more precisely, well-founded) structures.

A More Direct Proof Using Nat's Well-Foundedness #

The simplest way to prove this is to leverage the well-ordering principle of natural numbers: every non-empty subset of nat has a minimal element. Here's how to implement this in Coq:

Require Import Nat.

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).
Proof.
  intros H_nonempty.
  (* Define the image of f: all natural numbers reachable via f from mnnat *)
  Let Im f k := exists x : mnnat, f x = k.

  (* Prove the image is non-empty (follows from mnnat being non-empty) *)
  assert (Im_nonempty : exists k, Im f k).
  {
    destruct H_nonempty as [x _].
    exists (f x); exists x; reflexivity.
  }

  (* Use Nat's well-ordering principle to get the minimal element in the image *)
  assert (exists min_k, Im f min_k /\ forall m, Im f m -> min_k <= m).
  {
    apply Nat.Inf_pr; assumption. (* Nat.Inf_pr is the standard library lemma for well-ordering *)
  }

  (* Extract the minimal value and its corresponding mnnat element *)
  destruct this as [min_k [min_exists min_is_min]].
  destruct min_exists as [x_min fx_eq_min].

  (* This x_min is our desired minimal element *)
  exists x_min.
  intros y.
  apply min_is_min.
  exists y; reflexivity.
Qed.

Addressing Your f' Construction Idea #

Your idea to construct an extended function f' : nat -> nat has a small issue: the type signature you wrote has a mismatch. You mentioned wanting to prove:

exists (f' : nat -> nat), forall (x : nat) (H0: x < n), f' (exist (fun m : nat => m < n) x H0) = f x

But exist _ x H0 is of type mnnat, while f' expects a nat argument—this won't type-check. A corrected version would be to define g : nat -> nat such that g x = f (exist _ x H0) for any x < n, but even this has a problem: f can depend on the proof H0 (since mnnat elements include both the number and its proof of being less than n). For the same x, different proofs H0 and H1 could lead to different f values, so you can't guarantee g x equals f (exist _ x H1) for all proofs H1.

This means your original construction approach isn't feasible unless you restrict f to only depend on the numeric part of mnnat elements (i.e., f (exist x H0) = f (exist x H1) for any H0, H1 : x < n).

Solving Your Current Subgoal #

If you want to stick to inductive reasoning instead of using well-ordering, you can perform induction on n:

1. Base case: n = 1—there's only one element in mnnat (exist _ 0 (lt_0_S 0)), which trivially is the minimum.
2. Inductive step: Assume the lemma holds for n = k. For n = k+1, split mnnat into elements less than k and the element k. Use the inductive hypothesis to get the minimum of the smaller set, then compare it with f (exist _ k (lt_Sn_Sm k (lt_n_Sn k))) to find the global minimum.

Here's a sketch of this approach:

Proof.
  intros H_nonempty.
  destruct H_nonempty as [x _].
  destruct n.
  - inversion x. (* n=0 is impossible since x < 0 can't hold *)
  - induction k as [|k IH].
    + (* n=1, k=0 *)
      exists 0, (lt_0_S 0).
      intros y0 H1. inversion H1; reflexivity.
    + (* n = S (S k) *)
      pose (f_k := f (exist (fun m => m < S (S k)) (S k) (lt_Sn_Sm k (lt_n_Sn k)))).
      (* Use inductive hypothesis on n = S k *)
      assert (exists y (H0 : y < S k), forall y0 (H1 : y0 < S k),
              f (exist (fun m => m < S (S k)) y (lt_trans H0 (lt_n_Sn (S k)))) <=
              f (exist (fun m => m < S (S k)) y0 (lt_trans H1 (lt_n_Sn (S k))))).
      {
        apply IH; exists (exist (fun m => m < S k) 0 (lt_0_S k)); trivial.
      }
      destruct this as [y H0 y_min].
      (* Compare the minimum of the smaller set with f_k *)
      destruct (le_lt_dec (f (exist _ y (lt_trans H0 (lt_n_Sn (S k))))) f_k) as [Hle | Hlt].
      * exists y, (lt_trans H0 (lt_n_Sn (S k))).
        intros y0 H1.
        destruct (lt_eq_lt_dec y0 (S k)) as [y0_lt | [y0_eq | y0_gt]].
        - apply y_min; apply lt_trans with (m := S k); assumption.
        - rewrite y0_eq; apply Hle.
        - inversion H1. (* y0 > S k contradicts y0 < S (S k) *)
      * exists (S k), (lt_Sn_Sm k (lt_n_Sn k)).
        intros y0 H1.
        destruct (lt_eq_lt_dec y0 (S k)) as [y0_lt | [y0_eq | y0_gt]].
        - assert (f (exist _ y0 (lt_trans H1 (lt_n_Sn (S k)))) >= f (exist _ y (lt_trans H0 (lt_n_Sn (S k))))).
          { apply y_min; apply lt_trans with (m := S k); assumption. }
          omega. (* Uses Hlt to get f_k <= f y0 *)
        - rewrite y0_eq; reflexivity.
        - inversion H1.
Qed.

内容的提问来源于stack exchange，提问作者Alexander Boll