# Library CoLoR.Util.List.ListMax

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2007-01-22
• Sebastien Hinderer, 2004-04-02
greatest/smallest component of a list of natural numbers

Set Implicit Arguments.

Require Import ListUtil.
Require Import Max.
Require Import Min.
Require Import LogicUtil.
Require Import NatUtil.

Notation nats := (list nat).

max

Fixpoint lmax (l : nats) : nat :=
match l with
| nil ⇒ 0
| a :: l'max a (lmax l')
end.

Lemma in_lmax : x l, In x lx lmax l.

Proof.
destruct H. subst a. apply le_max_l.
ded (IHl H). apply le_max_intro_r. exact H0.
Qed.

Implicit Arguments in_lmax [x l].

Lemma incl_lmax : l1 l2, incl l1 l2lmax l1 lmax l2.

Proof.
intros l1 l2. induction l1 as [| a' l' Hrec].
auto with arith.
intro H. generalize (incl_cons_l H). clear H. intros (H1, H2). simpl.
apply (max_case2 a' (lmax l') (fun n : natn lmax l2)).
apply in_lmax. assumption.
apply Hrec. assumption.
Qed.

Lemma lmax_app : l m, lmax (l ++ m) = max (lmax l) (lmax m).

Proof.
intros. induction l as [| a l Hrec].
auto.
simpl. rewrite Hrec. rewrite max_assoc. reflexivity.
Qed.

Lemma lmax_in : l, length l > 0 → x, In x l lmax l = x.

Proof.
induction l; simpl; intros. contradict H; omega. destruct l.
a. intuition. set (l' := n::l) in ×. assert (length l'>0). simpl. omega.
ded (IHl H0). do 2 destruct H1. case (max_dec a (lmax l')); intro.
a. intuition. x. intuition.
Qed.

min

Fixpoint lmin (l : nats) : nat :=
match l with
| nil ⇒ 0
| a :: l'min a (lmin l')
end.

Lemma in_lmin : x l, In x llmin l x.

Proof.