Trying to define game of two player and its theor. result

Stream: new members

[Ilmārs Cīrulis]

Tried to write down necessary stuff for formalising the fact that Tic-tac-toe (for example) is a draw.

Right now my attempt seems too complex, but it's the best what I could do tonight. Hopefully all this makes sense.

EDIT: Sneakily edited (new version).

import Mathlib

structure Game where
  position : Type
  turn : position → Bool
  move : position → position → Prop
  move_changes_side : ∀ {p1 p2}, move p1 p2 → turn p1 ≠ turn p2
  leaf_score : ∀ {p}, (∀ p', ¬ move p p') → ℚ

def is_leaf {G : Game} (p : G.position) : Prop :=
  ∀ p', ¬ G.move p p'

def strategy (G : Game) (side : Bool) :=
  ∀ {p}, G.turn p = side → (¬ is_leaf p) → { p' // G.move p p' }

def move_of_strategy {G side} (s : strategy G side) (p1 p2 : G.position): Prop :=
    ∃ (H : G.turn p1 = side) (H0 : ¬ is_leaf p1), p2 = (s H H0).1

inductive game_of_strategies {G} (s1 : strategy G true) (s2 : strategy G false):
  G.position → G.position → Type
| nil : ∀ (x : G.position), is_leaf x → game_of_strategies s1 s2 x x
| cons : ∀ (x y z : G.position),
         (if G.turn x = true then move_of_strategy s1 x y else move_of_strategy s2 x y) →
         game_of_strategies s1 s2 y z → game_of_strategies s1 s2 x z

def length_of_game {G} {s1 : strategy G true} {s2 : strategy G false}
    {p1 p2} (L : game_of_strategies s1 s2 p1 p2) : ℕ :=
  match L with
  | .nil x Hx => 0
  | .cons x _ z Hxy Hyz => 1 + length_of_game Hyz

theorem last_is_leaf {G} {s1 : strategy G true} {s2 : strategy G false} {p p' : G.position} :
    game_of_strategies s1 s2 p p' → is_leaf p' := by
  intros g
  induction g with
  | nil x iH => exact iH
  | cons x y z iH0 iH1 iH2 => exact iH2

structure is_finite (G : Game) where
  end_position : strategy G true → strategy G false → G.position → G.position
  witness_game : ∀ s1 s2 p, game_of_strategies s1 s2 p (end_position s1 s2 p)


def result_of_strategies {G : Game} (HG: is_finite G) (s1 : strategy G true) (s2 : strategy G false)
    (p : G.position) : ℚ :=
  G.leaf_score (last_is_leaf (HG.witness_game s1 s2 p))

structure theoretical_eval_of_position {G : Game} (H : is_finite G) (p : G.position) (sc : ℚ) : Prop where
  score_achievable : ∃ (s1 : strategy G true) (s2 : strategy G false),
                     result_of_strategies H s1 s2 p = sc
  first_cant_improve : ∀ (s1 : strategy G true), ∃ (s2 : strategy G false),
                       result_of_strategies H s1 s2 p ≤ sc
  second_cant_improve : ∀ (s2 : strategy G false), ∃ (s1 : strategy G true),
                        sc ≤ result_of_strategies H s1 s2 p

def given_eval_in_at_most_N_moves {G : Game} (H : is_finite G) (p : G.position) (sc : ℚ) (n : ℕ) : Prop :=
  if G.turn p = true
  then ∃ (s1 : strategy G true), ∀ (s2 : strategy G false),
        let g := H.witness_game s1 s2 p
        let score := G.leaf_score (last_is_leaf g)
        let number_of_moves := length_of_game g
        sc < score ∨ (score = sc ∧ number_of_moves ≤ n)
  else ∃ (s2 : strategy G false), ∀ (s1 : strategy G true),
        let g := H.witness_game s1 s2 p
        let score := G.leaf_score (last_is_leaf g)
        let number_of_moves := length_of_game g
        score < sc ∨ (score = sc ∧ number_of_moves ≤ n)

structure forced_eval_in_N_moves {G : Game} (H : is_finite G) (p : G.position) (sc : ℚ) (n : ℕ) : Prop where
  score_correct : theoretical_eval_of_position H p sc
  number_of_moves_is_least : IsLeast { x | given_eval_in_at_most_N_moves H p sc x } n

[Ilmārs Cīrulis]

Okay, I've finished and now going to look for another people work. (I don't believe I'm the first trying to formalize this.)

[Violeta Hernández]

You might want to check out the #combinatorial-games channel. We haven't done tic-tac-toe yet, but I think we should have all the necessary infrastructure.

[Violeta Hernández]

In fact, if you're interested in proving some tic-tac-toe theorems (e.g. the first player has a winning strategy!), I'd be glad to walk you through our repository and how this might be done.