Mutilated Chessboard

Combinatorics Classic Problem

The classic proof that a chessboard with two opposite corners removed cannot be tiled by dominoes — formalized as a coloring argument in IML.

Overview

The mutilated chessboard problem is a famous puzzle in combinatorics: take a standard 8×8 chessboard and remove two diagonally opposite corners. Can the remaining 62 squares be covered by 31 dominoes, where each domino covers exactly two adjacent squares?

The answer is no, and the proof is elegant: each domino must cover one black and one white square (since adjacent squares always have different colors), but the two removed corners are the same color, leaving an imbalance.

This proof has been formalized in ImandraX, demonstrating the system's ability to reason about combinatorial structures, list operations, and inductive properties.

The Model

The complete development is self-contained IML you can paste into ImandraX.

Board and Coloring

type square = { x: int; y: int }
type color = Black | White
type domino = square * square
 
let color (p:square) : color =
  if (p.x + p.y) mod 2 = 0 then White else Black
 
let adjacent (p:square) (q:square) =
  (p.x = q.x && abs (p.y - q.y) = 1)
  || (p.y = q.y && abs (p.x - q.x) = 1)
 
eval color {x=0;y=0}
eval color {x=0;y=1}
 
eval adjacent {x=0;y=0} {x=0;y=1}
eval adjacent {x=0;y=0} {x=1;y=1}

Valid Dominoes

A domino is valid if both squares are on the board and they are adjacent:

let valid_n_square (n:int) (p:square) =
  p.x >= 0 && p.x < n
  && p.y >= 0 && p.y < n
 
let valid_domino n (d:domino) =
  let p,q = fst d,snd d in
  valid_n_square n p
  && valid_n_square n q
  && adjacent p q

Domino Placement

A state is a list of covered squares. The step function places a single valid domino, and run applies a sequence of placements:

type state = square list
 
type action = Place of domino
 
let step n (s:state) (a:action) : state option =
    match a with
    | Place ((p,q) as d) ->
      if valid_domino n d && not (List.mem p s || List.mem q s) then
        Some (p :: q :: s)
      else
        None
 
let rec run n (s:state) (acts:action list) =
  match acts with
  | [] -> Some s
  | act::acts ->
    begin match step n s act with
    | Some s' -> run n s' acts
    | None -> None
    end
[@@adm acts]

Color Counting

let rec num_white (s:state) : int =
  match s with
  | [] -> 0
  | x::xs ->
    (if color x = White then 1 else 0)
    + num_white xs
 
let rec num_black (s:state) : int =
    match s with
    | [] -> 0
    | x::xs ->
      (if color x = Black then 1 else 0)
      + num_black xs

Board Construction

The full 8×8 board is constructed row by row:

let rec mk_row y k =
  if k < 0 then []
  else {x=k; y} :: mk_row y (k-1)
 
let rec mk_board y n =
  if y < 0 then []
  else mk_row y n @ mk_board (y-1) n
 
eval mk_row 0 7
eval mk_board 7 7
 
let rec delete a xs =
  match xs with
  | [] -> []
  | x::xs -> if x=a then xs else x :: delete a xs
 
let dim_8x8 = 7 (* 0 ... 7 *)
let empty_board : state = []
let board_covered = mk_board dim_8x8 dim_8x8
 
let mutilated_board =
  delete {x=0;y=0} (delete {x=dim_8x8;y=dim_8x8} board_covered)

The mutilated board removes two opposite white corners from the complete 8×8 board.

Verification

Step 1: Dominoes Cover Opposite Colors

Every valid domino covers one white and one black square:

lemma domino_opposite_colors n (d:domino) =
  valid_domino n d ==> color (fst d) <> color (snd d)
[@@by auto]

Step 2: Single-Step Color Preservation

Each domino placement preserves the balance between white and black squares:

lemma step_color_count s n act =
  num_white s = num_black s
  ==>
  match step n s act with
  | Some s' -> num_white s' = num_black s'
  | None -> true
[@@by auto] [@@rw]

Step 3: Multi-Step Color Preservation

By induction over the entire sequence of placements:

lemma run_color_count n s acts =
  num_white s = num_black s
  ==>
  match run n s acts with
  | Some s' ->
    num_white s' = num_black s'
  | None -> true
[@@by induction ~id:[%id run] ()
  @>>| auto]
[@@disable step]

The @@disable step annotation prevents ImandraX from expanding the step function during induction — it has already been proved correct in step_color_count, so the inductive step only needs to invoke that rewrite rule.

Step 4: Empty Board Has Balanced Colors

lemma run_color_count_from_empty s n acts =
  s=[]
  ==>
  match run n s acts with
  | Some s' ->
    num_white s' = num_black s'
  | None -> true
[@@by [%use run_color_count n [] acts]
   @> auto]
[@@disable step]

Board Size Lemmas

Proving properties about the 8×8 board requires establishing row and board sizes:

lemma len_row y k =
  k >= 0 ==> List.length (mk_row y k) = k + 1
[@@by auto]
 
lemma num_white_append xs ys =
  num_white (xs @ ys) = num_white xs + num_white ys
[@@by auto] [@@rw]
 
lemma num_black_append xs ys =
  num_black (xs @ ys) = num_black xs + num_black ys
[@@by auto] [@@rw]
 
lemma len_board n m =
  n >= 0 && m >= 0
  ==> List.length (mk_board n m) = (n+1) * (m+1)
[@@by induction ()
   @>| [auto;
        lift_ifs
        @>| [swap (-2) @> [%subgoal n=0]
        @>| [[%replace n] @> [%normalize mk_board 0 m]
            @> lift_ifs
            @>| [[%normalize mk_row 0 m]
                @> [%normalize List.length ([]:square list)]
                @> esimp
                @> [%use len_row 0 m]
                @> auto;
            auto];
            arith];
          auto]]]
[@@rw]

This is one of the few proofs in the development that requires manual tactic guidance — the interaction between list append, row lengths, and multiplication requires careful case splitting.

Step 5: The Mutilated Board Is Imbalanced

Both removed corners {x=0;y=0} and {x=7;y=7} are the same color (White), creating an imbalance:

lemma mutilated_color_count =
  num_white mutilated_board
  <> num_black mutilated_board
[@@by auto]

The Main Theorem

Combining the preservation invariant with the imbalance:

theorem main acts =
  match run dim_8x8 empty_board acts with
  | Some covering ->
    covering <> mutilated_board
  | None -> true
[@@by [%use run_color_count_from_empty empty_board dim_8x8 acts]
   @> [%use mutilated_color_count]
   @> auto]

No sequence of valid domino placements on an empty board can ever produce a covering equal to the mutilated board.

Computational Exploration

ImandraX can also find partial coverings computationally:

instance (fun acts ->
  match run dim_8x8 empty_board acts with
  | Some covering ->
    List.length covering = 10
  | None -> false)

This finds a concrete sequence of 5 domino placements covering 10 squares — demonstrating that partial tilings exist, just not complete ones covering the mutilated board.

Results

The proof showcases several ImandraX features:

Induction following function structure — the key lemma uses induction ~id:[%id run] to follow the recursive structure of run
Tactic combinators — @>>| auto maps the auto tactic across all subgoals
Computational verification — eval and instance allow us to check concrete examples before attempting general proofs
Lemma composition — the final theorem combines two previously established lemmas with %use

Elegant Coloring Argument

The classic domino-coloring proof formalized with clean, readable IML.

Inductive Reasoning

Automatic induction following function structure proves the color preservation invariant.

Computational + Deductive

ImandraX seamlessly combines computation (eval, instance) with deductive proof.

References

Source: chessboard.iml