coq - Maximum elelment in the list

Question

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.

Answer 1

Well, your question is a little confusing...

My first guess is that you get stuck in the Theorem maxValueList : In n l -> n<=maxvalue l, once :

n<=maxvalue l) then maxvalue is greater /equal than h,h1 and all the elements present in the tail of a list.

It seems that you're doing induction on list l.

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 :

1. if y is less than x, then x is preserved, therefore it's just your induction hypothesis (conservation_ordering).
2. if y is bigger than x, then y is the new value, so you will need rewrite with ind hypothesis that your new maxvalue list is indeed less than your hypothesis (substituion_ordering).

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.

Then, just prove :

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.