Library CoLoR.Util.Vector.VecMax

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

Set Implicit Arguments.


Notation nats := (vector nat).

max


Fixpoint Vmax n (v : nats n) : nat :=
  match v with
    | Vnil => O
    | Vcons a w => max a (Vmax w)
  end.

Lemma Vmax_in : forall x n (v : nats n), Vin x v -> x <= Vmax v.


Lemma Vmax_head : forall n (v : nats (S n)), Vhead v <= Vmax v.

Lemma Vmax_tail : forall n (v : nats (S n)), Vmax (Vtail v) <= Vmax v.

Lemma Vmax_app_cons : forall n1 (v1 : nats n1) p n2 (v2 : nats n2),
  p <= Vmax (Vapp v1 (Vcons p v2)).

Lemma Vmax_forall : forall n (v : nats n) p,
  Vmax v <= p -> Vforall (fun n => n <= p) v.


Lemma Vmax_cast : forall n (v : nats n) p (e : n=p), Vmax (Vcast v e) = Vmax v.

min


Fixpoint Vmin n (v : nats n) : nat :=
  match v with
    | Vnil => O
    | Vcons a w => min a (Vmin w)
  end.