当前位置：文江博客话题详情

列表的最大值

发布于 2025-02-13 12:45:24 字数 123 浏览 1 评论 0原文

我有自然数列表，其最大值不是零。我也有反对陈述，索引nth kl 0的值大于最大值。我如何证明这个错误的语句？因为列表中存在的所有值都小于最大值（对于所有NL，N＆LT; = List Max LT; = list Max l ）。

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

人事已非 2025-02-20 12:45:24

确实有点复杂。代码中的搜索命令向您显示如何找到所需的引理。

Require Import List NArith.
Require Import Lia.

Example listmax: forall (l : list nat) (k : nat),
  nth k l 0 > list_max l ->  False.
Proof.
  intros l k C.
  Search list_max.
  pose proof list_max_le l (list_max l) as H.
  (* discard <- direction in H *)
  destruct H as [H _].
  specialize (H ltac:(lia)).
  Search "Forall" "nth".
  rewrite Forall_nth in H.
  specialize (H k 0).
  Search "_ < _" "dec".
  destruct (PeanoNat.Nat.lt_decidable k (length l)) as [Hlt|Hnlt].
  - lia.
  - Search (nth _ _ ?s = ?s).
    rewrite nth_overflow in C by lia.
    lia.
Qed.

如您所见，您甚至不需要列表的最大值大于0的前提。

It is indeed a bit intricate. The Search commands in the code show you how to find the required lemmas.

Require Import List NArith.
Require Import Lia.

Example listmax: forall (l : list nat) (k : nat),
  nth k l 0 > list_max l ->  False.
Proof.
  intros l k C.
  Search list_max.
  pose proof list_max_le l (list_max l) as H.
  (* discard <- direction in H *)
  destruct H as [H _].
  specialize (H ltac:(lia)).
  Search "Forall" "nth".
  rewrite Forall_nth in H.
  specialize (H k 0).
  Search "_ < _" "dec".
  destruct (PeanoNat.Nat.lt_decidable k (length l)) as [Hlt|Hnlt].
  - lia.
  - Search (nth _ _ ?s = ?s).
    rewrite nth_overflow in C by lia.
    lia.
Qed.

As you see you don't even need the premise that the max of your list is larger than 0.

回复收藏 0 原文

溺ぐ爱和你が 2025-02-20 12:45:24

您也可以尝试应用置换以证明更“直接”的属性。

这是一个使用（有限）元组的变体，而不是具有MathComp的列表，以给出一个想法：

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo n m (l : n.-tuple 'I_m) k : tnth l k > \max_i tnth l i -> false.
Proof.
apply: contraTT => _.
rewrite -leqNgt. 
exact: leq_bigmax.
Qed.

You could also try to apply contraposition to prove a more "direct" property.

Here is a variant using (finite) tuples instead of lists with mathcomp, to give an idea:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo n m (l : n.-tuple 'I_m) k : tnth l k > \max_i tnth l i -> false.
Proof.
apply: contraTT => _.
rewrite -leqNgt. 
exact: leq_bigmax.
Qed.

回复收藏 0 原文

~没有更多了~