我有一个自然数和函数(最大值)的列表,这些函数将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 :
您可以在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.更多推荐
列表中的最大元素
发布评论