#|
 Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.
 NO WARRANTY
 Computational Logic, Inc. 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 Computational Logic, Inc. 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 solution to the Gilbreath card trick challenge.
;; Matt Kaufmann, 10/92.
;; The proof splits into two halves.  The lemma main-1 handles the
;; case in which we do not make the final adjustment of rotating one
;; card.  The lemma main-2 handles the other case.  We glue these
;; together in the final theorem, main.

Event: Start with the initial nqthm theory.

Definition: length (x) = if listp (x) then 1 + length (cdr (x))

else 0 endif

;; The following definition takes an arbitrary `oracle', which says
;; whether the next card in the shuffle comes from the left pile or
;; the right pile.  See below for the definition of shuffle-top,
;; which makes the `move one card' adjustment when necessary.

Definition: shuffle (left, right, oracle) = if left ≃ nil then right

elseif right ≃ nil then left

elseif car (oracle)

then cons (car (left), shuffle (cdr (left), right, cdr (oracle)))

else cons (car (right), shuffle (left, cdr (right), cdr (oracle))) endif

;; To be really arbitrary, we postulate a color function that takes
;; two values (which might as well be booleans), using the
;; conservative CONSTRAIN principle to make this postulation.

Conservative Axiom: color-intro truep (color (x)) ∨ falsep (color (x))

Simultaneously, we introduce the new function symbol color.

Definition: same-color (x, y) = (color (x) ↔ color (y))

Definition: altp (pile) = if listp (pile)

then if listp (cdr (pile))

then if same-color (car (pile), cadr (pile)) then f

else altp (cdr (pile)) endif else t endif

else t endif

Definition: last (x) = if listp (x) ∧ listp (cdr (x)) then last (cdr (x))

else car (x) endif

Definition: butlast (x) = if listp (x) ∧ listp (cdr (x)) then cons (car (x), butlast (cdr (x)))

else nil endif

Definition: shuffle-top (left, right, oracle) = let shuf be shuffle (left, right, oracle)

in

if ¬ same-color (last (left), last (right)) then shuf else cons (last (shuf ), butlast (shuf )) endif endlet Definition: even-length-p-rec (x) = if listp (x) then ¬ even-length-p-rec (cdr (x))

else t endif

Theorem: even-length-p-rec-rewrite (listp (x) ∧ altp (x)) → (even-length-p-rec (x) = (¬ same-color (car (x), last (x))))

Theorem: even-length-p-rec-append even-length-p-rec (append (x, y)) = (even-length-p-rec (x) ↔ even-length-p-rec (y))

;; A conditional rewrite rule with hypothesis
;; (and (listp x) (listp y)) would probably suffice for most of the
;; proof, but I believe that this version is needed somewhere late in
;; the proof.

Theorem: altp-append altp (append (x, y)) = (altp (x)

∧ altp (y)

∧ ((listp (x) ∧ listp (y)) → (¬ same-color (last (x), car (y)))))

;; Probably the following lemma isn't needed till the end, but let's
;; make sure that we can prove it.  Once we know this to be true,
;; we'll use it implicitly by adding in the hypothesis
;; (not (same-color (car left) (car right))) to main-1 (and similarly
;; for main-2).

Theorem: last-same-color-iff-first-same-color (listp (left) ∧ listp (right) ∧ altp (append (left, right)) ∧ even-length-p-rec (append (left, right))) → (same-color (last (left), last (right))

↔ same-color (car (left), car (right)))

;; Here is the induction scheme we use for main-1, and in fact also
;; for main-2 (actually main-2-lemma).

Definition: main-1-induction (left, right, oracle) = if (left ≃ nil) ∨ (right ≃ nil) then t

elseif car (oracle) then if cadr (oracle)

then main-1-induction (cddr (left), right, cddr (oracle))

else main-1-induction (cdr (left), cdr (right), cddr (oracle)) endif elseif cadr (oracle) then main-1-induction (cdr (left), cdr (right), cddr (oracle)) else main-1-induction (left, cddr (right), cddr (oracle)) endif

Definition: alt2-p (x) = if listp (x)

then if listp (cdr (x))

then (¬ same-color (car (x), cadr (x))) ∧ alt2-p (cddr (x))

else f endif else t endif

Theorem: altp-implies-alt2-p altp (x) → (alt2-p (x) = even-length-p-rec (x))

Theorem: last-append listp (y) → (last (append (x, y)) = last (y))

;; Now we may prove a version of the first half.

Theorem: main-1 (listp (left) ∧ listp (right) ∧ even-length-p-rec (append (left, right)) ∧ altp (left) ∧ altp (right) ∧ (¬ same-color (car (left), car (right))) ∧ (¬ same-color (last (left), last (right)))) → alt2-p (shuffle (left, right, oracle))

