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