Skip to content

Games.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.


 {-
 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 = {!!}
 -}


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.


module ArgMinMax-Listed
        {𝓀 π“₯ : Universe}
        (R : 𝓀 Μ‡ )
        (_<_ : R β†’ R β†’ π“₯ Μ‡ )
        (Ξ΄ : (r s : R) β†’ is-decidable (r < s))
      where

 open import MLTT.List

 _β‰₯_ _≀_ : R β†’ R β†’ π“₯ Μ‡
 r β‰₯ s = Β¬ (r < s)
 s ≀ r = r β‰₯ s

 private
  min' max' : (r s : R) β†’ is-decidable (r < s) β†’ R

  min' r s (inl lt) = r
  min' r s (inr ge) = s

  max' r s (inl lt) = s
  max' r s (inr ge) = r

 min max : R β†’ R β†’ R
 min r s = min' r s (Ξ΄ r s)
 max r s = max' r s (Ξ΄ r s)

 open import MonadOnTypes.K
 open K-definitions R

 Min Max : {X : 𝓀 Μ‡ } β†’ listed⁺ X β†’ K X
 Min (xβ‚€ , xs , _) p = foldr (Ξ» x β†’ min (p x)) (p xβ‚€) xs
 Max (xβ‚€ , xs , _) p = foldr (Ξ» x β†’ max (p x)) (p xβ‚€) xs

 private
  argmin' argmax' : {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

  argmax' p x y (inl le) = y
  argmax' p x y (inr ge) = x

  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

  argmax'-spec : {X : 𝓀 Μ‡ } (p : X β†’ R) (x y : X) (d : is-decidable (p x < p y))
               β†’ p (argmax' p x y d) ＝ max' (p x) (p y) d
  argmax'-spec p x y (inl lt) = refl
  argmax'-spec p x y (inr ge) = refl


 argmin argmax : {X : 𝓀 Μ‡ } β†’ (X β†’ R) β†’ X β†’ X β†’ X

 argmin p x y = argmin' p x y (Ξ΄ (p x) (p y))
 argmax p x y = argmax' 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))

 argmax-spec : {X : 𝓀 Μ‡ } (p : X β†’ R) (x y : X)
             β†’ p (argmax p x y) ＝ max (p x) (p y)
 argmax-spec p x y = argmax'-spec p x y (Ξ΄ (p x) (p y))

 open import MonadOnTypes.J
 open J-definitions R

 ArgMin ArgMax : {X : 𝓀 Μ‡ } β†’ listed⁺ X β†’ J X
 ArgMin (xβ‚€ , xs , _) p = foldr (argmin p) xβ‚€ xs
 ArgMax (xβ‚€ , xs , _) p = foldr (argmax 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

 ArgMax-spec : {X : 𝓀 Μ‡ } (β„“ : listed⁺ X) β†’ (ArgMax β„“) attains (Max β„“)
 ArgMax-spec {X} (xβ‚€ , xs , m) p = I xs
  where
   I : (xs : List X)
     β†’ p (foldr (argmax p) xβ‚€ xs) ＝ foldr (Ξ» x β†’ max (p x)) (p xβ‚€) xs
   I [] = refl
   I (x ∷ xs) = Iβ‚€
    where
     IH : p (foldr (argmax p) xβ‚€ xs) ＝ foldr (Ξ» x β†’ max (p x)) (p xβ‚€) xs
     IH = I xs

     Iβ‚€ = p (argmax p x (foldr (argmax p) xβ‚€ xs))         ＝⟨ I₁ ⟩
          max (p x) (p (foldr (argmax p) xβ‚€ xs))          ＝⟨ Iβ‚‚ ⟩
          max (p x) (foldr (Ξ» x₁ β†’ max (p x₁)) (p xβ‚€) xs) ∎
           where
            I₁ = argmax-spec p x (foldr (argmax p) xβ‚€ xs)
            Iβ‚‚ = ap (max (p x)) IH