Martin Escardo, Paulo Oliva, 27th November 2024 - 14th May 2025

We define optimal moves and optimal plays for sequential games. Then
using the JT monad, with T the monad List⁺ of non-empty lists, we
compute all optimal plays of a game, provided it has ordinary
selection functions.

\begin{code}

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

open import MLTT.Spartan hiding (J)
open import UF.FunExt
open import UF.DiscreteAndSeparated

\end{code}

We work with a type of outcomes R with decidable equality (called
discreteness).

\begin{code}

module Games.OptimalPlays
        (fe : Fun-Ext)
        (R  : Type)
        (R-is-discrete : is-discrete R)
       where

open import Games.FiniteHistoryDependent R
open import Games.TypeTrees
open import MLTT.List hiding ([_]) renaming (map to lmap)
open import MonadOnTypes.J-transf-variation
open import MonadOnTypes.JK
open import MonadOnTypes.K
open import MonadOnTypes.List
open import MonadOnTypes.Monad
open import MonadOnTypes.NonEmptyList
open import Notation.CanonicalMap
open import UF.Base

open K-definitions R

\end{code}

The following are the main two notions considered in this file.

\begin{code}

is-optimal-move : {X : Type} {Xf : X → 𝑻}
                  (q : (Σ x ꞉ X , Path (Xf x)) → R)
                  (ϕ : K X)
                  (ϕf : (x : X) → 𝓚 (Xf x))
                → X
                → Type
is-optimal-move {X} {Xf} q ϕ ϕf x =
 optimal-outcome (game (X ∷ Xf) q (ϕ :: ϕf))
 ＝ optimal-outcome (game (Xf x) (subpred q x) (ϕf x))

is-optimal-play : {Xt : 𝑻} → 𝓚 Xt → (Path Xt → R) → Path Xt → Type
is-optimal-play {[]}     ⟨⟩        q ⟨⟩        = 𝟙
is-optimal-play {X ∷ Xf} (ϕ :: ϕf) q (x :: xs) =
   is-optimal-move {X} {Xf} q ϕ ϕf x
 × is-optimal-play {Xf x} (ϕf x) (subpred q x) xs

\end{code}

We now show that the strategic path of a strategy in subgame perfect
equilibrium is an optimal play. We start with a lemma that is
interesting on its own right.

\begin{code}

optimal-play-gives-optimal-outcome
 : {Xt : 𝑻}
   (ϕt : 𝓚 Xt)
   (q : Path Xt → R)
   (xs : Path Xt)
 → is-optimal-play {Xt} ϕt q xs
 → q xs ＝ optimal-outcome (game Xt q ϕt)
optimal-play-gives-optimal-outcome {[]}     ⟨⟩        q ⟨⟩        ⟨⟩ = refl
optimal-play-gives-optimal-outcome {X ∷ Xf} (ϕ :: ϕf) q (x :: xs) (o :: of)
 = subpred q x xs                                     ＝⟨ IH ⟩
   optimal-outcome (game (Xf x) (subpred q x) (ϕf x)) ＝⟨ o ⁻¹ ⟩
   optimal-outcome (game (X ∷ Xf) q (ϕ :: ϕf))        ∎
 where
  IH : subpred q x xs ＝ optimal-outcome (game (Xf x) (subpred q x) (ϕf x))
  IH = optimal-play-gives-optimal-outcome {Xf x} (ϕf x) (subpred q x) xs of

strategic-path-is-optimal-play
 : {Xt : 𝑻}
   (ϕt : 𝓚 Xt)
   (q : Path Xt → R)
   (σ : Strategy Xt)
 → is-in-sgpe ϕt q σ
 → is-optimal-play ϕt q (strategic-path σ)
