Library prosa.util.minmax

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Export prosa.util.notation prosa.util.nat prosa.util.list.

Additional lemmas about BigMax.

Section ExtraLemmas.

Given a function F, a predicate P, and a sequence xs, we show that F x ≤ max { F i | ∀ i ∈ xs, P i} for any x in xs.

  Lemma leq_bigmax_cond_seq :
    ∀ {X : eqType} (F : X → nat) (P : pred X) (xs : seq X) (x : X),
      x \in xs → P x → F x ≤ \max_(i <- xs | P i ) F i.

Next, we show that the fact max { F i | ∀ i ∈ xs, P i} ≤ m for some m is equivalent to the fact that ∀ x ∈ xs, P x → F x ≤ m.

  Lemma bigmax_leq_seqP :
    ∀ {X : eqType} (F : X → nat) (P : pred X) (xs : seq X) (m : nat),
      reflect (∀ x, x \in xs → P x → F x ≤ m)
              (\max_(x <- xs | P x ) F x ≤ m).

Given two functions F1 and F2, a predicate P, and sequence xs, we show that if F1 x ≤ F2 x for any x \in xs such that P x, then max of {F1 x | ∀ x ∈ xs, P x} is bounded by the max of {F2 x | ∀ x ∈ xs, P x}.

  Lemma leq_big_max :
    ∀ {X : eqType} (F1 F2 : X → nat) (P : pred X) (xs : seq X),
      (∀ x, x \in xs → P x → F1 x ≤ F2 x ) →
      \max_(x <- xs | P x ) F1 x ≤ \max_(x <- xs | P x ) F2 x.

We show that for a positive n, max of {0, …, n-1} is smaller than n.

  Lemma bigmax_ord_ltn_identity :
    ∀ (n : nat),
      n > 0 →
      \max_(i < n ) i < n.

We state the next lemma in terms of ordinals. Given a natural number n, a predicate P, and an ordinal i0 ∈ {0, …, n-1} satisfying P, we show that max {i | P i} < n. Note that the element satisfying P is needed to prove that {i | P i} is not empty.

  Lemma bigmax_ltn_ord :
    ∀ (n : nat) (P : pred nat) (i0 : 'I_n),
    P i0 →
    \max_(i < n | P i ) i < n.

Finally, we show that, given a natural number n, a predicate P, and an ordinal i0 ∈ {0, …, n-1} satisfying P, max {i | P i} < n also satisfies P.

  Lemma bigmax_pred :
    ∀ (n : nat) (P : pred nat) (i0 : 'I_n),
      P i0 →
      P (\max_(i < n | P i ) i).

End ExtraLemmas.