| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.Lists.CountOutAndTransfer
Description
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 Source #
Count-out-and-transfer (COAT): Take k cards from top, reverse it,
and put it at the bottom of a deck.
type Deck = SList Integer Source #
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 Source #
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 6Q.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.