#|
Copyright (C) 1994 by Sakthi Subramanian.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Sakthi Subramanian PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT
SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER
EXPRESS OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE SCRIPT IS
WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Sakthi Subramanian BE LIABLE TO YOU FOR ANY
DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL
OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE
THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING
RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF
YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR FOR ANY
CLAIM BY ANY OTHER PARTY.
|#

A Mechanically Checked Proof of the Mutilated Checkerboard Theorem

Sakthi Subramanian

Here is a formalization of the nxn mutilated checkerboard problem using Bob Boyer’s representation. I later learnt that Herb Simon uses a similar trick in discussing a solution to a “Cube-brick problem”. Our formalization allows us to prove by induction that every sequence of domino-placements leads to a state in which the number of covered black and white squares are equal. However, in the mutilated board the number of black and white squares are not equal and hence it cannot be covered completely. An interesting feature is the definition of the color predicates in terms of the representation of the squares. White squares are those whose coordinates sum up to an even number and black squares are those whose coordinates sum upto an odd number. We prove the theorem for a nxn board using mathematical induction.

REPRESENTATION:

We label the squares by their coordinates with (0,0) being the upper left hand corner and (n,n) being the diagonally opposite square. Thus, there are n+1 rows and columns in the board. If n=7, we are talking about the usual 8x8 checkerboard with the rows and columns numbered from 0 through 7. More generally, when n is odd, the number of rows and columns is even and vice versa. We use [0..m, 0..n] as our notation for a board whose rows are numbered from 0 through m and whose columns are numbered from 0 through n. Event: Start with the initial nqthm theory.

A square is represented by a pair cons (x, y) where x and y are its coordinates.

Definition: squarep (x) = (listp (x) ∧ (car (x) ∈ N) ∧ (cdr (x) ∈ N))

A domino is a pair of adjacent squares. Two squares are adjacent if one of their coordinates is the same and the other coordinate differs by one. Our predicate is true provided the sum of the coordinates of the first argument is less than that of the second argument. Thus, our definition is asymmetric but this will do: there is no loss of generality.

Definition: adjp (s1 , s2 ) = (((car (s1 ) = car (s2 )) ∧ ((1 + cdr (s1 )) = cdr (s2 )))

∨ ((cdr (s1 ) = cdr (s2 )) ∧ ((1 + car (s1 )) = car (s2 ))))

A square x in a [0..n,0..n] board is a pair of coordinates each less than or equal to n.

Definition: squarenp (x, n) = (squarep (x) ∧ (car (x) ≤ n) ∧ (cdr (x) ≤ n))

Dominoes are adjacent pairs of squares that fall within the board.

Definition: dominop (x, n) = (squarenp (car (x), n) ∧ squarenp (cdr (x), n) ∧ adjp (car (x), cdr (x)))

Square-listp recognizes a list of squares.

Definition: square-listp (x) = if x ≃ nil then t

else squarep (car (x)) ∧ square-listp (cdr (x)) endif

A board state is a list of covered squares.

Definition: board-statep (x) = square-listp (x)

Having modeled all possible states of all possible checkerboards let us move on to actions. There is exactly one action: place a domino with the preconditions that the squares of the domino should not be already covered. We don’t have to check if the dominoes fall within the board because the dominop definition takes care of it.

The state got as a result of placing a domino x on a board in state s is given by the following function. If the preconditions of the action are not satisfied then it returns a non-board-statep whose car is 'failed. This “error” state is returned when other actions are performed on it. Thus, a legal domino placement action is one that results in a board state.

Definition: res-place (x, s) = if (car (x) ∈ s) ∨ (cdr (x) ∈ s)

then list ('failed, 'place, x, s)

else cons (car (x), cons (cdr (x), s)) endif

Definition: result (a, s) = if car (s) = 'failed then s

else res-place (cadr (a), s) endif

