sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
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.

Synopsis

- coat :: SymVal a => SInteger -> SList a -> SList a
- fourCoat :: SymVal a => SInteger -> SList a -> SList a
- type Deck = SList Integer
- coatCheck :: Integer -> IO ThmResult

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

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

COAT 4 times.

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