时间戳

首页 > 解决方案 > 列表中的最大元素

coq - 列表中的最大元素

问题描述

我有以 natlist 作为参数并返回 nat 的自然数列表和函数（最大值），这是列表中最大的。为了证明由函数最大值确定的值大于或等于列表中的任何元素，我引入了命题，即 In n l-> n<=maxvalue l。现在想写一个引理 if (n<=maxvalue l) then maxvalue 大于/等于 h,h1 以及列表尾部中存在的所有元素。请指导我如何写这个引理。

标签： coq

解决方案

嗯，你的问题有点混乱……

我的第一个猜测是你陷入了定理 maxValueList ： In nl -> n<=maxvalue l, once ：

n<=maxvalue l) 则 maxvalue 大于/等于 h,h1 以及列表尾部中存在的所有元素。

看来您正在对列表 l 进行归纳。

例如，使用最大值函数：

Definition maxvalue (ls : list nat) : [] <> ls -> nat.
intros.
destruct ls.
destruct (H (@erefl (list nat) [])).
apply : (fold_left (fun x y => if x <=? y then y else x) ls n).
Defined.

您可以定义一个陈述您的介词的定理：

Theorem maxValue : forall ls (H : [] <> ls) n, In n ls -> n <= maxvalue H.

只需依靠插入列表中的任何数字都服从这一事实，就可以毫不费力地证明这一点：

  1. 如果 y 小于 x，则保留 x，因此这只是您的归纳假设（conservation_ordering）。
  2. 如果 y 大于 x，则 y 是新值，因此您需要使用 ind 假设重写，即您的新最大值列表确实小于您的假设（substituion_ordering）。

你可以在 Coq 库中使用可判定性（定理的解析在这里可用）：

Theorem substituion_ordering : forall ls n0 n1, n1 <= n0 ->
   fold_left (fun x y : nat => if x <=? y then y else x) ls n1 <= fold_left (fun x y : nat => if x <=? y then y else x) ls n0. 
... Qed.

Theorem conservation_ordering : forall ls n0, n0 <= fold_left (fun x y : nat => if x <=? y then y else x) ls n0.
 ... Qed.

Theorem maxValue : forall ls (H : [] <> ls) n, In n ls -> n <= maxvalue H.
  intros.
  unfold maxvalue.
  induction ls.
  destruct (H (@erefl (list nat) [])).
  destruct ls.
  destruct H0.
  by subst.
  inversion H0.
  destruct H0.
  simpl; subst.
  destruct (le_lt_dec n n0).
  by rewrite (leb_correct _ _ l); rewrite -> l; apply : conservation_ordering.
  by rewrite (leb_correct_conv _ _ l); apply : conservation_ordering.
  destruct (le_lt_dec a n0).
  by simpl; rewrite (leb_correct _ _ l); apply : (IHls (@nil_cons _ n0 ls) H0).
  simpl; rewrite -> (IHls (@nil_cons _ n0 ls) H0); rewrite (leb_correct_conv _ _ l); apply : substituion_ordering.
  auto with arith.
Qed.

我的第二个猜测是，你需要一种严格的说法[不管我多久取消一个列表，关系都保持不变]。

某个列表的顺序任意部分，或某个列表的尾序列可以形式化为：

Definition tail_of {A} (x : list A) (t : list A) := {y | t ++ y = x}.

为简单起见，您可以定义相同的表示，但使用更随意的归纳数据。

 (* gets a uncons part of some list over some natural *)
Fixpoint taill {A} (x : nat) (ls : list A) : list A := 
  match x with
    |S n => match ls with
             |k :: u => taill n u
             |[] => []
            end
    |0 => ls
  end.

Require Import FunInd.
Functional Scheme taill_scheme := Induction for taill Sort Prop.

然后，只需证明：

Theorem maxValue_tail : forall ls y (H : [] <> ls) n, In n (taill y ls) -> n <= maxvalue H.
  intros.
  apply : maxValue.
  clear H; move : H0.
  pattern y, ls, (taill y ls).
  apply : taill_scheme.
  intros; assumption.
  intros; destruct H0.
  intros; simpl in *.
  set (H H0).
  by right.
Qed.

推荐阅读