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