COQ-证明非空序列中存在最大元素

Question

作为一种练习，我想证明，在非空序列中始终存在最大元素。

Theorem largest_el_in_list (s: seq rat) x : x \in s -> exists y, y \in s /\ forall z, z \in s -> y >= z.

我的想法是通过归纳对S进行归纳，然后破坏X。在第一种情况下，最大的元素是列表中唯一的元素。但是，在第二种情况下，我感到非常困惑。我应该使用归纳假设吗？我的想法是，我们可以通过存在Max A A1来摆脱存在性，其中A是我们在上一步中发现的最大元素，而A1是正在添加到序列中的新元素。但是，如果我这样做，那么我将无法使用归纳假设，并且完全卡住了。

我已经呆了几个小时，很想知道我有正确的主意。

编辑： 这是到目前为止的证明，下面有当前的证明状态：

Theorem largest_el_in_list (s: seq rat) x : x \in s -> exists y, y \in s /\ forall z, z \in s -> y >= z.
Proof.
  elim/last_ind : s => //= s x0 IH x_in_rcons.
  case : s IH x_in_rcons.
  move => _ x_in_sx0.
  exists x0. split.
  rewrite in_cons. apply/orP. left. by apply/eqP.
  rewrite in_cons in x_in_sx0. case/orP : x_in_sx0 => //= xeqx0 z z_in_sx0.
  rewrite in_cons in z_in_sx0. case/orP : z_in_sx0 => //= zeqx0. case/eqP : zeqx0 => zeqx0.
  by rewrite zeqx0.
  move => a l IH x_in_rcons. 
  exists (maxr x0 a). split.
  have [agex0 | x0gta] := (lerP x0 a).
  by rewrite mem_head.
  rewrite rcons_cons in_cons. apply/orP. right. by rewrite in_rcons.
  move => z z_in_rcons.
Admitted.

证明状态：

x: rat_eqType
x0, a: rat
l: seq rat
IH: x \in a :: l ->
     exists y : rat, y \in a :: l /\ (forall z : rat, z \in a :: l -> z <= y)
x_in_rcons: x \in rcons (a :: l) x0
z: rat
z_in_rcons: z \in rcons (a :: l) x0
-------------------------------
(1/1)
z <= maxr x0 a

另一个编辑：

导入：

From finprob Require Import prob.
From mathcomp Require Import all_ssreflect all_algebra seq.
From extructures Require Import ord fset fmap ffun.
Import Num.Theory.
Import GRing. 
Import Bool. 
Import Num.Def.

您可以在此处找到挤压 https://github.com/arthuraa/extructures and Finprob在这里 https://github.com/arthuraa/finprob

---

：

尽管更改定义可以清除路径，但仍然存在问题。这是更新的证明和证明状态：

Theorem largest_el_in_list (s: seq rat) : s != [::] -> exists y, y \in s /\ forall z, z \in s -> y >= z.
Proof.
  elim/last_ind : s => //= s x0 IH x_in_rcons.
  case : s IH x_in_rcons.
  move => _ x_in_sx0.
  exists x0. split.
  rewrite in_cons. apply/orP. left. by apply/eqP.

  move => z z_in_cons.
  rewrite in_cons in z_in_cons.
  case/orP : z_in_cons => //= zeqx0.
  case/eqP : zeqx0 => zeqx0. by rewrite zeqx0.
  
  move => a l IH cons_nempty.
  case IH => //= x [x_in_cons IH'].
  exists x.
  split.
  rewrite in_cons in x_in_cons.
  rewrite in_cons. 
  case/orP : x_in_cons => [xeqa | x_in_l].
  by rewrite xeqa orTb. apply/orP. right. rewrite in_rcons. apply/orP. by right.
  move => z z_in_cons.
  apply IH'.
  rewrite in_cons. rewrite in_cons in z_in_cons.
  case/orP : z_in_cons => [zeqa | z_in_cons].
  by rewrite zeqa orTb.
Admitted.

x0, a: rat
l: seq rat
IH: a :: l != [::] ->
     exists y : rat, y \in a :: l /\ (forall z : rat, z \in a :: l -> z <= y)
cons_nempty: rcons (a :: l) x0 != [::]
x: rat
x_in_cons: x \in a :: l
IH': forall z : rat, z \in a :: l -> z <= x
z: rat
z_in_cons: z \in rcons l x0
-------------------------
(1/1)
(z == a) || (z \in l)

我看不出这是如何真实的，因为我们从z_in_cons知道z要么等于x0，要么在l中。因此，如果我们通过案例，第一种情况是不可能的，因为我们缺少有关X0的一些信息。

Answer 1

另一种方法是从一开始就明确提供y的值，即您正在寻找的值。这应该是列表的最大值，您可以通过fixpoint定义来指定自己，或者是COQ中定义的最大值。

但是，如果您想在评论中提出的那样，如果您想通过归纳来保留证明，这是一种方法（我想可以更简洁的方式编写它）。我在这里使用nat而不是rat，为方便起见：

Theorem largest_el_in_list (s: seq nat) : 
  s != [::] -> exists y, y \in s /\ forall z, z \in s -> y >= z.
Proof.
elim: s => [//=|n s IH _].
have [/eqP ->|/IH [max [maxins ismax]]] := boolP (s == nil).
- exists n.
  split=> [|y]; first by rewrite in_cons eq_refl orTb.
  by rewrite in_cons ?in_nil => /orP [/eqP ->|].
- have [lenx|] := boolP (n <= max).
  - exists max. 
    split=> [|z]; first by rewrite in_cons maxins orbT.
    by rewrite in_cons => /orP [/eqP ->|/ismax]. 
  - rewrite -ltnNge.
    exists n.
    split=> [|z]; first by rewrite in_cons eq_refl orTb.
    rewrite in_cons => /orP [/eqP -> //|/ismax ltzx].
    by rewrite (@leq_trans max) // ltnW.
Qed.

Answer 2

问题可能来自变量x。

一个可能的解决方法是拥有X普遍量化的，例如，使用移动：X（在s上进行启动之前）。

另一个解决方案是删除x，它在您的语句中仅出现一次，并使子目标难以读取并证明：

Theorem largest_el_in_list (s: seq rat)  : s <> nil  ->
          exists y, y \in s /\ forall z, z \in s -> y >= z.