Library prosa.util.minmax
Require Export prosa.util.notation prosa.util.nat prosa.util.list.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
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.