Martin Escardo and Paulo Oliva, October 2021, with later additions.

We have various versions of argmin and argmax with different assumptions.


\begin{code}

{-# OPTIONS --safe --without-K #-}

module Games.ArgMinMax where

open import MLTT.Spartan hiding (_+_ ; J)

\end{code}

In this version of argmin and argmax we a assume a finite domain with
a finite type of outcomes.

\begin{code}

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

\end{code}

Every inhabited complemented subset of Fin n has a least and a
greatest element.

\begin{code}

 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

\end{code}

We could define argmin and argmax independently of their
specification, and then prove their specification:

\begin{code}

 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 β†’ 𝟎)

\end{code}

TODO. Complete the following.

\begin{code}

 {-
 argmax'-correct : {a r : β„•} (p : Fin (succ a) β†’ Fin r)
                β†’ ((y : Fin (succ a)) β†’ p y ≀ p (argmax p))
 argmax'-correct {0}      p 𝟎 = ≀-refl ⟦ p 𝟎 ⟧
 argmax'-correct {succ a} p y = h y
  where
   m : Fin (succ a)
   m = argmax {a} (p ∘ suc)

   IH : (y : Fin (succ a)) β†’ p (suc y) ≀ p (suc m)
   IH = argmax-correct {a} (p ∘ suc)

   Ξ³ : Fin (succ (succ a))
   Ξ³ = Cases (≀-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc m) ⟧)
        (Ξ» (l : ⟦ p 𝟎 ⟧ ≀ ⟦ p (suc m) ⟧) β†’ suc m)
        (Ξ» otherwise β†’ 𝟎)

   Ξ³β‚€ : p 𝟎 ≀ p (suc m) β†’ Ξ³ ＝ suc m
   Ξ³β‚€ = {!!}

   γ₁ : Β¬ (p 𝟎 ≀ p (suc m)) β†’ Ξ³ ＝ 𝟎
   γ₁ = {!!}


   h : (y : Fin (succ (succ a))) β†’ p y ≀ p Ξ³
   h 𝟎 = l
    where
     l : p 𝟎 ≀ p Ξ³
     l = Cases (≀-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc m) ⟧)
          (Ξ» (l : p 𝟎 ≀ p (suc m)) β†’ transport (Ξ» - β†’ p 𝟎 ≀ p -) ((Ξ³β‚€ l)⁻¹) l)
          (Ξ» otherwise β†’ {!!})
   h (suc x) = l
    where
     l : p (suc x) ≀ p Ξ³
     l = {!!}
 -}

\end{code}

This version of argmin and argmax assumes a compact domain and a
finite type of outcomes.

\begin{code}

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))


\end{code}

Added 11th September 2024. Simplified and more efficient version for
the boolean-valued case.

\begin{code}

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               ∎)

\end{code}

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.

\begin{code}

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

\end{code}

By taking the opposite order, we can use ArgMin to compute ArgMax:

\begin{code}

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

\end{code}

We now define a single module that reexports ArgMin and ArgMax
together:

\begin{code}

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

\end{code}

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.

\begin{code}

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)

\end{code}

The main technical result of this module is the following relation
between argmin and min':

\begin{code}

  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

\end{code}

We do the same for ArgMax by taking the opposite order.

\begin{code}

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

\end{code}

And now we combine ArgMin' and ArgMax' in a single module that
reexports them.

\begin{code}

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

\end{code}