1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.Lists.CountOutAndTransfer
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Lists.CountOutAndTransfer where
import Prelude hiding (length, take, drop, reverse, (++))
import Data.SBV
import Data.SBV.List
-- | Count-out-and-transfer (COAT): Take @k@ cards from top, reverse it,
-- and put it at the bottom of a deck.
coat :: SymVal a => SInteger -> SList a -> SList a
coat k cards = drop k cards ++ reverse (take k cards)
-- | COAT 4 times.
fourCoat :: SymVal a => SInteger -> SList a -> SList a
fourCoat k = coat k . coat k . coat k . coat k
-- | 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.
type Deck = SList Integer
-- | 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.
coatCheck :: Integer -> IO ThmResult
coatCheck n = prove $ do
deck :: Deck <- free "deck"
k <- free "k"
constrain $ length deck .== literal n
constrain $ 2*k .>= literal n
pure $ deck .== fourCoat k deck
|
