#|
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.
|#

Event: Start with the initial nqthm theory.

; A Mechanical Checking of a Theorem About a Card Trick
;  Robert S. Boyer, May 22, 1991
; This is a formalization, in the Nqthm logic, of a card trick theorem
; that de Bruijn taught Huet, Huet taught Moore, and Moore taught me.
; Mine differs from a treatment of the same problem by Moore in that
; he uses oracles to simulate shuffling, whereas I use a merge
; predicate.
; Here is Moore's statement of the trick:
  ; Suppose you have a deck of cards of even length.  Suppose the cards
  ; alternate between red ones and black ones.  Cut the deck into two
  ; piles, a and b.  Shuffle a and b together.  Then the following is
  ; true of the shuffled deck.  If the bottom-most cards in a and b are
  ; of different color, then when the cards of the shuffled deck are

   ; taken from the top in adjacent pairs, each pair contains a card of
   ; each color.  On the other hand, if the bottom-most cards in a and b
   ; are the same color, the above pairing property holds after rotating
   ; the shuffled deck by one card, i.e., moving the bottom card to the
   ; top.
#| For other references see
The Gilbreath Tick: A Case Study in Axiomatization and Proof Development in the
COQ Proof Assistant, Gerard Huet, Technical Report 1511, INRIA, September,
1991.
M. Gardner, Mathematical Recreation Column, Scientific American, Aug. 1960.,
p. 149, vol. 203, no. 2.
N. Gilbreath, Magnetic Colors, The Linking Ring, 38(5), 1958, p. 60.
|#

; Now on to my formalization.  We first define the six functions
; needed in the statement of the theorem.  The main, all encompassing,
; theorem is stated at the very end, and is named ``all''.
; Intuitively, we imagine that cards are arbitrary objects, but
; numbers are ``red'' and nonnumbers are ``black.''

Definition: opposite-color (x, y) = (((x ∈ N) ∧ (y ∉ N)) ∨ ((y ∈ N) ∧ (x ∉ N)))

Definition: alternating-colors (x) = if (x ≃ nil) ∨ (cdr (x) ≃ nil) then t

else opposite-color (car (x), cadr (x))

∧ alternating-colors (cdr (x)) endif

Definition: paired-colors (x) = if (x ≃ nil) ∨ (cdr (x) ≃ nil) then t

else opposite-color (car (x), cadr (x)) ∧ paired-colors (cddr (x)) endif

Definition: plistp (x)

= if x ≃ nil then x = nil else plistp (cdr (x)) endif

Definition: shufflep (x, y, z) = if z ≃ nil then (x = nil) ∧ (y = nil) ∧ (z = nil)

elseif x ≃ nil then (x = nil) ∧ (y = z) ∧ plistp (y) elseif y ≃ nil then (y = nil) ∧ (x = z) ∧ plistp (x) else ((car (x) = car (z)) ∧ shufflep (cdr (x), y, cdr (z)))

∨ ((car (y) = car (z)) ∧ shufflep (x, cdr (y), cdr (z))) endif

Definition: even-length (l) = if l ≃ nil then t

elseif cdr (l) ≃ nil then f else even-length (cddr (l)) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; That ends the definitions needed to state the final theorem ``all,'' given
; at the end of this file.
; We now proceed to develop 17 auxiliary lemmas to help prove
; ``all.''

Theorem: al->pp alternating-colors (x) → paired-colors (x)

Definition: silly (x, y, z) = if z ≃ nil then t

else list (silly (cddr (x), y, cddr (z)), silly (cdr (x), cdr (y), cddr (z)), silly (x, cddr (y), cddr (z))) endif

Theorem: main (shufflep (x, y, z) ∧ alternating-colors (x) ∧ alternating-colors (y) ∧ listp (x) ∧ listp (y) ∧ opposite-color (car (x), car (y))) → paired-colors (z)

; The closer to a gensym is the name of a lemma, the more boring and
; obvious it is.  As usual in such Nqthm proofs, these tedious lemmas
; are conceived by carefully reading failed Nqthm proofs rather than
; by thinking ahead.  The idea is to prove only those things which are
; suggested by Nqthm failures.

Theorem: f2 (plistp (d) ∧ plistp (c)) → shufflep (c, d, append (c, d))

Theorem: f3 (plistp (d) ∧ plistp (c)) → shufflep (c, d, append (d, c))

Theorem: cdr-append cdr (append (c, d)) = if listp (c) then append (cdr (c), d)

else cdr (d) endif

Theorem: f4 (plistp (w) ∧ shufflep (x, y, z)) → shufflep (x, append (y, w), append (z, w))

Theorem: f5 (plistp (w) ∧ shufflep (x, y, z)) → shufflep (append (x, w), y, append (z, w))

Theorem: trick (listp (x) ∧ listp (y) ∧ shufflep (x, y, z)) → (shufflep (append (cdr (x), list (car (x))), y, append (cdr (z), list (car (z))))

∨ shufflep (x, append (cdr (y), list (car (y))), append (cdr (z), list (car (z)))))

Theorem: car-append car (append (x, y)) = if listp (x) then car (x)

else car (y) endif

Theorem: f12 (alternating-colors (append (c, list (d))) ∧ (¬ opposite-color (d, e))) → alternating-colors (append (c, list (e)))

Theorem: f6 (listp (l) ∧ even-length (l) ∧ alternating-colors (l)) → alternating-colors (append (cdr (l), list (car (l))))

Theorem: g19 (alternating-colors (c) ∧ (car (c) ∈ N) ∧ even-length (c) ∧ (v ∈ N)) → alternating-colors (append (c, list (v)))

Theorem: g20 (alternating-colors (c) ∧ (car (c) ∉ N) ∧ even-length (c) ∧ (v ∉ N)) → alternating-colors (append (c, list (v)))

Theorem: fap (shufflep (x, y, z) ∧ alternating-colors (x) ∧ alternating-colors (y) ∧ even-length (x) ∧ even-length (y) ∧ (¬ opposite-color (car (x), car (y)))) → paired-colors (append (cdr (z), list (car (z))))

Theorem: al2 (alternating-colors (append (x, y)) ∧ even-length (append (x, y)) ∧ (¬ opposite-color (car (x), car (y)))) → (even-length (x) ∧ even-length (y))

Theorem: g16 (¬ alternating-colors (x)) → (¬ alternating-colors (append (x, y)))

Theorem: g17 (¬ alternating-colors (y)) → (¬ alternating-colors (append (x, y)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; That ends the intermediate development of auxiliary lemmas.  We are now
; ready for the main result.

Theorem: all (alternating-colors (append (x, y)) ∧ even-length (append (x, y)) ∧ shufflep (x, y, z) ∧ listp (x) ∧ listp (y)) → if opposite-color (car (x), car (y)) then paired-colors (z)

else paired-colors (append (cdr (z), list (car (z)))) endif

; To run this list of events takes about 1 hour of cpu time on a
; Sun-3/280.  To develop this list of events took about 15 hours of
; work.

Index

al->pp, 3 al2, 5 all, 5 alternating-colors, 2–5

car-append, 4 cdr-append, 4

even-length, 3–5

f12, 4 f2, 4 f3, 4 f4, 4 f5, 4 f6, 4 fap, 5

g16, 5 g17, 5 g19, 4 g20, 5

main, 3

opposite-color, 2–5

paired-colors, 2, 3, 5 plistp, 2–4

shufflep, 3–5 silly, 3

trick, 4