Library prosa.util.minmax

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.

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.
  Lemma bigmax_pred :
     (n : nat) (P : pred nat) (i0 : 'I_n),
      P i0
      P (\max_(i < n | P i) i).

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).
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.
Conversely, we observe that if one predicates implies another, then the corresponding maxima are related.
  Corollary bigmax_subset {T : eqType} :
     {xs : seq T} {P1 P2 : pred T} {F},
      ( x, x \in xs P1 x P2 x)
      \max_(x <- xs | P1 x) F x \max_(x <- xs | P2 x) F x.

End ExtraLemmas.