# Library rt.util.minmax

Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat rt.util.list.

Section MinMaxSeq.

Section ArgGeneric.

Context {T1 T2: eqType}.

Variable rel: T2 T2 bool.
Variable F: T1 T2.

Fixpoint seq_argmin (l: seq T1) :=
if l is x :: l' then
if seq_argmin l' is Some y then
if rel (F x) (F y) then Some x else Some y
else Some x
else None.

Fixpoint seq_argmax (l: seq T1) :=
if l is x :: l' then
if seq_argmax l' is Some y then
if rel (F y) (F x) then Some x else Some y
else Some x
else None.

Section Lemmas.

Lemma seq_argmin_exists:
l x,
x \in l
seq_argmin l != None.

Lemma seq_argmin_in_seq:
l x,
seq_argmin l = Some x
x \in l.

Lemma seq_argmax_exists:
l x,
x \in l
seq_argmax l != None.

Lemma seq_argmax_in_seq:
l x,
seq_argmax l = Some x
x \in l.

Section TotalOrder.

Hypothesis H_transitive: transitive rel.

Variable l: seq T1.
Hypothesis H_total_over_list:
x y,
x \in l
y \in l
rel (F x) (F y) || rel (F y) (F x).

Lemma seq_argmin_computes_min:
x y,
seq_argmin l = Some x
y \in l
rel (F x) (F y).

Lemma seq_argmax_computes_max:
x y,
seq_argmax l = Some x
y \in l
rel (F y) (F x).

End TotalOrder.

End Lemmas.

End ArgGeneric.

Section MinGeneric.

Context {T: eqType}.
Variable rel: rel T.

Definition seq_min := seq_argmin rel id.
Definition seq_max := seq_argmax rel id.

Section Lemmas.

Lemma seq_min_exists:
l x,
x \in l
seq_min l != None.

Lemma seq_min_in_seq:
l x,
seq_min l = Some x
x \in l.

Lemma seq_max_exists:
l x,
x \in l
seq_max l != None.

Lemma seq_max_in_seq:
l x,
seq_max l = Some x
x \in l.

Section TotalOrder.

Hypothesis H_transitive: transitive rel.

Variable l: seq T.
Hypothesis H_total_over_list:
x y,
x \in l
y \in l
rel x y || rel y x.

Lemma seq_min_computes_min:
x y,
seq_min l = Some x
y \in l
rel x y.

Lemma seq_max_computes_max:
x y,
seq_max l = Some x
y \in l
rel y x.

End TotalOrder.

End Lemmas.

End MinGeneric.

Section ArgNat.

Context {T: eqType}.

Variable F: T nat.

Definition seq_argmin_nat := seq_argmin leq F.
Definition seq_argmax_nat := seq_argmax leq F.

Section Lemmas.

Lemma seq_argmin_nat_exists:
l x,
x \in l
seq_argmin_nat l != None.

Lemma seq_argmin_nat_in_seq:
l x,
seq_argmin_nat l = Some x
x \in l.

Lemma seq_argmax_nat_exists:
l x,
x \in l
seq_argmax_nat l != None.

Lemma seq_argmax_nat_in_seq:
l x,
seq_argmax_nat l = Some x
x \in l.

Section TotalOrder.

Lemma seq_argmin_nat_computes_min:
l x y,
seq_argmin_nat l = Some x
y \in l
F x F y.

Lemma seq_argmax_nat_computes_max:
l x y,
seq_argmax_nat l = Some x
y \in l
F x F y.

End TotalOrder.

End Lemmas.

End ArgNat.

Section MinNat.

Definition seq_min_nat := seq_argmin leq id.
Definition seq_max_nat := seq_argmax leq id.

Section Lemmas.

Lemma seq_min_nat_exists:
l x,
x \in l
seq_min_nat l != None.

Lemma seq_min_nat_in_seq:
l x,
seq_min_nat l = Some x
x \in l.

Lemma seq_max_nat_exists:
l x,
x \in l
seq_max_nat l != None.

Lemma seq_max_nat_in_seq:
l x,
seq_max_nat l = Some x
x \in l.

Section TotalOrder.

Lemma seq_min_nat_computes_min:
l x y,
seq_min_nat l = Some x
y \in l
x y.

Lemma seq_max_nat_computes_max:
l x y,
seq_max_nat l = Some x
y \in l
x y.

End TotalOrder.

End Lemmas.

End MinNat.

Section NatRange.

Definition values_between (a b: nat) :=
filter (fun xx a) (map (@nat_of_ord _) (enum 'I_b)).

Lemma mem_values_between a b:
x, x \in values_between a b = (a x < b).

Definition min_nat_cond P (a b: nat) :=
seq_min_nat (filter P (values_between a b)).

Definition max_nat_cond P (a b: nat) :=
seq_max_nat (filter P (values_between a b)).

Lemma min_nat_cond_exists:
(P: nat bool) (a b: nat) x,
a x < b
P x
min_nat_cond P a b != None.

Lemma min_nat_cond_in_seq:
P a b x,
min_nat_cond P a b = Some x
a x < b P x.

Lemma min_nat_cond_computes_min:
P a b x,
min_nat_cond P a b = Some x
( y, a y < b P y x y).

Lemma max_nat_cond_exists:
(P: nat bool) (a b: nat) x,
a x < b
P x
max_nat_cond P a b != None.

Lemma max_nat_cond_in_seq:
P a b x,
max_nat_cond P a b = Some x
a x < b P x.

Lemma max_nat_cond_computes_max:
P a b x,
max_nat_cond P a b = Some x
( y, a y < b P y y x).

End NatRange.

End MinMaxSeq.

Section ExtraLemmas.

Lemma leq_big_max I r (P : pred I) (E1 E2 : I nat) :
( i, P i E1 i E2 i)
\max_(i <- r | P i) E1 i \max_(i <- r | P i) E2 i.

Lemma bigmax_ord_ltn_identity n :
n > 0
\max_(i < n) i < n.

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

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

End ExtraLemmas.

Section Kmin.

Context {T1 T2: eqType}.

Variable rel: T2 T2 bool.
Variable F: T1 T2.

Fixpoint seq_argmin_k (l: seq T1) (k: nat) :=
if k is S k' then
if (seq_argmin rel F l) is Some min_x then
let l_without_min := rem min_x l in
min_x :: seq_argmin_k l_without_min k'
else [::]
else [::].

Lemma seq_argmin_k_exists:
k l x,
k > 0
x \in l
seq_argmin_k l k != [::].

End Kmin.