strategic-path-is-optimal-play {[]} ⟨⟩ q ⟨⟩ ⟨⟩ = ⋆
strategic-path-is-optimal-play {X ∷ Xf} ϕt@(ϕ :: ϕf) q σ@(x₀ :: σf) ot@(o :: of)
 = I , IH x₀
 where
  IH : (x : X) → is-optimal-play (ϕf x) (subpred q x) (strategic-path (σf x))
  IH x = strategic-path-is-optimal-play {Xf x} (ϕf x) (subpred q x) (σf x) (of x)

  I : is-optimal-move q ϕ ϕf x₀
  I = optimal-outcome (game (X ∷ Xf) q (ϕ :: ϕf))                  ＝⟨ refl ⟩
      sequenceᴷ {X ∷ Xf} (ϕ :: ϕf) q                               ＝⟨ refl ⟩
      ϕ (λ x → sequenceᴷ (ϕf x) (subpred q x))                     ＝⟨ refl ⟩
      ϕ (λ x → optimal-outcome (game (Xf x) (subpred q x) (ϕf x))) ＝⟨ I₁ ⟩
      ϕ (λ x → subpred q x (strategic-path (σf x)))                ＝⟨ o ⁻¹ ⟩
      q (strategic-path σ)                                         ＝⟨ refl ⟩
      subpred q x₀ (strategic-path (σf x₀))                        ＝⟨ I₂ ⟩
      optimal-outcome (game (Xf x₀) (subpred q x₀) (ϕf x₀))        ∎
       where
        I₀ : (x : X)
           → optimal-outcome (game (Xf x) (subpred q x) (ϕf x))
           ＝ subpred q x (strategic-path (σf x))
        I₀ x = (optimal-play-gives-optimal-outcome
                 (ϕf x) (subpred q x) (strategic-path (σf x)) (IH x))⁻¹

        I₁ = ap ϕ (dfunext fe I₀)
        I₂ = optimal-play-gives-optimal-outcome
              (ϕf x₀) (subpred q x₀) (strategic-path (σf x₀)) (IH x₀)

\end{code}

We now proceed to compute the non-empty list of all optimal plays of a
game, under suitable assumptions on the game.

The algebras of the nonempty list monad 𝕃⁺ are the semigroups
(associative magmas). We work with the magma structure on R defined by
x · y = x. Concretely, this amounts to the following construction.

\begin{code}

𝓐 : Algebra 𝕃⁺ R
𝓐 = record {
     structure-map = head⁺ ;
     aunit = u ;
     aassoc = a
    }
 where
  u : head⁺ ∘ η 𝕃⁺ ∼ id
  u r = refl

  a : head⁺ ∘ ext 𝕃⁺ (η 𝕃⁺ ∘ head⁺) ∼ head⁺ ∘ ext 𝕃⁺ id
  a ((((r ∷ _) , _) ∷ _) , _) = refl

open T-definitions 𝕃⁺
open α-definitions 𝕃⁺ R 𝓐
open JT-definitions 𝕃⁺ R 𝓐 fe
open JK R

\end{code}

Ordinary selection functions are of type J X := (X → R) → X. Here we
work with JT defined as follows.

\begin{code}

JT-remark : JT ＝ λ X → (X → R) → List⁺ X
JT-remark = by-definition

\end{code}

Every algebra α of any monad T induces an extension operator α­extᵀ,
which for the case T = List⁺ with the algebra defined above is
characterized as follows.

\begin{code}

α-extᵀ-explicitly : {X : Type} (p : X → R) (t : List⁺ X)
                  → α-extᵀ p t ＝ p (head⁺ t)
α-extᵀ-explicitly p ((x ∷ _) :: _) = refl

\end{code}

We now construct a JT-selection function ε⁺ from an ordinary
J-selection function ε that attains a quantifier ϕ, for any listed
type X with at least one element.

Recall that we say that a type is listed⁺ if it has a distinguished
element and a list of all its elements (which will automatically
include the distinguished element).

\begin{code}

module _ (X : Type)
         (X-is-listed⁺@(x₀ , xs , μ) : listed⁺ X)
         (ϕ : (X → R) → R)
         (ε : (X → R) → X)
         (ε-attains-ϕ : ε attains ϕ)
      where

 private
  A : (X → R) → X → Type
  A p x = p x ＝ ϕ p

  δA : (p : X → R) (x : X) → is-decidable (A p x)
  δA p x = R-is-discrete (p x) (ϕ p)

  εᴸ :  (X → R) → List X
  εᴸ p = filter (A p) (δA p) xs

  ε-member-of-εᴸ : (p : X → R) → member (ε p) (εᴸ p)
  ε-member-of-εᴸ p = filter-member← (A p) (δA p) (ε p) xs (ε-attains-ϕ p) (μ (ε p))

  εᴸ-is-non-empty : (p : X → R) → is-non-empty (εᴸ p)
  εᴸ-is-non-empty p = lists-with-members-are-non-empty (ε-member-of-εᴸ p)

 ε⁺ : JT X
 ε⁺ p = εᴸ p , εᴸ-is-non-empty p

 εᴸ-property→ : (p : X → R) (x : X) → member x (εᴸ p) → p x ＝ ϕ p
 εᴸ-property→ p x = filter-member→ (A p) (δA p) x xs

 εᴸ-property← : (p : X → R) (x : X) → p x ＝ ϕ p → member x (εᴸ p)
 εᴸ-property← p x e = filter-member← (A p) (δA p) x xs e (μ x)