;; For the other half, we modify the notion of alt2-p (calling the
;; result by the weird name alt3-p), except that we expect an odd
;; number of cards.  Our strategy is to first prove that in the second
;; case, the CDR of the shuffle has this alt3-p property
;; (main-2-lemma).  Then we can show that when we move the final card
;; of the shuffle to the top, the result is an alt2-p.  The lemma
;; alt3-p-to-alt2-p below lets us do that little adjustment, once we
;; know (by the lemma shuffle-preserves-reds-equal-blacks) that the

;; shuffle has the property that the numbers of red and black cards in
;; it are the same.

Definition: alt3-p (x) = if listp (x)

then if listp (cdr (x))

then (¬ same-color (car (x), cadr (x))) ∧ alt3-p (cddr (x)) else t endif

else f endif

;; The following lemma is analogous to one proved for main-1; then the
;; proof of main-2-lemma goes through.

Theorem: altp-implies-alt3-p altp (x) → (alt3-p (x) = (¬ even-length-p-rec (x)))

Theorem: main-2-lemma (listp (left) ∧ listp (right) ∧ even-length-p-rec (append (left, right)) ∧ altp (left) ∧ altp (right) ∧ same-color (car (left), car (right)) ∧ same-color (last (left), last (right))) → alt3-p (cdr (shuffle (left, right, oracle)))

Definition: count-color (color, x) = if listp (x)

then if color = color (car (x)) then 1 + count-color (color, cdr (x))

else count-color (color, cdr (x)) endif else 0 endif

Definition: reds-equal-blacks (x) = (count-color (t, x) = count-color (f, x))

Theorem: alt-implies-reds-equal-blacks altp (x) → if even-length-p-rec (x) then count-color (t, x) = count-color (f, x)

elseif color (car (x)) then count-color (t, x)

= (1 + count-color (f, x))

else (1 + count-color (t, x)) = count-color (f, x) endif Theorem: count-color-shuffle count-color (color, shuffle (x, y, oracle)) = (count-color (color, x) + count-color (color, y))

Theorem: shuffle-preserves-reds-equal-blacks (altp (append (x, y)) ∧ even-length-p-rec (append (x, y))) → reds-equal-blacks (shuffle (x, y, oracle))

Theorem: alt3-p-to-alt2-p (reds-equal-blacks (cons (a, x)) ∧ alt3-p (x)) → alt2-p (cons (last (x), butlast (cons (a, x))))

Theorem: shuffle-cdr (listp (x) ∧ listp (y)) → (listp (shuffle (x, y, oracle)) ∧ listp (cdr (shuffle (x, y, oracle))))

Theorem: main-2 (listp (left) ∧ listp (right) ∧ even-length-p-rec (append (left, right)) ∧ altp (left) ∧ altp (right) ∧ altp (append (left, right)) ∧ same-color (car (left), car (right)) ∧ same-color (last (left), last (right))) → alt2-p (shuffle-top (left, right, oracle))

;; The following three events are there simply to show that our
;; definition of ``even length'' is honest.

Definition: even-length-p (x) = ((length (x) mod 2) = 0)

Theorem: remainder-2-add1 (((1 + x) mod 2) = 0) = ((x mod 2) ≠ 0)

Theorem: even-length-p-is-even-length-p-rec even-length-p (x) = even-length-p-rec (x)

Theorem: main (listp (left) ∧ listp (right) ∧ even-length-p (append (left, right)) ∧ altp (append (left, right))) → alt2-p (shuffle-top (left, right, oracle))

Index

alt-implies-reds-equal-blacks, 5 alt2-p, 4, 6 alt3-p, 5, 6 alt3-p-to-alt2-p, 6 altp, 2–6 altp-append, 3 altp-implies-alt2-p, 4 altp-implies-alt3-p, 5

butlast, 2, 6

color, 2, 5 color-intro, 2 count-color, 5, 6 count-color-shuffle, 6

even-length-p, 6 even-length-p-is-even-length-p-

rec, 6 even-length-p-rec, 3–6 even-length-p-rec-append, 3 even-length-p-rec-rewrite, 3

last, 2–6 last-append, 4 last-same-color-iff-first-same-

color, 3 length, 1, 6

main, 6 main-1, 4 main-1-induction, 3, 4 main-2, 6 main-2-lemma, 5

reds-equal-blacks, 5, 6 remainder-2-add1, 6

same-color, 2–6 shuffle, 2, 4–6 shuffle-cdr, 6 shuffle-preserves-reds-equal-bl

acks, 6 shuffle-top, 2, 6