ArgMinMax
Martin Escardo and Paulo Oliva, October 2021, with later additions.
We have various versions of argmin and argmax with different assumptions.
{-# OPTIONS --safe --without-K #-}
module Games.ArgMinMax where
open import MLTT.Spartan hiding (_+_ ; J)
In this version of argmin and argmax we a assume a finite domain with
a finite type of outcomes.
module ArgMinMax-Fin where
open import Fin.Embeddings
open import Fin.Order
open import Fin.Topology
open import Fin.Type
open import MLTT.SpartanList
open import Naturals.Order
open import Notation.Order
open import NotionsOfDecidability.Complemented
Every inhabited complemented subset of Fin n has a least and a
greatest element.
Fin-wf : {n : ℕ} (A : Fin n → 𝓤 ̇ ) (r₀ : Fin n)
→ is-complemented A
→ A r₀
→ Σ r ꞉ Fin n , A r × ((s : Fin n) → A s → r ≤ s)
Fin-wf {𝓤} {succ n} A 𝟎 d a = 𝟎 , a , λ s a' → ⟨⟩
Fin-wf {𝓤} {succ n} A (suc r₀) d a = γ
where
IH : Σ r ꞉ Fin n , A (suc r) × ((s : Fin n) → A (suc s) → r ≤ s)
IH = Fin-wf {𝓤} {n} (λ x → A (suc x)) r₀ (λ x → d (suc x)) a
r : Fin n
r = pr₁ IH
b : A (suc r)
b = pr₁ (pr₂ IH)
c : (s : Fin n) → A (suc s) → r ≤ s
c = pr₂ (pr₂ IH)
l : ¬ A 𝟎 → (s : Fin (succ n)) → A s → suc r ≤ s
l ν 𝟎 a = 𝟘-elim (ν a)
l ν (suc x) a = c x a
γ : Σ r ꞉ Fin (succ n) , A r × ((s : Fin (succ n)) → A s → r ≤ s)
γ = Cases (d 𝟎)
(λ a₀ → 𝟎 , a₀ , λ s a' → ⟨⟩)
(λ (ν : ¬ A 𝟎) → suc r , b , l ν)
Fin-co-wf : {n : ℕ} (A : Fin n → 𝓤 ̇ ) (r₀ : Fin n)
→ is-complemented A
→ A r₀
→ Σ r ꞉ Fin n , A r × ((s : Fin n) → A s → s ≤ r)
Fin-co-wf {𝓤} {succ n} A 𝟎 d a = γ
where
δ : is-decidable (Σ i ꞉ Fin n , A (suc i))
δ = Fin-Compact (A ∘ suc) (d ∘ suc)
Γ = Σ r ꞉ Fin (succ n) , A r × ((s : Fin (succ n)) → A s → s ≤ r)
γ : Γ
γ = Cases δ f g
where
f : Σ i ꞉ Fin n , A (suc i) → Γ
f (i , b) = suc r' , a' , h
where
IH : Σ r' ꞉ Fin n , A (suc r') × ((s' : Fin n) → A (suc s') → s' ≤ r')
IH = Fin-co-wf {𝓤} {n} (A ∘ suc) i (d ∘ suc) b
r' : Fin n
r' = pr₁ IH
a' : A (suc r')
a' = pr₁ (pr₂ IH)
ϕ : (s' : Fin n) → A (suc s') → s' ≤ r'
ϕ = pr₂ (pr₂ IH)
h : (s : Fin (succ n)) → A s → s ≤ suc r'
h 𝟎 c = ⋆
h (suc x) c = ϕ x c
g : ¬ (Σ i ꞉ Fin n , A (suc i)) → Γ
g ν = 𝟎 , a , h
where
h : (s : Fin (succ n)) → A s → s ≤ 𝟎
h (suc x) c = 𝟘-elim (ν (x , c))
h 𝟎 c = ⋆
Fin-co-wf {𝓤} {succ n} A (suc x) d a = suc (pr₁ IH) , pr₁ (pr₂ IH) , h
where
IH : Σ r ꞉ Fin n , A (suc r) × ((s : Fin n) → A (suc s) → s ≤ r)
IH = Fin-co-wf {𝓤} {n} (A ∘ suc) x (d ∘ suc) a
h : (s : Fin (succ n)) → A s → s ≤ suc (pr₁ IH)
h 𝟎 b = ⋆
h (suc x) b = pr₂ (pr₂ IH) x b
Fin-argmin : {a r : ℕ} (p : Fin (succ a) → Fin r)
→ Σ x ꞉ Fin (succ a) , ((y : Fin (succ a)) → p x ≤ p y)
Fin-argmin {0} p = 𝟎 , α
where
α : (y : Fin 1) → p 𝟎 ≤ p y
α 𝟎 = ≤-refl ⟦ p 𝟎 ⟧
Fin-argmin {succ a} p = γ
where
IH : Σ x ꞉ Fin (succ a) , ((y : Fin (succ a)) → p (suc x) ≤ p (suc y))
IH = Fin-argmin {a} (p ∘ suc)
x = pr₁ IH
ϕ = pr₂ IH
γ : Σ x' ꞉ Fin (succ (succ a)) , ((y : Fin (succ (succ a))) → p x' ≤ p y)
γ = h (≤-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc x) ⟧)
where
h : is-decidable (p 𝟎 ≤ p (suc x)) → type-of γ
h (inl l) = 𝟎 , α
where
α : (y : (Fin (succ (succ a)))) → p 𝟎 ≤ p y
α 𝟎 = ≤-refl ⟦ p 𝟎 ⟧
α (suc y) = ≤-trans ⟦ p 𝟎 ⟧ ⟦ p (suc x) ⟧ ⟦ p (suc y) ⟧ l (ϕ y)
h (inr ν) = suc x , α
where
α : (y : (Fin (succ (succ a)))) → p (suc x) ≤ p y
α 𝟎 = not-less-bigger-or-equal ⟦ p (suc x) ⟧ ⟦ p 𝟎 ⟧
(contrapositive (<-coarser-than-≤ ⟦ p 𝟎 ⟧ ⟦ p (suc x) ⟧) ν)
α (suc y) = ϕ y
argmin : {a r : ℕ} → (Fin (succ a) → Fin r) → Fin (succ a)
argmin p = pr₁ (Fin-argmin p)
argmin-correct : {a r : ℕ} (p : Fin (succ a) → Fin r)
→ (y : Fin (succ a)) → p (argmin p) ≤ p y
argmin-correct p = pr₂ (Fin-argmin p)
Fin-argmax : {a r : ℕ} (p : Fin (succ a) → Fin r)
→ Σ x ꞉ Fin (succ a) , ((y : Fin (succ a)) → p y ≤ p x)
Fin-argmax {0} p = 𝟎 , α
where
α : (y : Fin 1) → p y ≤ p 𝟎
α 𝟎 = ≤-refl ⟦ p 𝟎 ⟧
Fin-argmax {succ a} p = γ
where
IH : Σ x ꞉ Fin (succ a) , ((y : Fin (succ a)) → p (suc y) ≤ p (suc x))
IH = Fin-argmax {a} (p ∘ suc)
x = pr₁ IH
ϕ = pr₂ IH
γ : Σ x' ꞉ Fin (succ (succ a)) , ((y : Fin (succ (succ a))) → p y ≤ p x')
γ = h (≤-decidable ⟦ p (suc x) ⟧ ⟦ p 𝟎 ⟧)
where
h : is-decidable (p (suc x) ≤ p 𝟎) → type-of γ
h (inl l) = 𝟎 , α
where
α : (y : (Fin (succ (succ a)))) → p y ≤ p 𝟎
α 𝟎 = ≤-refl ⟦ p 𝟎 ⟧
α (suc y) = ≤-trans ⟦ p (suc y) ⟧ ⟦ p (suc x) ⟧ ⟦ p 𝟎 ⟧ (ϕ y) l
h (inr ν) = suc x , α
where
α : (y : (Fin (succ (succ a)))) → p y ≤ p (suc x)
α 𝟎 = not-less-bigger-or-equal ⟦ p 𝟎 ⟧ ⟦ p (suc x) ⟧
(contrapositive (<-coarser-than-≤ ⟦ p (suc x) ⟧ ⟦ p 𝟎 ⟧) ν)
α (suc y) = ϕ y
We could define argmin and argmax independently of their
specification, and then prove their specification:
argmin' : {a r : ℕ} → (Fin (succ a) → Fin r) → Fin (succ a)
argmin' {0} p = 𝟎
argmin' {succ a} p = γ
where
m : Fin (succ a)
m = argmin' {a} (p ∘ suc)
γ : Fin (succ (succ a))
γ = Cases (≤-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc m) ⟧)
(λ (l : p 𝟎 ≤ p (suc m)) → 𝟎)
(λ otherwise → suc m)
argmax' : {a r : ℕ} → (Fin (succ a) → Fin r) → Fin (succ a)
argmax' {0} p = 𝟎
argmax' {succ a} p = γ
where
m : Fin (succ a)
m = argmax' {a} (p ∘ suc)
γ : Fin (succ (succ a))
γ = Cases (≤-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc m) ⟧)
(λ (l : p 𝟎 ≤ p (suc m)) → suc m)
(λ otherwise → 𝟎)
TODO. Complete the following.
This version of argmin and argmax assumes a compact domain and a
finite type of outcomes.
module ArgMinMax-Compact-Fin where
open import Fin.Order
open import Fin.Topology
open import Fin.Type
open import Notation.Order
open import NotionsOfDecidability.Complemented
open import TypeTopology.CompactTypes
open ArgMinMax-Fin
compact-argmax : {X : 𝓤 ̇ } {n : ℕ} (p : X → Fin n)
→ is-Compact X
→ X
→ Σ x ꞉ X , ((y : X) → p y ≤ p x)
compact-argmax {𝓤} {X} {n} p κ x₀ = II I
where
A : Fin n → 𝓤 ̇
A r = Σ x ꞉ X , p x ＝ r
a₀ : A (p x₀)
a₀ = x₀ , refl
δ : is-complemented A
δ r = κ (λ x → p x ＝ r) (λ x → Fin-is-discrete (p x) r)
I : Σ r ꞉ Fin n , A r × ((s : Fin n) → A s → s ≤ r)
I = Fin-co-wf A (p x₀) δ a₀
II : type-of I → Σ x ꞉ X , ((y : X) → p y ≤ p x)
II (.(p y) , ((y , refl) , ϕ)) = y , (λ y → ϕ (p y) (y , refl))
compact-argmin : {X : 𝓤 ̇ } {n : ℕ} (p : X → Fin n)
→ is-Compact X
→ X
→ Σ x ꞉ X , ((y : X) → p x ≤ p y)
compact-argmin {𝓤} {X} {n} p κ x₀ = II I
where
A : Fin n → 𝓤 ̇
A r = Σ x ꞉ X , p x ＝ r
a₀ : A (p x₀)
a₀ = x₀ , refl
δ : is-complemented A
δ r = κ (λ x → p x ＝ r) (λ x → Fin-is-discrete (p x) r)
I : Σ r ꞉ Fin n , A r × ((s : Fin n) → A s → r ≤ s)
I = Fin-wf A (p x₀) δ a₀
II : type-of I → Σ x ꞉ X , ((y : X) → p x ≤ p y)
II (.(p y) , ((y , refl) , ϕ)) = y , (λ y → ϕ (p y) (y , refl))
Added 11th September 2024. Simplified and more efficient version for
the boolean-valued case.
module ArgMinMax-Fin-𝟚 where
open import Fin.Type
open import MLTT.Two-Properties
open import Naturals.Addition
Min₂ : (i : ℕ) → (Fin (i + 1) → 𝟚) → 𝟚
Min₂ 0 p = p 𝟎
Min₂ (succ i) p = min𝟚 (p 𝟎) (Min₂ i (p ∘ suc))
Max₂ : (i : ℕ) → (Fin (i + 1) → 𝟚) → 𝟚
Max₂ 0 p = p 𝟎
Max₂ (succ i) p = max𝟚 (p 𝟎) (Max₂ i (p ∘ suc))
argMin₂ : (i : ℕ) → (Fin (i + 1) → 𝟚) → Fin (i + 1)
argMin₂ 0 p = 𝟎
argMin₂ (succ i) p =
𝟚-equality-cases
(λ (_ : p 𝟎 ＝ ₀) → 𝟎)
(λ (_ : p 𝟎 ＝ ₁) → suc (argMin₂ i (p ∘ suc)))
argMax₂ : (i : ℕ) → (Fin (i + 1) → 𝟚) → Fin (i + 1)
argMax₂ 0 p = 𝟎
argMax₂ (succ i) p =
𝟚-equality-cases
(λ (_ : p 𝟎 ＝ ₀) → suc (argMax₂ i (p ∘ suc)))
(λ (_ : p 𝟎 ＝ ₁) → 𝟎)
argMin₂-is-selection-for-Min₂ : (i : ℕ)
(p : Fin (i + 1) → 𝟚)
→ p (argMin₂ i p) ＝ Min₂ i p
argMin₂-is-selection-for-Min₂ 0 p = refl
argMin₂-is-selection-for-Min₂ (succ i) p =
𝟚-equality-cases
(λ (e : p 𝟎 ＝ ₀)
→ p (argMin₂ (succ i) p) ＝⟨ ap p (𝟚-equality-cases₀ e) ⟩
p 𝟎 ＝⟨ e ⟩
₀ ＝⟨refl⟩
min𝟚 ₀ (Min₂ i (p ∘ suc)) ＝⟨ ap (λ - → min𝟚 - (Min₂ i (p ∘ suc))) (e ⁻¹) ⟩
min𝟚 (p 𝟎) (Min₂ i (p ∘ suc)) ＝⟨refl⟩
Min₂ (succ i) p ∎)
(λ (e : p 𝟎 ＝ ₁)
→ p (argMin₂ (succ i) p) ＝⟨ ap p (𝟚-equality-cases₁ e) ⟩
p (suc (argMin₂ i (p ∘ suc))) ＝⟨ argMin₂-is-selection-for-Min₂ i (p ∘ suc) ⟩
Min₂ i (p ∘ suc) ＝⟨refl⟩
min𝟚 ₁ (Min₂ i (p ∘ suc)) ＝⟨ ap (λ - → min𝟚 - (Min₂ i (p ∘ suc))) (e ⁻¹) ⟩
min𝟚 (p 𝟎) (Min₂ i (p ∘ suc)) ＝⟨refl⟩
Min₂ (succ i) p ∎)
argMax₂-is-selection-for-Max₂ : (i : ℕ)
(p : Fin (i + 1) → 𝟚)
→ p (argMax₂ i p) ＝ Max₂ i p
argMax₂-is-selection-for-Max₂ 0 p = refl
argMax₂-is-selection-for-Max₂ (succ i) p =
𝟚-equality-cases
(λ (e : p 𝟎 ＝ ₀)
→ p (argMax₂ (succ i) p) ＝⟨ ap p (𝟚-equality-cases₀ e) ⟩
p (suc (argMax₂ i (p ∘ suc))) ＝⟨ argMax₂-is-selection-for-Max₂ i (p ∘ suc) ⟩
Max₂ i (p ∘ suc) ＝⟨refl⟩
max𝟚 ₀ (Max₂ i (p ∘ suc)) ＝⟨ ap (λ - → max𝟚 - (Max₂ i (p ∘ suc))) (e ⁻¹) ⟩
max𝟚 (p 𝟎) (Max₂ i (p ∘ suc)) ＝⟨refl⟩
Max₂ (succ i) p ∎)
(λ (e : p 𝟎 ＝ ₁)
→ p (argMax₂ (succ i) p) ＝⟨ ap p (𝟚-equality-cases₁ e) ⟩
p 𝟎 ＝⟨ e ⟩
₁ ＝⟨refl⟩
max𝟚 ₁ (Max₂ i (p ∘ suc)) ＝⟨ ap (λ - → max𝟚 - (Max₂ i (p ∘ suc))) (e ⁻¹) ⟩
max𝟚 (p 𝟎) (Max₂ i (p ∘ suc)) ＝⟨refl⟩
Max₂ (succ i) p ∎)
Added 3rd March 2026. Moved and refined from the alpha-beta file.
This version of argmin and argmax assumes a listed domain and
any type of outcomes that has a decidable order.
Modified 1st July 2026. It suffices to consider only argmin, because
we can work with the opposite order to get argmax.
module ArgMin-Listed
{𝓤 𝓥 : Universe}
(R : 𝓤 ̇ )
(_<_ : R → R → 𝓥 ̇ )
(δ : (r s : R) → is-decidable (r < s))
where
open import MLTT.List
minδ : (r s : R) → is-decidable (r < s) → R
minδ r s (inl lt) = r
minδ r s (inr ge) = s
min : R → R → R
min r s = minδ r s (δ r s)
open import MonadOnTypes.K
open K-definitions {𝓤} {R}
Min : {X : 𝓤 ̇ } → listed⁺ X → K X
Min (x₀ , xs , _) p = foldr (λ x → min (p x)) (p x₀) xs
argminδ : {X : 𝓤 ̇ } (p : X → R) (x y : X) → is-decidable (p x < p y) → X
argminδ p x y (inl le) = x
argminδ p x y (inr ge) = y
argminδ-spec : {X : 𝓤 ̇ } (p : X → R) (x y : X) (d : is-decidable (p x < p y))
→ p (argminδ p x y d) ＝ minδ (p x) (p y) d
argminδ-spec p x y (inl lt) = refl
argminδ-spec p x y (inr ge) = refl
argmin : {X : 𝓤 ̇ } → (X → R) → X → X → X
argmin p x y = argminδ p x y (δ (p x) (p y))
argmin-spec : {X : 𝓤 ̇ } (p : X → R) (x y : X)
→ p (argmin p x y) ＝ min (p x) (p y)
argmin-spec p x y = argminδ-spec p x y (δ (p x) (p y))
open import MonadOnTypes.J
open J-definitions {𝓤} {R}
ArgMin : {X : 𝓤 ̇ } → listed⁺ X → J X
ArgMin (x₀ , xs , _) p = foldr (argmin p) x₀ xs
open import MonadOnTypes.JK R
ArgMin-spec : {X : 𝓤 ̇ } (ℓ : listed⁺ X) → (ArgMin ℓ) attains (Min ℓ)
ArgMin-spec {X} (x₀ , xs , m) p = I xs
where
I : (xs : List X)
→ p (foldr (argmin p) x₀ xs) ＝ foldr (λ x → min (p x)) (p x₀) xs
I [] = refl
I (x ∷ xs) = I₀
where
IH : p (foldr (argmin p) x₀ xs) ＝ foldr (λ x → min (p x)) (p x₀) xs
IH = I xs
I₀ = p (argmin p x (foldr (argmin p) x₀ xs)) ＝⟨ I₁ ⟩
min (p x) (p (foldr (argmin p) x₀ xs)) ＝⟨ I₂ ⟩
min (p x) (foldr (λ x₁ → min (p x₁)) (p x₀) xs) ∎
where
I₁ = argmin-spec p x (foldr (argmin p) x₀ xs)
I₂ = ap (min (p x)) IH
foldr-min-attainment
: {X : 𝓤 ̇ } (p : X → R) (x₀ : X) (xs : List X)
→ p (foldr (argmin p) x₀ xs) ＝ foldr (λ x → min (p x)) (p x₀) xs
foldr-min-attainment p x₀ [] = refl
foldr-min-attainment {X} p x₀ (x ∷ xs) =
p (argmin p x x') ＝⟨ argmin-spec p x x' ⟩
min (p x) (p x') ＝⟨ ap (min (p x)) IH ⟩
min (p x) (foldr (λ x → min (p x)) (p x₀) xs) ∎
where
x' : X
x' = foldr (argmin p) x₀ xs
IH : p x' ＝ foldr (λ x → min (p x)) (p x₀) xs
IH = foldr-min-attainment p x₀ xs
By taking the opposite order, we can use ArgMin to compute ArgMax:
module ArgMax-Listed
{𝓤 𝓥 : Universe}
(R : 𝓤 ̇ )
(_<_ : R → R → 𝓥 ̇ )
(δ : (r s : R) → is-decidable (r < s))
where
open ArgMin-Listed R (λ x y → y < x) (λ x y → δ y x)
renaming (
minδ to maxδ
; min to max
; argminδ to argmaxδ
; argminδ-spec to argmaxδ-spec
; argmin to argmax
; argmin-spec to argmax-spec
; Min to Max
; ArgMin to ArgMax
; ArgMin-spec to ArgMax-spec
; foldr-min-attainment to foldr-max-attainment
)
public
We now define a single module that reexports ArgMin and ArgMax
together:
module ArgMinMax-Listed
{𝓤 𝓥 : Universe}
(R : 𝓤 ̇ )
(_<_ : R → R → 𝓥 ̇ )
(δ : (r s : R) → is-decidable (r < s))
where
open ArgMin-Listed {𝓤} {𝓥} R _<_ δ public
open ArgMax-Listed {𝓤} {𝓥} R _<_ δ public
We now define a version of ArgMin with a modification R' of the
outcome type R, and, crucially, we relate it to the original
version. We use this for the purpose of the module alpha-beta.
module ArgMin'-Listed
{𝓤 𝓥 𝓦 : Universe}
(R : 𝓤 ̇ )
(_<_ : R → R → 𝓥 ̇ )
(δ : (r s : R) → is-decidable (r < s))
(P : 𝓦 ̇ )
where
open import MLTT.List
private
R' : 𝓤 ⊔ 𝓦 ̇
R' = R × P
_<'_ : R' → R' → 𝓥 ̇
(r , _) <' (s , _) = r < s
δ' : (r' s' : R') → is-decidable (r' <' s')
δ' (r , _) (s , _) = δ r s
open ArgMin-Listed R' _<'_ δ'
using () renaming (minδ to min'δ ; min to min' ; Min to Min')
module _ (X : 𝓤 ̇ )
(X-is-listed⁺@(x₀ , xs , m) : listed⁺ X)
where
open ArgMinMax-Listed {𝓤} {𝓥} R _<_ δ
using (ArgMin; argminδ ; argmin ; foldr-min-attainment)
The main technical result of this module is the following relation
between argmin and min':
foldr-min'-attainment
: (p : X → R') (x₀ : X) (xs : List X)
→ p (foldr (argmin (pr₁ ∘ p)) x₀ xs) ＝ foldr (λ x → min' (p x)) (p x₀) xs
foldr-min'-attainment p x₀ [] = refl
foldr-min'-attainment p x₀ (x ∷ xs) =
p (argmin p' x x') ＝⟨ I (δ (p' x) (p' x')) ⟩
min' (p x) (p x') ＝⟨ ap (min' (p x)) IH ⟩
min' (p x) (foldr (λ x → min' (p x)) (p x₀) xs) ∎
where
p' : X → R
p' = pr₁ ∘ p
x' : X
x' = foldr (argmin p') x₀ xs
IH : p (foldr (argmin p') x₀ xs)
＝ foldr (λ x → min' (p x)) (p x₀) xs
IH = foldr-min'-attainment p x₀ xs
I : (d : is-decidable (p' x < p' x'))
→ p (argminδ p' x x' d) ＝ min'δ (p x) (p x') d
I (inl lt) = refl
I (inr ge) = refl
We do the same for ArgMax by taking the opposite order.
module ArgMax'-Listed
{𝓤 𝓥 𝓦 : Universe}
(R : 𝓤 ̇ )
(_<_ : R → R → 𝓥 ̇ )
(δ : (r s : R) → is-decidable (r < s))
(P : 𝓦 ̇ )
where
open ArgMin'-Listed R (λ r s → s < r) (λ r s → δ s r) P
renaming (foldr-min'-attainment to foldr-max'-attainment)
public
And now we combine ArgMin' and ArgMax' in a single module that
reexports them.
module ArgMinMax'-Listed
{𝓤 𝓥 𝓦 : Universe}
(R : 𝓤 ̇ )
(_<_ : R → R → 𝓥 ̇ )
(δ : (r s : R) → is-decidable (r < s))
(P : 𝓦 ̇ )
where
open ArgMin'-Listed R _<_ δ P public
open ArgMax'-Listed R _<_ δ P public