A Formality proof that TicTacToe winning lines are isomorphic to the 3x3 magic square.

ticTac15.fm

import Base#

// There are eight possible winning lines in a game of tic-tac-toe
// ----------------
// | 00 | 01 | 02 |
// -----+----+-----
// | 10 | 11 | 12 |
// -----+----+-----
// | 20 | 21 | 22 |
// ----------------

T Line
| l00_02
| l00_20
| l00_22
| l01_21
| l10_12
| l02_20
| l02_22
| l20_22

// There are eight triples of numbers that sum to 15
// 1 + 5 + 9 = 15
// 1 + 6 + 8 = 15
// 2 + 4 + 9 = 15
// 2 + 6 + 7 = 15
// 3 + 4 + 8 = 15
// 3 + 5 + 7 = 15
// 4 + 5 + 6 = 15

T Triple
| t159
| t168
| t249
| t258
| t267
| t348
| t357
| t456

// an isomorphism is a pair of morphisms such that the composistion of morphism
// are equal
T Iso<A, B>
| iso( f : A -> B
     , g : B -> A
     , left : (x : A) -> x == g(f(x))
     , right : (x : B) -> x == f(g(x))
     )

// a left-identity morphism
f(x : Line) : Triple
  case x
  | l00_02 => t159
  | l00_20 => t168
  | l00_22 => t249
  | l01_21 => t258
  | l10_12 => t267
  | l02_20 => t348
  | l02_22 => t357
  | l20_22 => t456

// a right-identity morphism
g(x : Triple) : Line
  case x
  | t159 => l00_02
  | t168 => l00_20
  | t249 => l00_22
  | t258 => l01_21
  | t267 => l10_12
  | t348 => l02_20
  | t357 => l02_22
  | t456 => l20_22

// the left identity property
left(x : Line) : Equal(Line,x,g(f(x)))
  case x
  | l00_02 => equal(__)
  | l00_20 => equal(__)
  | l00_22 => equal(__)
  | l01_21 => equal(__)
  | l10_12 => equal(__)
  | l02_20 => equal(__)
  | l02_22 => equal(__)
  | l20_22 => equal(__)
  : Equal(Line,x,g(f(x)))

right(x : Triple) : Equal(Triple,x,f(g(x)))
  case x
  | t159 => equal(__)
  | t168 => equal(__)
  | t249 => equal(__)
  | t258 => equal(__)
  | t267 => equal(__)
  | t348 => equal(__)
  | t357 => equal(__)
  | t456 => equal(__)
  : Equal(Triple,x,f(g(x)))

ticTac15 : Iso(Line, Triple)
  iso(Line;Triple;f,g,left,right)

// or more concisely
proof : 8n == 8n
  equal(__)