列表中的最大元素 [英] Maximum elelment in the list
问题描述
我有一个自然数和函数（最大值）的列表，这些函数将natlist作为参数并返回nat，这在列表中是最大的。为了显示由函数最大值确定的值大于或等于列表中的任何元素，我介绍了命题，即在n l-> n <= maxvalue l中。现在想编写一个引理，如果（n ＜= maxvalue l），则maxvalue大于/等于h，h1，并且所有元素都出现在列表的尾部。请指导我如何写这个引理。
I have list of natural numbers and function (maxvalue) that takes natlist as argument and returns nat,which is greatest among all in the list. To show that value determine by function-maxvalue is greater or equal than any element in the list, I introduce Proposition i.e In n l-> n<=maxvalue l. Now want to write a lemma if (n<=maxvalue l) then maxvalue is greater /equal than h,h1 and all the elements present in the tail of list. Please guide me how to write this lemma.
推荐答案
好，您的问题有点令人困惑...
Well, your question is a little confusing...
我的第一个猜测是，您陷入定理maxValueList：在nl-> n< = maxvalue l中，一次：
My first guess is that you get stuck in the Theorem maxValueList : In n l -> n<=maxvalue l, once :
n< = maxvalue l），则maxvalue大于/等于h，h1，并且所有元素都位于列表尾部。
n<=maxvalue l) then maxvalue is greater /equal than h,h1 and all the elements present in the tail of a list.
它
例如，使用maxvalue函数：
For example, purposing a maxvalue function :
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.
您可以定义一个定理，陈述您的介词：
You can define a theorem that states your preposition :
Theorem maxValue : forall ls (H : [] <> ls) n, In n ls -> n <= maxvalue H.
只需事实，就可以证明这一点插入列表中的任何数字都遵循：
It can be proved without any big effort, just relying on the fact that any number inserted into the list obeys :
- 如果y小于x，则x被保留，因此这只是您的归纳假设（
- 如果y大于x，则y是新值，因此您将需要用ind假设重写，即新的maxvalue列表确实小于假设（substituion_ordering）
您可以在Coq库中使用可判定性（定理的解析度此处）：
You can use decidability in Coq library (the resolution of the theorems is avaliable here) :
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.
我的第二个猜测是，您严格地需要一种表达方式[我没有多少时间都没关系取消对列表的约束，则关系得以维护]。
My second guess is that you need strictly a way of saying [doesn't matter how much time I uncons a list, the relation is maintained].
某些列表的顺序任意部分或某些列表的尾部序列可以形式化为：
An sequential arbitrary part of some list, or a tail sequence of some list can be formalized as :
Definition tail_of {A} (x : list A) (t : list A) := {y | t ++ y = x}.
为简单起见，您可以定义相同的表示形式，但使用更多的归纳数据。
For the sake of simplicity, you can define the same representation but using more casual inductive data.
(* 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.
这篇关于列表中的最大元素的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
