    -----------------------------------------------------------------------------
    -- |
    -- 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 = SInteger -> SList a -> SList a
    forall a. SymVal a => SInteger -> SList a -> SList a
    drop SInteger
    k SList a
    cards SList a -> SList a -> SList a
    forall a. SymVal a => SList a -> SList a -> SList a
    ++ SList a -> SList a
    forall a. SymVal a => SList a -> SList a
    reverse (SInteger -> SList a -> SList a
    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 = SInteger -> SList a -> SList a
    forall a. SymVal a => SInteger -> SList a -> SList a
    coat SInteger
    k (SList a -> SList a) -> (SList a -> SList a) -> SList a -> SList a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SInteger -> SList a -> SList a
    forall a. SymVal a => SInteger -> SList a -> SList a
    coat SInteger
    k (SList a -> SList a) -> (SList a -> SList a) -> SList a -> SList a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SInteger -> SList a -> SList a
    forall a. SymVal a => SInteger -> SList a -> SList a
    coat SInteger
    k (SList a -> SList a) -> (SList a -> SList a) -> SList a -> SList a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SInteger -> SList a -> SList a
    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 = SymbolicT IO SBool -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove (SymbolicT IO SBool -> IO ThmResult)
    -> SymbolicT IO SBool -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ do
         Deck
    deck :: Deck <- String -> Symbolic Deck
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "deck"
         SInteger
    k            <- String -> Symbolic SInteger
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "k"

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

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