\end{code}

We now extend this to trees of selection functions that attain
quantifiers.

\begin{code}

𝓙𝓣 : 𝑻 → Type
𝓙𝓣 = structure JT

εt⁺ : (Xt : 𝑻)
    → structure listed⁺ Xt
    → (ϕt : 𝓚 Xt)
    → (εt : 𝓙 Xt)
    → εt Attains ϕt
    → 𝓙𝓣 Xt
εt⁺ [] ⟨⟩ ⟨⟩ ⟨⟩ ⟨⟩ = ⟨⟩
εt⁺ (X ∷ Xf) (l :: lf) (ϕ :: ϕf) (ε :: εf) (a :: af) =
 ε⁺ X l ϕ ε a :: (λ x → εt⁺ (Xf x) (lf x) (ϕf x) (εf x) (af x))

open List⁺-definitions

\end{code}

We now prove a couple of technical lemmas.

\begin{code}

module _ {X : Type} {Xf : X → 𝑻}
         (e⁺ : JT X)
         (d⁺ : (x : X) → JT (Path (Xf x)))
         (q : Path (X ∷ Xf)  → R)
       where

 private
  g : (x : X) → T (Path (Xf x))
  g x = d⁺ x (subpred q x)

  f : X → R
  f x = α-extᵀ (subpred q x) (g x)

  xt : T X
  xt = e⁺ f

  x : X
  x = head⁺ xt

  xs : Path (Xf x)
  xs = head⁺ (g x)

 head⁺-of-⊗ᴶᵀ : head⁺ ((e⁺ ⊗ᴶᵀ d⁺) q) ＝ x :: xs
 head⁺-of-⊗ᴶᵀ =
  head⁺ ((e⁺ ⊗ᴶᵀ d⁺) q)                                         ＝⟨ I ⟩
  head⁺ (xt ⊗ᴸ⁺ g)                                              ＝⟨ II ⟩
  head⁺ (concat⁺ (lmap⁺ (λ x → lmap⁺ (λ y → x :: y) (g x)) xt)) ＝⟨ III ⟩
  head⁺ (head⁺ (lmap⁺ (λ x → lmap⁺ (λ y → x :: y) (g x)) xt))   ＝⟨ IV ⟩
  head⁺ (lmap⁺ (head⁺ xt ::_) (g (head⁺ xt)))                   ＝⟨ refl ⟩
  head⁺ (lmap⁺ (x ::_) (g x))                                   ＝⟨ V ⟩
  x :: head⁺ (g x)                                              ＝⟨ refl ⟩
  x :: xs                                                       ∎
   where
    I   = ap head⁺ (⊗ᴶᵀ-in-terms-of-⊗ᵀ e⁺ d⁺ q fe)
    II  = ap head⁺ (⊗ᴸ⁺-explicitly fe (e⁺ f) g)
    III = head⁺-of-concat⁺ (lmap⁺ (λ x → lmap⁺ (λ y → x :: y) (g x)) xt)
    IV  = ap head⁺ (head⁺-of-lmap⁺ (λ x → lmap⁺ (λ y → x :: y) (g x)) xt)
    V   = head⁺-of-lmap⁺ (x ::_) (g x)

JT-in-terms-of-K : (Xt : 𝑻)
                   (ϕt : 𝓚 Xt)
                   (q : Path Xt → R)
                   (εt : 𝓙 Xt)
                   (at : εt Attains ϕt)
                   (lt : structure listed⁺ Xt)
                 → α-extᵀ q (path-sequence 𝕁𝕋 (εt⁺ Xt lt ϕt εt at) q)
                 ＝ path-sequence (𝕂 R) ϕt q
