formalizing games

Stream: general

[Arthur Paulino]

This is something that I've been contemplating (and trying) for a few days with no success. I'm trying to understand how "games" can be formalized. I will explain.

By "games" I mean structures that have to obey certain criteria. For instance, the tower of Hanoi is composed by three towers filled by discs such that a larger disc can't be on top of a smaller one. And the other characteristic of a "game" is that we want to travel through states like these in order to reach a certain state (and win).

I'm trying to formalize an old SNES game called Cu-On-Pa. You control a cube with colorful faces and make it roll on a grid. The constraint is that you can't step on a colorful cell unless the color of the top of the cube is the same color as the cell you're stepping on.

My version of the game only has one colorful goal and the grid is infinite. Here's my Lean 4 code:

inductive Face | F1 | F2 | F3 | F4 | F5 | F6
  deriving DecidableEq

open Face

inductive Cube
  | C12 | C13 | C14 | C15
  | C21 | C23 | C24 | C26
  | C31 | C32 | C35 | C36
  | C41 | C42 | C45 | C46
  | C51 | C53 | C54 | C56
  | C62 | C63 | C64 | C65

def Cube.top : Cube → Face
  | C12 => F1 | C13 => F1 | C14 => F1 | C15 => F1
  | C21 => F2 | C23 => F2 | C24 => F2 | C26 => F2
  | C31 => F3 | C32 => F3 | C35 => F3 | C36 => F3
  | C41 => F4 | C42 => F4 | C45 => F4 | C46 => F4
  | C51 => F5 | C53 => F5 | C54 => F5 | C56 => F5
  | C62 => F6 | C63 => F6 | C64 => F6 | C65 => F6

/-                  →      ↑      ←      ↓ -/
abbrev CubeMoves := Cube × Cube × Cube × Cube

def CubeMoves.r (m : CubeMoves) := m.1
def CubeMoves.u (m : CubeMoves) := m.2.1
def CubeMoves.l (m : CubeMoves) := m.2.2.1
def CubeMoves.d (m : CubeMoves) := m.2.2.2

def Cube.moves : Cube → CubeMoves
  | C12 => (C32, C26, C42, C51)
  | C13 => (C53, C36, C23, C41)
  | C14 => (C24, C46, C54, C31)
  | C15 => (C45, C56, C35, C21)
  | C21 => (C41, C15, C31, C62)
  | C23 => (C13, C35, C63, C42)
  | C24 => (C64, C45, C14, C32)
  | C26 => (C36, C65, C46, C12)
  | C31 => (C21, C14, C51, C63)
  | C32 => (C62, C24, C12, C53)
  | C35 => (C15, C54, C65, C23)
  | C36 => (C56, C64, C26, C13)
  | C41 => (C51, C13, C21, C64)
  | C42 => (C12, C23, C62, C54)
  | C45 => (C65, C53, C15, C24)
  | C46 => (C26, C63, C56, C14)
  | C51 => (C31, C12, C41, C65)
  | C53 => (C63, C32, C13, C45)
  | C54 => (C14, C42, C64, C35)
  | C56 => (C46, C62, C36, C15)
  | C62 => (C42, C21, C32, C56)
  | C63 => (C23, C31, C53, C46)
  | C64 => (C54, C41, C24, C36)
  | C65 => (C35, C51, C45, C26)

structure CuOnPa where
  coords     : Int × Int
  target     : Face
  cube       : Cube
  consistent : coords = (0, 0) → cube.top = target

def CuOnPa.isSolved (cop : CuOnPa) : Prop :=
  cop.coords = (0, 0) ∧ cop.cube.top = cop.target

Now I want to prove that any state of the game is solvable, that is, there's always a series of transformations that will take a certain state to another for which isSolved stands.

I'm not looking for a specific answer to this problem. I'm trying to understand the reasoning for formalizing these kinds of problems :pray:

[Bryan Gin-ge Chen]

It's not immediately clear to me what you're having trouble with, but I think you could start by thinking of the set of valid states of a game as the set of vertices of a directed graph and the transitions between valid states as edges between those vertices. Then proving the game is solvable is "just" a matter of proving that there is always a path to a "winning" vertex.

Of course there's not much you can say at this level of generality, you really need to use detailed properties of the game itself to prove that those paths exist. For example, if the game is sufficiently symmetric, you could potentially use that to show the graph is strongly connected simply by constructing a path between one pair of special vertices, etc.

[Arthur Paulino]

My difficulty is constraining the formalism in a way that it's impossible to "cheat". For instance, if I ask for a function that solves the game, one can simply use the CuOnPa constructor and return the winning state independently from the provided state.

I had a similar issue trying to formalize the Hanoi tower. The function that solved the game could just return the solved problem.

[Bhavik Mehta]

I think the restriction you need might be something like: a "solution" function can only provide edges of the directed graph that Bryan talks about, not move along any pair of vertices

[Stuart Presnell]

A solution to the game should be a path from an initial state to a solved state — e.g. in the Tower of Hanoi puzzle, a series of steps from the tower-on-peg-A state to the tower-on-peg-B state.

[Stuart Presnell]

So for example, a solution to the 3-disc problem might look like this:

321, . , .
32, 1, .
3, 1, 2
3, . , 21
. , 3, 21
1, 3, 2
1, 32, .
. , 321, .

[Kevin Buzzard]

Someone on the Discord had some Hanoi code which also did graphics!

[Arthur Paulino]

@Stuart Presnell I was going in that direction:

def mayLeft (cop : CuOnPa) : Prop :=
  cop.coords = (1, 0) → cop.cube.moves.l.top = cop.target

def mayUp (cop : CuOnPa) : Prop :=
  cop.coords = (0, -1) → cop.cube.moves.u.top = cop.target

def mayRight (cop : CuOnPa) : Prop :=
  cop.coords = (-1, 0) → cop.cube.moves.r.top = cop.target

def mayDown (cop : CuOnPa) : Prop :=
  cop.coords = (0, 1) → cop.cube.moves.d.top = cop.target

def goLeft (cop : CuOnPa) (h : cop.mayLeft) : CuOnPa :=
  let newCoords := (cop.coords.fst - 1, cop.coords.snd)
  let newCube := cop.cube.moves.l
  sorry

def goUp (cop : CuOnPa) (h : cop.mayUp) : CuOnPa := sorry

def goRight (cop : CuOnPa) (h : cop.mayRight) : CuOnPa := sorry

def goDown (cop : CuOnPa) (h : cop.mayDown) : CuOnPa := sorry

Then I'd say that a path would be a sequence of applications of those goUp, ... functions and a solution would be a path that would take me to the winning state. But I got stuck because of the hypotheses h that they need. How'd you formalize such path?

[Arthur Paulino]

More generally, how to formalize a path that's valid?

[Arthur Paulino]

(I think I saw the solution just by talking it out :open_mouth: )

[Arthur Paulino]

The issue is that I'm constraining consistency in my structure. Instead, I should allow the instantiation of invalid states have validity check as a prop, then require that every state in the path obeys to it

[Stuart Presnell]

So you could (lazily) build a tree with the starting state as root and the available moves as branches, and then search the tree for a path to a solved state, pruning branches that correspond to invalid moves.