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.


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 : forall x l, In x l -> x <= lmax l.


Lemma incl_lmax : forall l1 l2, incl l1 l2 -> lmax l1 <= lmax l2.

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

Lemma lmax_in : forall l, length l > 0 -> exists x, In x l /\ lmax l = x.

min

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

Lemma in_lmin : forall x l, In x l -> lmin l <= x.