JT-in-terms-of-K [] ϕt q εt at lt = refl
JT-in-terms-of-K Xt@(X ∷ Xf) ϕt@(ϕ :: ϕf) q εt@(ε :: εf) at@(a :: af) lt@(l :: lf) = II
 where
  d⁺ : (x : X) → JT (Path (Xf x))
  d⁺ x = path-sequence 𝕁𝕋 (εt⁺ (Xf x) (lf x) (ϕf x) (εf x) (af x))

  f : (x : X) → List⁺ (Path (Xf x))
  f x = d⁺ x (subpred q x)

  p : X → R
  p x = α-extᵀ (subpred q x) (f x)

  IH : (x : X) → p x ＝ path-sequence (𝕂 R) (ϕf x) (subpred q x)
  IH x = JT-in-terms-of-K (Xf x) (ϕf x) (subpred q x) (εf x) (af x) (lf x)

  e⁺ : JT X
  e⁺ = ε⁺ X l ϕ ε a

  x : X
  x = head⁺ (e⁺ p)

  I : member x (ι (e⁺ p))
  I = head⁺-is-member (e⁺ p)

  II = α-extᵀ q ((e⁺ ⊗ᴶᵀ d⁺) q)                           ＝⟨ II₀ ⟩
       q (head⁺ ((e⁺ ⊗ᴶᵀ d⁺) q))                          ＝⟨ II₁ ⟩
       q (x :: head⁺ (f x))                               ＝⟨ II₂ ⟩
       p x                                                ＝⟨ II₃ ⟩
       ϕ p                                                ＝⟨ II₄ ⟩
       ϕ (λ x → path-sequence (𝕂 R) (ϕf x) (subpred q x)) ＝⟨ refl ⟩
       (ϕ ⊗[ 𝕂 R ] (λ x → path-sequence (𝕂 R) (ϕf x))) q  ∎
        where
         II₀ = α-extᵀ-explicitly q ((e⁺ ⊗[ 𝕁𝕋 ] d⁺) q)
         II₁ = ap q (head⁺-of-⊗ᴶᵀ e⁺ d⁺ q)
         II₂ = (α-extᵀ-explicitly (subpred q x) (f x))⁻¹
         II₃ = εᴸ-property→ X l ϕ ε a p x I
         II₄ = ap ϕ (dfunext fe IH)

\end{code}

We now show that path-sequence 𝕁𝕋 computes the non-empty list of all
optimal plays.

\begin{code}

main-lemma→ : (Xt : 𝑻)
              (ϕt : 𝓚 Xt)
              (q : Path Xt → R)
              (εt : 𝓙 Xt)
              (at : εt Attains ϕt)
              (lt : structure listed⁺ Xt)
              (xs : Path Xt)
            → member xs (ι (path-sequence 𝕁𝕋 (εt⁺ Xt lt ϕt εt at) q))
            → is-optimal-play ϕt q xs
main-lemma→ [] ⟨⟩ q ⟨⟩ ⟨⟩ ⟨⟩ ⟨⟩ in-head = ⟨⟩
main-lemma→ Xt@(X ∷ Xf) ϕt@(ϕ :: ϕf) q εt@(ε :: εf) at@(a :: af)
            lt@(l :: lf) (x :: xs) m =
 head-is-optimal-move , tail-is-optimal-play
 where
  e⁺ : JT X
  e⁺ = ε⁺ X l ϕ ε a

  d⁺ : (x : X) → JT (Path (Xf x))
  d⁺ x = path-sequence 𝕁𝕋 (εt⁺ (Xf x) (lf x) (ϕf x) (εf x) (af x))

  t : List⁺ X
  t = τ e⁺ d⁺ q

  tf : (x : X) → T (Path (Xf x))
  tf x = d⁺ x (subpred q x)

  p : X → R
  p x = path-sequence (𝕂 R) (ϕf x) (subpred q x)

  p' : X → R
  p' x = α-extᵀ
          (subpred q x)
          (path-sequence 𝕁𝕋
            (εt⁺ (Xf x) (lf x) (ϕf x) (εf x) (af x))
            (subpred q x))

  I : path-sequence 𝕁𝕋 (εt⁺ Xt lt ϕt εt at) q ＝ t ⊗ᴸ⁺ tf
  I = ⊗ᴶᵀ-in-terms-of-⊗ᵀ e⁺ d⁺ q fe

  II : member (x :: xs) (ι (t ⊗ᴸ⁺ tf))
  II = transport (member (x :: xs)) (ap ι I) m

  III : member x (ι t)
  III = pr₁ (split-membership fe x xs t tf II)

  IV : member xs (ι (tf x))
  IV = pr₂ (split-membership fe x xs t tf II)

  V : p' ∼ p
  V x = JT-in-terms-of-K (Xf x) (ϕf x) (subpred q x) (εf x ) (af x) (lf x)

  VI : t ＝ e⁺ p
  VI = ap e⁺ (dfunext fe V)

  VII : member x (ι (e⁺ p))
  VII = transport (λ - → member x (ι -)) VI III

  head-is-optimal-move =
   ϕ p                                      ＝⟨ VIII ⟩
   p x                                      ＝⟨ refl ⟩
   path-sequence (𝕂 R) (ϕf x) (subpred q x) ∎
    where
     VIII = (εᴸ-property→ X l ϕ ε a p x VII)⁻¹

  IH : member xs (ι (tf x))
     → is-optimal-play (ϕf x) (subpred q x) xs
  IH = main-lemma→ (Xf x) (ϕf x) (subpred q x) (εf x) (af x) (lf x) xs

  tail-is-optimal-play : is-optimal-play (ϕf x) (subpred q x) xs
  tail-is-optimal-play = IH IV

