Proving a simple list function applied four times is the identity

Question

The following video contains a mathematical card trick due to Colm Mulcahy: https://www.youtube.com/watch?v=dHzUQnRjbuM

The key operation in the trick is defined as follows:

COAT (Count Out And Transfer)

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.

(Definition taken from http://graphics8.nytimes.com/packages/pdf/crossword/Mulcahy_Mathematical_Card_Magic-Sample2.pdf)

In Haskell:

coat k cards = (drop k cards) ++ (reverse . take k $ cards)

Example:

Main> take 5 $ iterate (coat 3) [1..5]

[[1,2,3,4,5],[4,5,3,2,1],[2,1,3,5,4],[5,4,3,1,2],[1,2,3,4,5]]

A characteristic property of the COAT operation is that after 4 iterations, the list returns to its original order, iff k >= n/2.

Is it practical to prove this property for the Haskell code? Would a proof require the use of dependent types to express the constraint on k? (Maybe Idris would be a better language?)

(I'm not sure how to deal with iteration in a proof. I guess in this case the four iterations could just be unrolled.)

Answer 1

An SMT solver can handle such a proof for any concrete deck-size. Proving for an arbitrary deck-size n would require induction, which is beyond the capability of automated provers, at least for the time being. (Also, there isn't any out-of-the-box tools that can take an arbitrary Haskell program and do such proofs for you. Liquid Haskell goes far, but I'm not sure if it would be suitable for this purpose.)

Haskell's SBV library allows you to express such problems conveniently, shipping the proof obligations to z3 (or other SMT solvers) for a push-button experience. Here's how one can code your problem using SBV.

First some preliminaries:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import Data.SBV.List

import Prelude hiding (length, take, drop, reverse, (++))

Note the hiding of common functions length/take etc. from Prelude. We'll instead use their symbolic equivalents as provided by Data.SBV.List. (You're going to have to trust SBV that they are faithful implementations of the same, extending them to the domain of symbolic inputs that you can do proofs with.)

As you noted, here's how coat can be defined:

coat :: SymVal a => SInteger -> SList a -> SList a
coat k cards = drop k cards ++ reverse (take k cards)

Aside from the "funky" signature, the definition is the same as you gave, i.e., stereotypical Haskell. The signature "generalizes" from concrete integer/lists to their symbolic counterparts, so we can do a proof on them.

Coating four times can be expressed using regular composition:

fourCoat :: SymVal a => SInteger -> SList a -> SList a
fourCoat k = coat k . coat k . coat k . coat k

Let's represent the deck as a list of integers:

type Deck = SList Integer

Think of SList Integer as [Integer], just one whose contents can be symbolic values. 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 you're trying to establish.

And here's how you can pose your theorem as an SBV query:

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

This part of the code is a bit involved. But we're essentially saying for any arbitrary deck (free "deck"), and any k, if you fourCoat the deck then you get it back intact. The first constraint limit the size of the deck to the given literal value, i.e., we'll be doing the proof for a deck that has exactly n cards in it. The second constraint is exactly what your theorem stipulated, written slightly rearranged to avoid division by 2. Note that k is not fixed: The proof will be valid for any k, subject to the given constraints.

How does this proof fare? Well, it depends on how large n is! Here's a demo with n = 6:

*Main> coatCheck 6
Q.E.D.

This takes about 3 seconds to run on my machine. As you increase n, the solver time will increase; but if you wait long enough either you'll get a proof. (Or run out of memory, depending on your hardware!)

Notice that it's also possible to make the parameter n symbolic as well. While the SMT solver is capable of expressing this, in my experiments I couldn't get any proof whatsoever. (It simply didn't return in a reasonable time.) And I wouldn't expect it to either: As alluded above, such a proof would require induction, and SMT solvers can't handle such problems quite yet.

So, the answer to your question is a qualified yes: If you're willing to squint the right way and do the proof for fixed-sized decks, then yes; there's an automated way to conduct such proofs in Haskell by using an SMT solver as the underlying engine. If you want a proof for an arbitrary n, then you'll have to use a proper theorem prover like Isabelle, Coq, Lean, etc., and of course you will have to program in their native language, and not Haskell. (Though they accept more or less the same family of functional programs, and this particular problem wouldn't be hard to code in any of these tools.)

You can find the entire code for this problem as an example in the SBV distribution.