Максимальный элемент в списке

Question

У меня есть список натуральных чисел и функция (maxvalue), которая принимает natlist в качестве аргумента и возвращает nat, которая является наибольшей среди всех в списке. Чтобы показать, что значение, определяемое функцией maxvalue, больше или равно любому элементу в списке, я ввожу предложение, т. Е. В n l-> n <= maxvalue l. Теперь нужно написать лемму, если (n <= maxvalue l), тогда maxvalue больше / равно h, h1 и всем элементам, присутствующим в хвосте списка. Пожалуйста, объясните мне, как написать эту лемму. </p>

Answer 1

Ну, ваш вопрос немного сбивает с толку ...

Мое первое предположение: вы застряли в теореме maxValueList: In nl -> n <= maxvalue l, один раз: </p>

n <= maxvalue l) тогда maxvalue больше / равно h, h1 и всем элементам, присутствующим в хвосте списка. </p>

Похоже, вы выполняете индукцию на список l.

Например, используя функцию maxvalue:

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 сохраняется, поэтому это просто ваша гипотеза индукции (servation_ordering).
2. если y больше x, тогда y - это новое значение, поэтому вам нужно будет переписать гипотезу ind о том, что ваш новый список maxvalue действительно меньше вашей гипотезы (substion_ordering).

Вы можете использовать разрешимость в Coq libr ary (разрешение теорем доступно здесь ):

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.