-----------------------------------------------------------------------------
-- |
-- 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 :: forall a. SymVal a => SInteger -> SList a -> SList a
coat SInteger
k SList a
cards = forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
k SList a
cards forall a. SymVal a => SList a -> SList a -> SList a
++ forall a. SymVal a => SList a -> SList a
reverse (forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
k SList a
cards)

-- | COAT 4 times.
fourCoat :: SymVal a => SInteger -> SList a -> SList a
fourCoat :: forall a. SymVal a => SInteger -> SList a -> SList a
fourCoat SInteger
k = forall a. SymVal a => SInteger -> SList a -> SList a
coat SInteger
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => SInteger -> SList a -> SList a
coat SInteger
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => SInteger -> SList a -> SList a
coat SInteger
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SymVal a => SInteger -> SList a -> SList a
coat SInteger
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 :: Integer -> IO ThmResult
coatCheck Integer
n = forall a. Provable a => a -> IO ThmResult
prove forall a b. (a -> b) -> a -> b
$ do
     Deck
deck :: Deck <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"deck"
     SInteger
k            <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"k"

     forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SList a -> SInteger
length Deck
deck forall a. EqSymbolic a => a -> a -> SBool
.== forall a. SymVal a => a -> SBV a
literal Integer
n
     forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SInteger
2forall a. Num a => a -> a -> a
*SInteger
k forall a. OrdSymbolic a => a -> a -> SBool
.>= forall a. SymVal a => a -> SBV a
literal Integer
n

     forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Deck
deck forall a. EqSymbolic a => a -> a -> SBool
.== forall a. SymVal a => SInteger -> SList a -> SList a
fourCoat SInteger
k Deck
deck