
%\documentstyle[11pt,zed]{csart}
\documentstyle{article}

\begin{document}

\sloppy

\def\dotdot{\mathinner{\ldotp\ldotp}}

\section{Problem}

     You will need a box of matches.  Divide the matches into a number of
piles, not necessarily the same number of matches in each pile.
For example, you might lay out:

     7, 5, 4, 7, 6, 19, 3

     You are allowed to pick any of two piles.  If the piles are equal,
put them together to make one pile; if the piles are not equal, take
from the larger the number of matches that are in the smaller and
add them to the smaller.

     Using the example above, if you select the 5 and the 3, you get:

     7, 2, 4, 7, 7, 6, 19, 6\\
If you then select the two piles of 6 you get:

     7, 2, 4, 7, 12, 19\\
If you then select the second 7 and the 19, you get:

     7, 2, 4, 14, 12, 12

     You carry on in this way, repeatedly acting on the piles you got
from your previous action.  Your target is to collect all the matches
into one large pile.  Sometimes that is possible, sometimes it is not.

     For which of the following layouts is it possible to collect
all the matches into one pile?

A. $17, 4, 5, 5, 1, 2, 3, 15, 12$.

B. $17, 4, 5, 5, 9$.

C. $51, 72, 57, 78, 78, 48$.

D. $1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 3, 23$.

(Enigma 648: {\em Piles of Fun},
Keith Austin,
{\em New Scientist}, 11 January 1992).

\section{Solution}

For an array $A$, define
\begin{eqnarray*}
   \mbox{SUM} (A)  & = & \mbox{Sum of elements of } A, \\
   \mbox{GCD} (A)  & = & \mbox{Greatest common divisor of elements of } A, \\
   A/f             & = & \mbox{Array of values } A [i] / f, \\
   \mbox{odds} (A) & = & \{i \, | \, \mbox{odd} (A [i])\},
\end{eqnarray*}
and let $\mbox{move} (x, y)$
implement the pairwise move specified in the problem.  Show
\begin{tabbing}
\hspace{1em} \= \+ \kill
  \{$b = B \land S = \mbox{SUM}(B) \land (\exists e:\mbox{\bf N} \cdot S = 2^e \, \mbox{GCD}(B))$\} \\
  \\
%  \{invariant: \= $\mbox{SUM}(b) = S
%      \land (\exists e:\mbox{\bf N} \cdot S = 2^e \, \mbox{GCD}(b))$, \+ \\
%      bound: \' $ S / \mbox{GCD} (b) +  |\mbox{odds} (b / \mbox{GCD} (b))| - 2$\} \- \\
  \{invariant $I$: $\mbox{SUM}(b) = S
      \land (\exists e:\mbox{\bf N} \cdot S = 2^e \, \mbox{GCD}(b))$\} \\
  \{bound $t$: $S / \mbox{GCD} (b) +  |\mbox{odds} (b / \mbox{GCD} (b))| - 2$\} \\
  {\bf do} $\mbox{GCD} (b) < \mbox{SUM} (b)$ $\rightarrow$ \= 
		      Choose ($i$, $\mbox{odds} (b / \mbox{GCD} (b))$) ; \+ \\
		      Choose ($j$, $\mbox{odds} (b / \mbox{GCD} (b)) - \{i\}$) ; \\
		      move ($b [i]$, $b [j]$) \- \\
  {\bf od} \\
  \\
  \{$\exists i:0\dotdot n-1 \cdot \forall j:0\dotdot n-1 \cdot ((i = j \Rightarrow b [j] = S) \land (i \neq j \Rightarrow b [j] = 0))$\}.
\end{tabbing}
$n$ is the size of the initial array $B$.  $\mbox{Choose}$ selects
an element from a set.  An equivalent bound function is
$(\sum_i \lceil b [i] / 2 \, \mbox{GCD (b)} \rceil) - 1$.

Also, show that if the invariant is true after an arbitrary application
of $\mbox{move}$, it must have been true before:
\begin{displaymath}
\forall i:0\dotdot n-1 \cdot \forall j:0\dotdot n-1 \cdot
  i \neq j \Rightarrow
  (\mbox{wp} (\mbox{``move} (b [i], b [j])\mbox{''}, I) \Rightarrow I)
\end{displaymath}

%% following version is more `procedural' than needs to be.  It does
%% have simpler bound functions.
%\begin{tabbing}
%\hspace{1em} \= \+ \kill
%  \{$b = B \land S = \mbox{SUM}(B) \land (\exists e:\mbox{\bf N} \cdot S = 2^e \, \mbox{GCD}(B))$\} \\
%  $s$, $g$ := SUM ($b$), GCD ($b$) ; \\
%  \{invariant: \= $s = S \land \mbox{SUM}(b) = S \land
%		   (\forall i:0\dotdot n-1\cdot g \, | \, b [i]) \land
%		   (\exists e:\mbox{\bf N}\cdot 2^e g = S)$, \+ \\
%      variant: \' $S - g$\} \- \\
%  {\bf do} $g < s$ $\rightarrow$ \\
%    \hspace{1em} \= \+ \kill
%    \{invariant: \= $\mbox{SUM}(b) = S \land
%		     (\forall i:0\dotdot n-1\cdot g \, | \, b [i]) \land
%		     even (| \mbox{odds} (b / g) |)$, \+ \\
%	variant: \' $| \mbox{odds} (b / g) |$\} \- \\
%    {\bf do} $\mbox{odds} (b / g) \neq \emptyset$ $\rightarrow$ \=
%				Choose ($i$, $\mbox{odds} (b / g)$) ; \+ \\
%				Choose ($j$, $\mbox{odds} (b / g) - \{i\}$) ; \\
%				move ($b [i]$, $b [j]$) \- \\
%    {\bf od} ; \\
%    $g$ := $2g$ \- \\
%  {\bf od} \\
%  \{$\exists i:0\dotdot n-1 \cdot \forall j:0\dotdot n-1 \cdot ((i = j \rightarrow b [j] = S) \land (i \neq j \rightarrow b [j] = 0))$\}.
%\end{tabbing}
%$n$ is the size of the initial array $B$.  $\mbox{Choose}$ selects
%an element from a set.
  
%\begin{tabbing}
%
%\hspace{1em} \= \+ \kill
%  {\bf proc} move (var $x$, $y$) ; \\
%    \hspace{1em} \= \+ \kill
%    {\bf if} \hspace{1em} \= $x \geq y$ $\rightarrow$ $x$, $y$ := $x - y$, $2y$ \+ \\
%                  $\Box$  \' $x \leq y$ $\rightarrow$ $x$, $y$ := $2x$, $y - x$ \- \\
%    {\bf fi} \- \\
%  \\
%  $s$, $g$ := SUM ($b$), GCD ($b$) ; \\
%  {\bf do} $g < s$ $\rightarrow$ \\
%    \hspace{1em} \= \+ \kill
%    {\bf do} $\mbox{odds} (b / g) \neq \emptyset$ $\rightarrow$ \=
%				Choose ($i$, $\mbox{odds} (b / g)$) ; \+ \\
%				Choose ($j$, $\mbox{odds} (b / g) - \{i\}$) ; \\
%				move ($b [i]$, $b [j]$) \- \\
%    {\bf od} ; \\
%    $g$ := $2g$ \- \\
%  {\bf od} \\
%\end{tabbing}
  
\end{document}
