From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
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 :
    forall {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.
forall (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
  Proof.
forall (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 by intros * IN Px; rewrite (big_rem x) //= Px leq_maxl. Qed.

  (** 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 : 
    forall {X : eqType} (F : X -> nat) (P : pred X) (xs : seq X) (m : nat),
      reflect (forall x, x \in xs -> P x -> F x <= m)
              (\max_(x <- xs | P x) F x <= m).
forall (X : eqType) (F : X -> nat) (P : pred X)
  (xs : seq X) (m : nat),
reflect (forall x : X, x \in xs -> P x -> F x <= m)
  (\max_(x <- xs | P x) F x <= m)
  Proof.
forall (X : eqType) (F : X -> nat) (P : pred X)
  (xs : seq X) (m : nat),
reflect (forall x : X, x \in xs -> P x -> F x <= m)
  (\max_(x <- xs | P x) F x <= m)
    intros *.
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
reflect (forall x : X, x \in xs -> P x -> F x <= m)
  (\max_(x <- xs | P x) F x <= m)
    apply: (iffP idP) => leFm => [i IINR Pi|].
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: \max_(x <- xs | P x) F x <= m
i: X
IINR: i \in xs
Pi: P i
F i <= m
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : 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
leFm: \max_(x <- xs | P x) F x <= m
i: X
IINR: i \in xs
Pi: P i
F i <= m
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : X, x \in xs -> P x -> F x <= m
\max_(x <- xs | P x) F x <= m by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : 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
leFm: forall x : X, x \in xs -> P x -> F x <= m
\max_(x <- xs | P x) F x <= m rewrite big_seq_cond; elim/big_ind: _ => // m1 m2.
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : X, x \in xs -> P x -> F x <= m
m1, m2: nat
m1 <= m -> m2 <= m -> maxn m1 m2 <= m
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : X, x \in xs -> P x -> F x <= m
m1: X
m2: (m1 \in xs) && P m1
F m1 <= m
      +
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : X, x \in xs -> P x -> F x <= m
m1, m2: nat
m1 <= m -> m2 <= m -> maxn m1 m2 <= m
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : X, x \in xs -> P x -> F x <= m
m1: X
m2: (m1 \in xs) && P m1
F m1 <= m by intros; rewrite geq_max; apply/andP; split.
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : X, x \in xs -> P x -> F x <= m
m1: X
m2: (m1 \in xs) && P m1
F m1 <= m 
      +
X: eqType
F: X -> nat
P: pred X
xs: seq X
m: nat
leFm: forall x : X, x \in xs -> P x -> F x <= m
m1: X
m2: (m1 \in xs) && P m1
F m1 <= m by move: m2 => /andP [M1IN Pm1]; apply: leFm.
  Qed.

  (** 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 :
    forall {X : eqType} (F1 F2 : X -> nat) (P : pred X) (xs : seq X), 
      (forall x, x \in xs -> P x -> F1 x <= F2 x) ->
      \max_(x <- xs | P x) F1 x <= \max_(x <- xs | P x) F2 x.
forall (X : eqType) (F1 F2 : X -> nat) (P : pred X)
  (xs : seq X),
(forall 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
  Proof.
forall (X : eqType) (F1 F2 : X -> nat) (P : pred X)
  (xs : seq X),
(forall 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
    intros * ALL; apply /bigmax_leq_seqP; intros * IN Px.
X: eqType
F1, F2: X -> nat
P: pred X
xs: seq X
ALL: forall x : X, x \in xs -> P x -> F1 x <= F2 x
x: X
IN: x \in xs
Px: P x
F1 x <= \max_(x <- xs | P x) F2 x
    specialize (ALL x); feed_n 2 ALL; try done.
X: eqType
F1, F2: X -> nat
P: pred X
xs: seq X
x: X
ALL: F1 x <= F2 x
IN: x \in xs
Px: P x
F1 x <= \max_(x <- xs | P x) F2 x
    rewrite (big_rem x) //=; rewrite Px.
X: eqType
F1, F2: X -> nat
P: pred X
xs: seq X
x: X
ALL: F1 x <= F2 x
IN: x \in xs
Px: P x
F1 x <=
maxn (F2 x) (\max_(y <- rem (T:=X) x xs | P y) F2 y)
    by apply leq_trans with (F2 x); [ | rewrite leq_maxl].
  Qed.

  (** We show that for a positive [n], [max] of [{0, …, n-1}] is
      smaller than [n]. *)
  Lemma bigmax_ord_ltn_identity :
    forall (n : nat), 
      n > 0 ->
      \max_(i < n) i < n.
forall n : nat, 0 < n -> \max_(i < n) i < n
  Proof.
forall n : nat, 0 < n -> \max_(i < n) i < n
    intros [ | n] POS; first by rewrite ltn0 in POS.
n: nat
POS: 0 < n.+1
\max_(i < n.+1) i < n.+1
    clear POS; induction n; first by rewrite big_ord_recr /= big_ord0 maxn0.
n: nat
IHn: \max_(i < n.+1) i < n.+1
\max_(i < n.+2) i < n.+2
    rewrite big_ord_recr /=.
n: nat
IHn: \max_(i < n.+1) i < n.+1
maxn (\max_(i < n.+1) i) n.+1 < n.+2
    by rewrite /maxn IHn.
  Qed.

  (** 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 :
    forall (n : nat) (P : pred nat) (i0 : 'I_n), 
    P i0 ->
    \max_(i < n | P i) i < n.
forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 -> \max_(i < n | P i) i < n
  Proof.
forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 -> \max_(i < n | P i) i < n
    intros n P i0 Pi.
n: nat
P: pred nat
i0: 'I_n
Pi: P i0
\max_(i < n | P i) i < n
    destruct n; first by destruct i0 as [i0 P0]; move: (P0) => P0'; rewrite ltn0 in P0'.
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\max_(i < n.+1 | P i) i < n.+1
    rewrite big_mkcond.
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\big[maxn_monoid/0]_i (if P i then i else 0) < n.+1
    apply leq_ltn_trans with (n := \max_(i < n.+1) i).
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\big[maxn_monoid/0]_i (if P i then i else 0) <=
\max_(i < n.+1) i
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\max_(i < n.+1) i < n.+1
    -
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\big[maxn_monoid/0]_i (if P i then i else 0) <=
\max_(i < n.+1) i
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\max_(i < n.+1) i < n.+1 apply/bigmax_leqP; ins.
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
i: 'I_n.+1
H: true
(if P i then i else 0) <= \max_(i < n.+1) i
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\max_(i < n.+1) i < n.+1
      destruct (P i); last by done.
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
i: 'I_n.+1
H: true
i <= \max_(i < n.+1) i
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\max_(i < n.+1) i < n.+1
      by apply leq_bigmax_cond.
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\max_(i < n.+1) i < n.+1
    -
n: nat
P: pred nat
i0: 'I_n.+1
Pi: P i0
\max_(i < n.+1) i < n.+1 by apply bigmax_ord_ltn_identity.
  Qed.

  (** 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 :
    forall (n : nat) (P : pred nat) (i0 : 'I_n), 
      P i0 ->
      P (\max_(i < n | P i) i).
forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 -> P (\max_(i < n | P i) i)
  Proof.
forall (n : nat) (P : pred nat) (i0 : 'I_n),
P i0 -> P (\max_(i < n | P i) i)
    intros * Pi0.
n: nat
P: pred nat
i0: 'I_n
Pi0: P i0
P (\max_(i < n | P i) i)
    induction n.
P: pred nat
i0: 'I_0
Pi0: P i0
P (\max_(i < 0 | P i) i)
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
P (\max_(i < n.+1 | P i) i)
    {
P: pred nat
i0: 'I_0
Pi0: P i0
P (\max_(i < 0 | P i) i) by destruct i0 as [i0 P0]; move: (P0) => P1; rewrite ltn0 in P1. }
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
P (\max_(i < n.+1 | P i) i)
    {
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
P (\max_(i < n.+1 | P i) i) rewrite big_mkcond big_ord_recr /=.
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
P
  (maxn (\max_(i < n) (if P i then i else 0))
     (if P n then n else 0))
      destruct (P n) eqn:Pn.
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = true
P (maxn (\max_(i < n) (if P i then i else 0)) n)
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = false
P (maxn (\max_(i < n) (if P i then i else 0)) 0)
      {
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = true
P (maxn (\max_(i < n) (if P i then i else 0)) n) destruct n; first by rewrite big_ord0 maxn0.
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
P (maxn (\max_(i < n.+1) (if P i then i else 0)) n.+1)
        unfold maxn at 1.
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
P
  (if \max_(i < n.+1) (if P i then i else 0) < n.+1
   then n.+1
   else \max_(i < n.+1) (if P i then i else 0))
        destruct (\max_(i < n.+1) (match P (@nat_of_ord (S n) i) return nat with
                                   | true => @nat_of_ord (S n) i
                                   | false => O
                                   end) < n.+1) eqn:Pi; first by rewrite Pi.
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
Pi: (\max_(i < n.+1) (if P i then i else 0) < n.+1) =
false
P
  (if \max_(i < n.+1) (if P i then i else 0) < n.+1
   then n.+1
   else \max_(i < n.+1) (if P i then i else 0))
        exfalso.
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
Pi: (\max_(i < n.+1) (if P i then i else 0) < n.+1) =
false
False
        apply negbT in Pi; move: Pi => /negP BUG; apply: BUG.
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
\max_(i < n.+1) (if P i then i else 0) < n.+1 
        apply leq_ltn_trans with (n := \max_(i < n.+1) i).
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
\max_(i < n.+1) (if P i then i else 0) <=
\max_(i < n.+1) i
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
\max_(i < n.+1) i < n.+1
        {
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
\max_(i < n.+1) (if P i then i else 0) <=
\max_(i < n.+1) i apply/bigmax_leqP; rewrite //= => i _.
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
i: 'I_n.+1
(if P i then i else 0) <= \max_(i < n.+1) i 
          by destruct (P i); first apply leq_bigmax_cond.
        }
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
\max_(i < n.+1) i < n.+1
        {
n: nat
P: pred nat
i0: 'I_n.+2
Pi0: P i0
IHn: forall i0 : 'I_n.+1, P i0 -> P (\max_(i < n.+1 | P i) i)
Pn: P n.+1 = true
\max_(i < n.+1) i < n.+1 by apply bigmax_ord_ltn_identity. } 
      }
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = false
P (maxn (\max_(i < n) (if P i then i else 0)) 0)
      {
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = false
P (maxn (\max_(i < n) (if P i then i else 0)) 0) rewrite maxn0 -big_mkcond /=.
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = false
P (\max_(i < n | P i) i)
        have LT: i0 < n; last by rewrite (IHn (Ordinal LT)).
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = false
i0 < n
        rewrite ltn_neqAle; apply/andP; split;
          last by rewrite -ltnS; apply ltn_ord.
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = false
i0 != n
        apply/negP; move => /eqP BUG.
n: nat
P: pred nat
i0: 'I_n.+1
Pi0: P i0
IHn: forall i0 : 'I_n, P i0 -> P (\max_(i < n | P i) i)
Pn: P n = false
BUG: i0 = n
False
        by rewrite -BUG Pi0 in Pn.
      }
    }
  Qed.

  (** 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} :
    forall {xs : seq T} {P} F,
      has P xs ->
      exists x, x \in xs /\ P x /\ (F x = \max_(x <- xs | P x) F x).
T: eqType
forall (xs : seq T) (P : pred T) (F : T -> nat),
has P xs ->
exists x : T,
  x \in xs /\ P x /\ F x = \max_(x0 <- xs | P x0) F x0
  Proof.
T: eqType
forall (xs : seq T) (P : pred T) (F : T -> nat),
has P xs ->
exists x : T,
  x \in xs /\ P x /\ F x = \max_(x0 <- xs | P x0) F x0
    move=> xs P F.
T: eqType
xs: seq T
P: pred T
F: T -> nat
has P xs ->
exists x : T,
  x \in xs /\ P x /\ F x = \max_(x0 <- xs | P x0) F x0
    elim: xs => // a xs IH HAS.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
    case: (boolP (P a)); last first.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
~~ P a ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
P a ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
    {
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
~~ P a ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0 move=> /negPf NOT.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
NOT: P a = false
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
      move: HAS; rewrite /has NOT //= -/(has P xs) => HAS.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
NOT: P a = false
HAS: has P xs
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
      move: (IH HAS) => [x [IN [Px Fx]]].
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
NOT: P a = false
HAS: has P xs
x: T
IN: x \in xs
Px: P x
Fx: F x = \max_(x <- xs | P x) F x
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
      exists x; repeat split => //;
                            first by rewrite in_cons; apply /orP; right.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
NOT: P a = false
HAS: has P xs
x: T
IN: x \in xs
Px: P x
Fx: F x = \max_(x <- xs | P x) F x
F x = \max_(x <- (a :: xs) | P x) F x
      by rewrite big_cons ifF. }
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
P a ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
    {
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
P a ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0 move=> Pa.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
      case: (boolP (has P xs)) => HAS'; last first.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': ~~ has P xs
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
      {
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': ~~ has P xs
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0 exists a; repeat split => //; first by apply: mem_head.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': ~~ has P xs
F a = \max_(x <- (a :: xs) | P x) F x
        by rewrite big_cons ifT // big_hasC. }
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
      {
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0 move: (IH HAS') => [x [IN [Px MAX]]].
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
        case: (leqP (\max_(x <- xs | P x) F x) (F a)).
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
\max_(x <- xs | P x) F x <= F a ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
F a < \max_(x <- xs | P x) F x ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
        {
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
\max_(x <- xs | P x) F x <= F a ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0 move=> LEQ.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
LEQ: \max_(x <- xs | P x) F x <= F a
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0 exists a.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
LEQ: \max_(x <- xs | P x) F x <= F a
a \in a :: xs /\
P a /\ F a = \max_(x <- (a :: xs) | P x) F x
          repeat split => //; first by rewrite mem_head.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
LEQ: \max_(x <- xs | P x) F x <= F a
F a = \max_(x <- (a :: xs) | P x) F x
          rewrite big_cons ifT //= [maxn (_) (_)]/maxn ifF //.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
LEQ: \max_(x <- xs | P x) F x <= F a
(F a < \max_(j <- xs | P j) F j) = false
          by lia. }
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
F a < \max_(x <- xs | P x) F x ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0
        {
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
F a < \max_(x <- xs | P x) F x ->
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0 move=> LT.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
LT: F a < \max_(x <- xs | P x) F x
exists x : T,
  x \in a :: xs /\
  P x /\ F x = \max_(x0 <- (a :: xs) | P x0) F x0 exists x.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
LT: F a < \max_(x <- xs | P x) F x
x \in a :: xs /\
P x /\ F x = \max_(x <- (a :: xs) | P x) F x
          repeat split => //; first by rewrite in_cons; apply /orP; right.
T: eqType
P: pred T
F: T -> nat
a: T
xs: seq T
IH: has P xs ->
exists x : T,
  x \in xs /\
  P x /\ F x = \max_(x0 <- xs | P x0) F x0
HAS: has P (a :: xs)
Pa: P a
HAS': has P xs
x: T
IN: x \in xs
Px: P x
MAX: F x = \max_(x <- xs | P x) F x
LT: F a < \max_(x <- xs | P x) F x
F x = \max_(x <- (a :: xs) | P x) F x
          by rewrite big_cons ifT //= [maxn (_) (_)]/maxn ifT. } } }
  Qed.

  (** 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} :
    forall {xs : seq T} {P1 P2 F},
      \max_(x <- xs | P1 x) F x < \max_(x <- xs | P2 x) F x ->
      exists x, x \in xs /\ ~~ P1 x /\ P2 x.
T: eqType
forall (xs : seq T) (P1 P2 : T -> bool) (F : T -> nat),
\max_(x <- xs | P1 x) F x < \max_(x <- xs | P2 x) F x ->
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
  Proof.
T: eqType
forall (xs : seq T) (P1 P2 : T -> bool) (F : T -> nat),
\max_(x <- xs | P1 x) F x < \max_(x <- xs | P2 x) F x ->
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
    move=> xs P1 P2 F LT.
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
    case: (boolP (has P1 xs)) => HP1;
                                  case: (boolP (has P2 xs)) => HP2.
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: ~~ has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: ~~ has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
    {
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x move: (bigmax_witness F HP2) => [x2 [IN2 [Px2 MAX2]]].
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: has P2 xs
x2: T
IN2: x2 \in xs
Px2: P2 x2
MAX2: F x2 = \max_(x <- xs | P2 x) F x
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
      exists x2; repeat split => //.
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: has P2 xs
x2: T
IN2: x2 \in xs
Px2: P2 x2
MAX2: F x2 = \max_(x <- xs | P2 x) F x
~~ P1 x2
      apply: contraT => /negPn Px1; exfalso.
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: has P2 xs
x2: T
IN2: x2 \in xs
Px2: P2 x2
MAX2: F x2 = \max_(x <- xs | P2 x) F x
Px1: P1 x2
False
      have BOUNDED: F x2 <=  \max_(x <- xs | P1 x) F x by apply: leq_bigmax_cond_seq.
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: has P2 xs
x2: T
IN2: x2 \in xs
Px2: P2 x2
MAX2: F x2 = \max_(x <- xs | P2 x) F x
Px1: P1 x2
BOUNDED: F x2 <= \max_(x <- xs | P1 x) F x
False
      by lia. }
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: ~~ has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: ~~ has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
    {
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: has P1 xs
HP2: ~~ has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x by exfalso; move: LT; rewrite (big_hasC _ _ _ HP2). }
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: ~~ has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
    {
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x move: (bigmax_witness F HP2) => [x2 [IN2 [Px2 MAX2]]].
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: has P2 xs
x2: T
IN2: x2 \in xs
Px2: P2 x2
MAX2: F x2 = \max_(x <- xs | P2 x) F x
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
      exists x2; repeat split => //.
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: has P2 xs
x2: T
IN2: x2 \in xs
Px2: P2 x2
MAX2: F x2 = \max_(x <- xs | P2 x) F x
~~ P1 x2
      move: HP1 => /hasPn HP1.
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP2: has P2 xs
x2: T
IN2: x2 \in xs
Px2: P2 x2
MAX2: F x2 = \max_(x <- xs | P2 x) F x
HP1: {in xs, forall x : T, ~~ P1 x}
~~ P1 x2
      by move: (HP1 x2 IN2). }
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: ~~ has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x
    {
T: eqType
xs: seq T
P1, P2: T -> bool
F: T -> nat
LT: \max_(x <- xs | P1 x) F x <
\max_(x <- xs | P2 x) F x
HP1: ~~ has P1 xs
HP2: ~~ has P2 xs
exists x : T, x \in xs /\ ~~ P1 x /\ P2 x by exfalso; move: LT; rewrite !big_hasC. }
  Qed.

  (** Conversely, we observe that if one predicates implies another, then the
      corresponding maxima are related. *)
  Corollary bigmax_subset {T : eqType} :
    forall {xs : seq T} {P1 P2 : pred T} {F},
      (forall x, x \in xs -> P1 x -> P2 x) ->
      \max_(x <- xs | P1 x) F x <= \max_(x <- xs | P2 x) F x.
T: eqType
forall (xs : seq T) (P1 P2 : pred T) (F : T -> nat),
(forall x : T, x \in xs -> P1 x -> P2 x) ->
\max_(x <- xs | P1 x) F x <= \max_(x <- xs | P2 x) F x
  Proof.
T: eqType
forall (xs : seq T) (P1 P2 : pred T) (F : T -> nat),
(forall x : T, x \in xs -> P1 x -> P2 x) ->
\max_(x <- xs | P1 x) F x <= \max_(x <- xs | P2 x) F x
    move=> xs P1 P2 F IMPL.
T: eqType
xs: seq T
P1, P2: pred T
F: T -> nat
IMPL: forall x : T, x \in xs -> P1 x -> P2 x
\max_(x <- xs | P1 x) F x <= \max_(x <- xs | P2 x) F x
    apply: contraT; rewrite -ltnNge => LT.
T: eqType
xs: seq T
P1, P2: pred T
F: T -> nat
IMPL: forall x : T, x \in xs -> P1 x -> P2 x
LT: \max_(x <- xs | P2 x) F x <
\max_(x <- xs | P1 x) F x
false
    exfalso.
T: eqType
xs: seq T
P1, P2: pred T
F: T -> nat
IMPL: forall x : T, x \in xs -> P1 x -> P2 x
LT: \max_(x <- xs | P2 x) F x <
\max_(x <- xs | P1 x) F x
False
    move: (bigmax_witness_diff LT) => [x [IN [/negP Px2 Px1]]].
T: eqType
xs: seq T
P1, P2: pred T
F: T -> nat
IMPL: forall x : T, x \in xs -> P1 x -> P2 x
LT: \max_(x <- xs | P2 x) F x <
\max_(x <- xs | P1 x) F x
x: T
IN: x \in xs
Px2: ~ P2 x
Px1: P1 x
False
    by apply Px2, IMPL.
  Qed.

End ExtraLemmas.