The state got from s as a result of executing a list of actions l is given by the following function.

Definition: resultlist (l, s) = if l ≃ nil then s

else resultlist (cdr (l), result (car (l), s)) endif

A constructor for the action is given below.

Definition: place (x) = list ('place, x)

The following are predicates on domino-placement actions and sequences of them.

Definition: placep (x, n) = dominop (cadr (x), n)

Definition: place-planp (x, n) = if x ≃ nil then t

else placep (car (x), n) ∧ place-planp (cdr (x), n) endif

To express the theorem, we need a predicate on states in which all squares except the corner squares (0,0) and (n,n) are covered. We write functions to generate the set of all squares on the board and then delete the two corner squares from the set.

Make-row constructs the set of all squares in the row numbered m from columns 0 through n.

Definition: make-row (m, n) = if n ≃ 0 then list (cons (m, 0))

else append (make-row (m, n − 1), list (cons (m, n))) endif

Make-all-rows constructs the set of squares in rows 0 through m and columns 0 through n.

Definition: make-all-rows (m, n) = if m ≃ 0 then make-row (0, n)

else append (make-all-rows (m − 1, n), make-row (m, n)) endif

The following function deletes the first occurrence of x in l.

Definition: delete (x, l) = if l ≃ nil then l

elseif x = car (l) then cdr (l)

else cons (car (l), delete (x, cdr (l))) endif

A mutilated [0..n,0..n] board includes all squares in rows 0 through n except the squares '(0 . 0) and cons (n, n).

Definition: mutilated-board (n) = delete (cons (n, n), delete ('(0 . 0), make-all-rows (n, n)))

Definition: set-equal (l1 , l2 ) = if l1 ≃ nil then l2 ≃ nil

else (car (l1 ) ∈ l2 )

∧ set-equal (cdr (l1 ), delete (car (l1 ), l2 )) endif

A state in which all squares of the mutilated [0..n,0..n] board are covered is given by the following predicate.

Definition: all-covered-except-cornerp (x, n) = set-equal (x, mutilated-board (n))

A white square is one whose coordinates add up to an even number. Otherwise it is a black square. Predicates on white and black squares are given below.

Definition: oddp (x) = ((x mod 2) = 1)

Definition: whitep (x) = (((car (x) + cdr (x)) mod 2) = 0)

Definition: blackp (x) = (((car (x) + cdr (x)) mod 2) = 1)

The following functions compute the number of white and black squares in a state.

Definition: nwhite (x) = if x ≃ nil then 0

elseif whitep (car (x)) then 1 + nwhite (cdr (x))

else nwhite (cdr (x)) endif

Definition: nblack (x) = if x ≃ nil then 0

elseif blackp (car (x)) then 1 + nblack (cdr (x))

else nblack (cdr (x)) endif

THE PROOF.

What is the impossibility argument? In the desired state the number of covered white squares is not equal to number of covered black squares. Every placement operation covers exactly one white square and one black square. Thus, all states reachable starting with a state in which there are no dominoes on the board have an equal number of covered white and black squares. Ergo the desired state is unachievable.

First we show that make-all-rows (n, n) has an equal number of white and black squares when n is odd (theorem eq-bw-board1) and that the number of white squares = number of black squares + 1 when n is even (theorem white-one-plus-black2). The lemmas appearing before them were needed for the proofs.

Theorem: add-before-sub1 (x ≥ 2) → ((1 + (x − 2)) = ((1 + x) − 2))

Odd numbers succeed even numbers. Theorem: odd-succeed-even1 ((n mod 2) = 0) → (((1 + n) mod 2) = 1) Theorem: move-1-out (m + (1 + n)) = (1 + (m + n))

If a square is white then the next square is black. Theorem: black-follows-white1 whitep (cons (m, n)) → blackp (cons (m, 1 + n))

Even numbers succeed odd numbers. Theorem: even-succeed-odd1 ((n mod 2) = 1) → (((1 + n) mod 2) = 0)

The square next to a black square is white. Theorem: white-follows-black1 blackp (cons (m, n)) → whitep (cons (m, 1 + n)) Theorem: odd-even1 ((n mod 2) ≠ 0) → ((n mod 2) = 1)

The following is the base case of the lemma that the number of white squares equals the number of black squares in a row with an even number of squares. Theorem: expand-make-row1 make-row (m, 1) = list (cons (m, 0), cons (m, 1)) Theorem: equal-bw-row-base0 nwhite (make-row (m, 1)) = nblack (make-row (m, 1)) Theorem: t5 ((y mod 2) ≠ 1) → (((1 + y) mod 2) = 1) Theorem: append-assoc append (append (l1 , l2 ), l3 ) = append (l1 , append (l2 , l3 )) Theorem: t6 (n ≥ 2) → (make-row (m, n)

= append (make-row (m, n − 2), list (cons (m, n − 1), cons (m, n))))

The number of white/black squares obtained on appending two lists is the sum of the number of white/black squares of the individual lists.

Theorem: nwhite-append1 nwhite (append (l1 , l2 )) = (nwhite (l1 ) + nwhite (l2 ))

Theorem: nblack-append1 nblack (append (l1 , l2 )) = (nblack (l1 ) + nblack (l2 ))

In each row of a chess board [0..m,0..n] where n is odd, the number of black squares is equal to the number of white squares.

Theorem: equal-bw-row1 oddp (n) → (nwhite (make-row (m, n)) = nblack (make-row (m, n)))

In an entire [0..m,0..n] board, n odd, there are an equal number of white and black squares.

Theorem: eq-bw-board1 oddp (n) → (nwhite (make-all-rows (m, n)) = nblack (make-all-rows (m, n)))

Instantiating m as n in the above we get the following.

Theorem: eq-bw-board oddp (n) → (nwhite (make-all-rows (n, n)) = nblack (make-all-rows (n, n)))

Now we prove that the number of white squares = number of black squares + 1 in a board with an odd number of rows and columns (theorem white-one-plus-black2). The following are intermediate lemmas needed for the proof.

Definition: evenp (x) = ((x mod 2) = 0)

Theorem: zero-ident (m + 0) = fix (m)

The number of white squares of an even numbered row with an odd number of columns is equal to the number of black squares + 1.

Theorem: white-one-plus-black (evenp (m) ∧ evenp (n)) → (nwhite (make-row (m, n)) = (1 + nblack (make-row (m, n))))

Theorem: black-one-plus-white (oddp (m) ∧ evenp (n)) → (nblack (make-row (m, n)) = (1 + nwhite (make-row (m, n))))

Theorem: l13 make-all-rows (1, n) = append (make-row (0, n), make-row (1, n))

Theorem: l14 evenp (n) → (nwhite (make-all-rows (1, n)) = nblack (make-all-rows (1, n)))

Theorem: base2 (nwhite (make-row (0, n)) + nwhite (make-row (1, n))) = (nblack (make-row (0, n)) + nblack (make-row (1, n)))

Theorem: l15 (m > 0) → ((nwhite (make-row (m − 1, n)) + nwhite (make-row (m, n)))

= (nblack (make-row (m − 1, n)) + nblack (make-row (m, n))))

Theorem: t61 (m ≥ 2) → (make-all-rows (m, n)

= append (make-all-rows (m − 2, n), append (make-row (m − 1, n), make-row (m, n))))

Theorem: l16 ((x1 + y1 + z1 ) = (x1 + y2 + z2 )) = ((y1 + z1 ) = (y2 + z2 ))

In a [0..m,0..n] checkerboard in which m is odd, the number of black squares is equal to the number of white squares.

Theorem: eq-bw-board2 oddp (m) → (nwhite (make-all-rows (m, n)) = nblack (make-all-rows (m, n)))

Theorem: l17 (evenp (m) ∧ (m > 0)) → (((m − 1) mod 2) = 1)

The following function is introduced to force Nqthm to chose the appropriate induction scheme for theorem white-one-plus-black2. A hint to induct on m according to the recursive structure of f1 was given.

Definition: f1 (x) = if x ≃ 0 then t

else f1 (x − 1) endif

If the number of rows and columns of a checkerboard is odd then the number of white squares in the board is 1 greater than the number of black squares.

Theorem: white-one-plus-black2 (evenp (m) ∧ evenp (n)) → (nwhite (make-all-rows (m, n)) = (1 + nblack (make-all-rows (m, n))))

Having established that the number of white squares is equal to the number of black squares in a board with an even number of rows and columns and that the number of white squares is 1 greater than the number of black squares in a board with an odd number of rows and columns, we would like to show that in a mutilated board the number of white squares is less than the number of black squares. This is proved as theorem mut3 below. The lemmas preceding it are intermediate lemmas needed for the proof.

Theorem: t7 (n ∈ N) → (cons (m, n) ∈ make-row (m, n))

Theorem: t8 (x ∈ l2 ) → (x ∈ append (l1 , l2 ))

Theorem: m1 ((n ∈ N) ∧ (m ∈ N)) → (cons (m, n) ∈ make-all-rows (m, n))

If we delete a white square from a list then the number of white squares in the new list is less than that in the old list.

Theorem: white-delete ((x ∈ l) ∧ whitep (x)) → (nwhite (delete (x, l)) < nwhite (l))

The (n,n) square is white.

Theorem: white1 whitep (cons (n, n))

Deleting a white square does not change the number of black squares.

Theorem: black-same1 whitep (x) → (nblack (delete (x, l)) = nblack (l))

Deleting '(0 . 0) and cons (n, n) does not change the number of black squares in a list since both of them are white.

Theorem: black-del1 nblack (delete (cons (n, n), delete ('(0 . 0), x))) = nblack (x)

Theorem: mut-l2 oddp (n) → (n ≠ 0)

Theorem: mem-del1 ((x ∈ l) ∧ (x ≠ y)) → (x ∈ delete (y, l))

Theorem: m2 '(0 . 0) ∈ make-all-rows (m, n)

Theorem: mut-l1 oddp (n) → (cons (n, n) ∈ delete ('(0 . 0), make-all-rows (n, n)))

In a mutilated board with an even number of rows and columns the number of white squares is less than the number of black squares.

Theorem: mut1 (oddp (n) ∧ (x = mutilated-board (n))) → (nwhite (x) < nblack (x))

In a mutilated board with an odd number of rows and columns, the number of white squares is less than the number of black squares.

Theorem: mut2 (evenp (n) ∧ (x = mutilated-board (n)) ∧ (n > 0)) → (nwhite (x) < nblack (x))

In any mutilated board the number of white squares is less than the number of black squares.

Theorem: mut3 ((x = mutilated-board (n)) ∧ (n > 0)) → (nwhite (x) < nblack (x))

The following shows what a mutilated board looks like for n = 7.

Theorem: mutboard7 mutilated-board (7)

= '((0 . 1)
(0 . 2)
(0 . 3)
(0 . 4)
(0 . 5)
(0 . 6)
(0 . 7)
(1 . 0)
(1 . 1)
(1 . 2)
(1 . 3)
(1 . 4)
(1 . 5)
(1 . 6)
(1 . 7)
(2 . 0)
(2 . 1)
(2 . 2)
(2 . 3)

(2 . 4)
(2 . 5)
(2 . 6)
(2 . 7)
(3 . 0)
(3 . 1)
(3 . 2)
(3 . 3)
(3 . 4)
(3 . 5)
(3 . 6)
(3 . 7)
(4 . 0)
(4 . 1)
(4 . 2)
(4 . 3)
(4 . 4)
(4 . 5)
(4 . 6)
(4 . 7)
(5 . 0)
(5 . 1)
(5 . 2)
(5 . 3)
(5 . 4)
(5 . 5)
(5 . 6)
(5 . 7)
(6 . 0)
(6 . 1)
(6 . 2)
(6 . 3)
(6 . 4)
(6 . 5)
(6 . 6)
(6 . 7)
(7 . 0)
(7 . 1)
(7 . 2)
(7 . 3)
(7 . 4)
(7 . 5)
(7 . 6))

We will now use mut3 to show that in all states satisfying all-covered-except-cornerp the number of white squares is less than the number of black squares. This is proved as theorem unequal3 below. We need some more lemmas for the proof because all-covered-except-cornerp checks for set equality by deleting squares in two given lists.

Deleting a non-white element from a list of white squares does not alter the number of white squares.

Theorem: white-same1 (¬ whitep (x)) → (nwhite (delete (x, l)) = nwhite (l))

Theorem: white-del1 ((x ∈ l) ∧ whitep (x)) → (nwhite (l) = (1 + nwhite (delete (x, l))))

If two sets of squares are equal then the number of white/black squares in them are equal.

Theorem: nwhite-eq1 set-equal (l1 , l2 ) → (nwhite (l1 ) = nwhite (l2 ))

Theorem: black-same2 (¬ blackp (x)) → (nblack (delete (x, l)) = nblack (l))

Theorem: black-del2 ((x ∈ l) ∧ blackp (x)) → (nblack (l) = (1 + nblack (delete (x, l))))

Theorem: nblack-eq1 set-equal (l1 , l2 ) → (nblack (l1 ) = nblack (l2 ))

If all the squares except the corner ones are covered in a board state then the number of white squares covered is less than the number of covered black squares.

Theorem: unequal1 (evenp (n) ∧ (n > 0) ∧ board-statep (x) ∧ all-covered-except-cornerp (x, n)) → (nwhite (x) < nblack (x))

Theorem: unequal2 (oddp (n) ∧ board-statep (x) ∧ all-covered-except-cornerp (x, n)) → (nwhite (x) < nblack (x))

Theorem: unequal3 ((n > 0) ∧ board-statep (x) ∧ all-covered-except-cornerp (x, n)) → (nwhite (x) < nblack (x))

Now we want to show that the number of covered white squares is equal to the number of covered black squares in every state that arises starting with an initial state when there are no dominoes on the board. This is proved as theorem bcequal1. This in turn uses theorem bw-equal2 which says that the number of covered black and white squares remain equal when a domino is placed on a board legally.

First we need some more number theory: If the sum of two numbers is even then adding one to one of the numbers will make the sum odd and vice versa.

Theorem: t10 ((1 + w) + z) = (1 + (w + z))

Theorem: t11 (x + 1 + y) = (1 + (x + y))

A domino covers exactly one white square and one black square.

Theorem: domino-white1 dominop (x, n) → (nwhite (cons (car (x), cons (cdr (x), y))) = (1 + nwhite (y)))

Theorem: domino-black1 dominop (x, n) → (nblack (cons (car (x), cons (cdr (x), y))) = (1 + nblack (y)))

If a domino is placed on a board then the new board state will have the two squares under the domino covered.

Theorem: place-dom1 (board-statep (s) ∧ placep (a, n) ∧ board-statep (result (a, s))) → (result (a, s) = cons (caadr (a), cons (cdadr (a), s)))

If the number of covered black and white squares in a state are equal then they remain the same after a legal domino placement.

Theorem: bw-equal2 (board-statep (s) ∧ (nwhite (s) = nblack (s)) ∧ placep (a, n) ∧ board-statep (result (a, s))) → (nwhite (result (a, s)) = nblack (result (a, s)))

The following lemmas are need to show that if the number of covered white and black squares are equal in a state then they will remain equal after every legal sequence of domino-placement actions.

First we prove that executing an action sequence in an error state results in the error state.

Theorem: failed-state1 (car (s) = 'failed) → (car (resultlist (p, s)) = 'failed)

Theorem: res2 (board-statep (s) ∧ placep (a, n) ∧ (¬ board-statep (result (a, s)))) → (car (result (a, s)) = 'failed)

Theorem: s1 (car (s) = 'failed) → (¬ board-statep (s))

Theorem: res3 (board-statep (s) ∧ place-planp (p, n) ∧ listp (p) ∧ board-statep (resultlist (p, s))) → board-statep (result (car (p), s))

The following function is used to force the prover to choose the correct induction scheme for the theorem bcequal1.

Definition: foo (s, p) = if p ≃ nil then nil

else foo (result (car (p), s), cdr (p)) endif

If the number of covered white and black squares is equal in a state and a sequence of legal domino placement operations is executed then the number of covered white and black squares would be equal in the resulting state.

Theorem: bcequal1 (board-statep (s) ∧ (nwhite (s) = nblack (s)) ∧ place-planp (p, n) ∧ board-statep (resultlist (p, s))) → (nwhite (resultlist (p, s)) = nblack (resultlist (p, s)))

The final theorem: Starting with an initial state s of an [0..n,0..n] board, n greater than 0, in which there are no covered squares there is no sequence of actions that will result in a state in which all the squares except (0,0) and (n,n) are covered.

Theorem: tough-nut (place-planp (p, n) ∧ (n > 0) ∧ (s1 = resultlist (p, nil)) ∧ board-statep (s1 )) → (¬ all-covered-except-cornerp (s1 , n))

Index

add-before-sub1, 7 adjp, 3, 4 all-covered-except-cornerp, 6, 13, 15 append-assoc, 7

base2, 9 bcequal1, 15 black-del1, 10 black-del2, 13 black-follows-white1, 7 black-one-plus-white, 8 black-same1, 10 black-same2, 13 blackp, 6, 7, 13 board-statep, 4, 13–15 bw-equal2, 14

delete, 5, 6, 10, 11, 13 domino-black1, 14 domino-white1, 14 dominop, 4, 5, 14

eq-bw-board, 8 eq-bw-board1, 8 eq-bw-board2, 9 equal-bw-row-base0, 7 equal-bw-row1, 8 even-succeed-odd1, 7 evenp, 8, 9, 11, 13 expand-make-row1, 7

f1, 9 failed-state1, 15 foo, 15

l13, 8 l14, 9 l15, 9 l16, 9 l17, 9

m1, 10 m2, 10 make-all-rows, 5, 6, 8–11 make-row, 5, 7–10 mem-del1, 10 move-1-out, 7 mut-l1, 11 mut-l2, 10 mut1, 11 mut2, 11 mut3, 11 mutboard7, 11 mutilated-board, 5, 6, 11

nblack, 6–11, 13–15 nblack-append1, 8 nblack-eq1, 13 nwhite, 6–11, 13–15 nwhite-append1, 8 nwhite-eq1, 13

odd-even1, 7

odd-succeed-even1, 7 oddp, 6, 8–11, 13

place, 5

place-dom1, 14 place-planp, 5, 15 placep, 5, 14, 15

res-place, 4 res2, 15 res3, 15 result, 4, 14, 15 resultlist, 4, 15

s1, 15

set-equal, 6, 13 square-listp, 4 squarenp, 3, 4 squarep, 3, 4

t10, 14 t11, 14 t5, 7 t6, 7 t61, 9 t7, 10 t8, 10 tough-nut, 15

unequal1, 13 unequal2, 13 unequal3, 13

white-del1, 13 white-delete, 10 white-follows-black1, 7 white-one-plus-black, 8 white-one-plus-black2, 9 white-same1, 13 white1, 10 whitep, 6, 7, 10, 13

zero-ident, 8