Martin Escardo, Paulo Oliva, 2-27 July 2021

Example: Tic-tac-toe. We have three versions. The other versions are
in other files.

TODO. Organaze this module better, following the organization of TicTacToe0.

\begin{code}

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



module Games.TicTacToe1 where

open import Fin.ArgMinMax
open import Fin.Topology
open import Fin.Type
open import MLTT.Athenian
open import MLTT.Spartan hiding (J)
open import TypeTopology.CompactTypes
open import TypeTopology.SigmaDiscreteAndTotallySeparated
open import UF.DiscreteAndSeparated

πŸ› : Type
πŸ› = Fin 3

open import Games.FiniteHistoryDependent πŸ›
open import Games.Constructor πŸ›
open import Games.J

tic-tac-toe₁ : Game
tic-tac-toe₁ = build-Game draw Board transition 9 boardβ‚€
 where
  data Player : Type where
   X O : Player

  opponent : Player β†’ Player
  opponent X = O
  opponent O = X

  pattern X-wins = 𝟎
  pattern draw   = 𝟏
  pattern O-wins = 𝟐

  value : Player β†’ πŸ›
  value X = X-wins
  value O = O-wins

  Grid   = πŸ› Γ— πŸ›
  Matrix = Grid β†’ Maybe Player
  Board  = Player Γ— Matrix

\end{code}

Convention: in a board (p , A), p is the opponent of the the current player.

\begin{code}

  wins : Player β†’ Matrix β†’ Bool
  wins p A = line || col || diag
   where
    _is_ : Maybe Player β†’ Player β†’ Bool
    Nothing is _ = false
    Just X  is X = true
    Just O  is X = false
    Just X  is O = false
    Just O  is O = true

    infix 30 _is_

    lβ‚€ = A (𝟎 , 𝟎) is p && A (𝟎 , 𝟏) is p && A (𝟎 , 𝟐) is p
    l₁ = A (𝟏 , 𝟎) is p && A (𝟏 , 𝟏) is p && A (𝟏 , 𝟐) is p
    lβ‚‚ = A (𝟐 , 𝟎) is p && A (𝟐 , 𝟏) is p && A (𝟐 , 𝟐) is p

    cβ‚€ = A (𝟎 , 𝟎) is p && A (𝟏 , 𝟎) is p && A (𝟐 , 𝟎) is p
    c₁ = A (𝟎 , 𝟏) is p && A (𝟏 , 𝟏) is p && A (𝟐 , 𝟏) is p
    cβ‚‚ = A (𝟎 , 𝟐) is p && A (𝟏 , 𝟐) is p && A (𝟐 , 𝟐) is p

    dβ‚€ = A (𝟎 , 𝟎) is p && A (𝟏 , 𝟏) is p && A (𝟐 , 𝟐) is p
    d₁ = A (𝟎 , 𝟐) is p && A (𝟏 , 𝟏) is p && A (𝟐 , 𝟎) is p

    line = lβ‚€ || l₁ || lβ‚‚
    col  = cβ‚€ || c₁ || cβ‚‚
    diag = dβ‚€ || d₁

  Grid-is-discrete : is-discrete Grid
  Grid-is-discrete = Γ—-is-discrete Fin-is-discrete Fin-is-discrete

  Grid-compact : is-Compact Grid {𝓀₀}
  Grid-compact = Γ—-is-Compact Fin-Compact Fin-Compact

  boardβ‚€ : Board
  boardβ‚€ = X , (Ξ» _ β†’ Nothing)

  Move : Board β†’ Type
  Move (_ , A) = Ξ£ g κž‰ Grid , A g ＝ Nothing

  Move-decidable : (b : Board) β†’ is-decidable (Move b)
  Move-decidable (_ , A) = Grid-compact
                            (Ξ» g β†’ A g ＝ Nothing)
                            (Ξ» g β†’ Nothing-is-isolated' (A g))

  Move-compact : (b : Board) β†’ is-Compact (Move b)
  Move-compact (x , A) = complemented-subset-of-compact-type
                          Grid-compact
                          (Ξ» g β†’ Nothing-is-isolated' (A g))
                          (Ξ» g β†’ Nothing-is-h-isolated' (A g))

  open J-definitions πŸ›

  selection : (b : Board) β†’ Move b β†’ J (Move b)
  selection b@(X , A) m p = pr₁ (compact-argmax p (Move-compact b) m)
  selection b@(O , A) m p = pr₁ (compact-argmin p (Move-compact b) m)

  update : (p : Player) (A : Matrix)
         β†’ Move (p , A)
         β†’ Matrix
  update p A (m , _) m' = f (Grid-is-discrete m m')
   where
    f : is-decidable (m ＝ m') β†’ Maybe Player
    f (inl _) = Just p
    f (inr _) = A m

  play : (b : Board) β†’ Move b β†’ Board
  play (p , A) m = opponent p , update p A m

  transition : Board β†’ πŸ› + (Ξ£ M κž‰ Type , (M β†’ Board) Γ— J M)
  transition b@(p , A) = f b (wins p A)
   where
    f : (b : Board)
      β†’ Bool
      β†’ πŸ› + (Ξ£ M κž‰ Type , (M β†’ Board) Γ— J M)
    f (p , A) true  = inl (value p)
    f b       false = Cases (Move-decidable b)
                       (Ξ» (m : Move b)
                             β†’ inr (Move b ,
                                    play b ,
                                    selection b m))
                       (Ξ» (Ξ½ : is-empty (Move b))
                             β†’ inl draw)

t₁ : πŸ›
t₁ = optimal-outcome tic-tac-toe₁

\end{code}

The above computation takes too long, due to the use of brute-force
search. A more efficient one is in another file.