main-lemma← : (Xt : 𝑻)
              (ϕt : 𝓚 Xt)
              (q : Path Xt → R)
              (εt : 𝓙 Xt)
              (at : εt Attains ϕt)
              (lt : structure listed⁺ Xt)
              (xs : Path Xt)
            → is-optimal-play ϕt q xs
            → member xs (ι (path-sequence 𝕁𝕋 (εt⁺ Xt lt ϕt εt at) q))
main-lemma← [] ⟨⟩ q ⟨⟩ ⟨⟩ ⟨⟩ ⟨⟩ ⋆ = in-head
main-lemma← Xt@(X ∷ Xf) ϕt@(ϕ :: ϕf) q εt@(ε :: εf) at@(a :: af)
            lt@(l :: lf) (x :: xs) (om , op) = VI
 where
  p : X → R
  p x = path-sequence (𝕂 R) (ϕf x) (subpred q x)

  e⁺ : JT X
  e⁺ = ε⁺ X l ϕ ε a

  d⁺ : (x : X) → JT (Path (Xf x))
  d⁺ x = path-sequence 𝕁𝕋 (εt⁺ (Xf x) (lf x) (ϕf x) (εf x) (af x))

  t : List⁺ X
  t = τ e⁺ d⁺ q

  tf : (x : X) → T (Path (Xf x))
  tf x = d⁺ x (subpred q x)

  p' : X → R
  p' x = α-extᵀ (subpred q x) (tf x)

  IH : member xs (ι (tf x))
  IH = main-lemma← (Xf x) (ϕf x) (subpred q x) (εf x) (af x) (lf x) xs op

  I : p ＝ p'
  I = dfunext fe
       (λ x → (JT-in-terms-of-K (Xf x) (ϕf x) (subpred q x) (εf x) (af x) (lf x))⁻¹)

  II : p' x ＝ ϕ p'
  II = transport (λ - → - x ＝ ϕ -) I (om ⁻¹)

  III : member x (ι t)
  III = εᴸ-property← X l ϕ ε a p' x II

  IV : member (x :: xs) (ι (t ⊗ᴸ⁺ tf))
  IV = join-membership fe x xs t tf (III , IH)

  V : ι (t ⊗ᴸ⁺ tf) ＝ ι (path-sequence 𝕁𝕋 (εt⁺ Xt lt ϕt εt at) q)
  V = (ap ι (⊗ᴶᵀ-in-terms-of-⊗ᵀ e⁺ d⁺ q fe))⁻¹

  VI : member (x :: xs) (ι (path-sequence 𝕁𝕋 (εt⁺ Xt lt ϕt εt at) q))
  VI = transport (member (x :: xs)) V IV

\end{code}

To conclude, we package the above with a game as a parameter, where
the types of moves are listed, and where we are given attaining
selection functions for the quantifiers.

\begin{code}

module _ (G@(game Xt q ϕt) : Game)
         (Xt-is-listed⁺ : structure listed⁺ Xt)
         (εt : 𝓙 Xt)
         (εt-Attains-ϕt : εt Attains ϕt)
       where

 optimal-plays : List⁺ (Path Xt)
 optimal-plays = path-sequence 𝕁𝕋 (εt⁺ Xt Xt-is-listed⁺ ϕt εt εt-Attains-ϕt) q

 Theorem→ : (xs : Path Xt) → member xs (ι optimal-plays) → is-optimal-play ϕt q xs
 Theorem→ = main-lemma→ Xt ϕt q εt εt-Attains-ϕt Xt-is-listed⁺

 Theorem← : (xs : Path Xt) → is-optimal-play ϕt q xs → member xs (ι optimal-plays)
 Theorem← = main-lemma← Xt ϕt q εt εt-Attains-ϕt Xt-is-listed⁺

\end{code}

This concludes what we wished to construct and prove.

Remark. The assumption Xt-is-listed⁺ implies that the type R of
outcomes has at least one element.

\begin{code}

 r₀ : R
 r₀ = q (head⁺ optimal-plays)

\end{code}

In a previous version of this file, we instead assumed r₀ : R, and we
worked with "listed" instead of "listed⁺", but the listings were
automatically non-empty.