Set Implicit Arguments.

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

Notation nats := (list nat).

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

Lemma in_lmax : ∀ x l, In x l → x ≤ lmax l.

Proof.
induction l; simpl; intro. contradiction.
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 l2 → lmax 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 : nat ⇒ n ≤ 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.

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

Lemma in_lmin : ∀ x l, In x l → lmin l ≤ x.

Proof.
induction l; simpl; intro. contradiction.
destruct H. subst a. apply le_min_l.
ded (IHl H). apply elim_min_r. exact H0.
Qed.

Implicit Arguments in_lmin [x l].