Минимум в непустом, конечном множестве

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 непуста и конечна «естественно / интуитивно» имеет некоторый наименьший элемент (после применения 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. Как я могу доказать это утверждение?

Есть ли способ доказать, что "непустые конечные множества (после применения f к каждому элементу) имеют минимум" большенапрямую? Мой текущий путь кажется слишком сложным для моих навыков Coq.

Answer 1

Ваша проблема является конкретным примером более общего результата, который доказан, например, в математике.Там у вас даже есть обозначение для обозначения «минимального x, такого, что оно соответствует 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 2

Я нашел доказательство моего утверждения (exists (f' : nat -> nat), forall (x : nat) (H0: x < n), f (exist (fun m : nat => m < n) x H0) = f' x)., доказав аналогичное утверждение (exists (f' : nat -> nat), forall x : mnnat, f x = f' (proj1_sig x)). с помощью леммы f'exists.Первое утверждение следует почти тривиально.
После того, как я доказал это утверждение, я могу сделать аналогичное доказательство для пользователя larsr, чтобы доказать лемму without_P.

Я использовал mod -функцию для преобразования любого nat в nat меньше n, кроме базового случая n = 0.

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.

Answer 3

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

Variable f : nat -> nat.

Это, по сути, ваша цель, по модулю упаковка оператора в некоторый зависимый тип.(Это не говорит о том, что mi <n, но вы можете расширить выражение доказательства, чтобы оно также содержало это.)