Documentation.SBV.Examples.Lists.CountOutAndTransfer

Shows that COAT (Count-out-and-transfer) trick preserves order of cards. From pg. 35 of http://graphics8.nytimes.com/packages/pdf/crossword/Mulcahy_Mathematical_Card_Magic-Sample2.pdf:

Given a packet of n cards, COATing k cards refers to counting out that many from the top into a pile, thus reversing their order, and transferring those as a unit to the bottom.

We show that if you COAT 4 times where k is at least n/2 for a deck of size n, then the deck remains in the same order.

Documentation

coat :: SymVal a => SInteger -> SList a -> SList a

Count-out-and-transfer (COAT): Take k cards from top, reverse it, and put it at the bottom of a deck.

fourCoat :: SymVal a => SInteger -> SList a -> SList a

COAT 4 times.

type Deck = SList Integer

A deck is simply a list of integers. Note that a regular deck will have distinct cards, we do not impose this in our proof. That is, the proof works regardless whether we put duplicates into the deck, which generalizes the theorem.

coatCheck :: Integer -> IO ThmResult

Key property of COATing. If you take a deck of size n, and COAT it 4 times, then the deck remains in the same order. The COAT factor, k, must be greater than half the size of the deck size.

Note that the proof time increases significantly with n. Here's a proof for deck size of 6, for all k >= 3.

>>> coatCheck 6
Q.E.D.

It's interesting to note that one can also express this theorem by making n symbolic as well. However, doing so definitely requires an inductive proof, and the SMT-solver doesn't handle this case out-of-the-box, running forever.