# 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.

Require Export prosa.util.notation prosa.util.nat prosa.util.list.

Additional lemmas about BigMax.

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.

∀ {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).

∀ {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.

∀ {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 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.
Next, 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.

Furthermore, we observe that, if there is any element that satisfies the
predicate, then there exists a witness for the computed maximum.

Lemma bigmax_witness {T : eqType} :

∀ {xs : seq T} {P} F,

has P xs →

∃ x, x \in xs ∧ P x ∧ (F x = \max_(x <- xs | P x) F x).

∀ {xs : seq T} {P} F,

has P xs →

∃ x, x \in xs ∧ P x ∧ (F x = \max_(x <- xs | P x) F x).

Additionally, we observe that, if two predicates yield different maxima,
then there must exist a witness that satisfies only one of the
predicates.

Lemma bigmax_witness_diff {T : eqType} :

∀ {xs : seq T} {P1 P2 F},

\max_(x <- xs | P1 x) F x < \max_(x <- xs | P2 x) F x →

∃ x, x \in xs ∧ ~~ P1 x ∧ P2 x.

∀ {xs : seq T} {P1 P2 F},

\max_(x <- xs | P1 x) F x < \max_(x <- xs | P2 x) F x →

∃ x, x \in xs ∧ ~~ P1 x ∧ P2 x.

Conversely, we observe that if one predicates implies another, then the
corresponding maxima are related.