Gilbreath's Card Trick

A correctness proof of the famous Gilbreath card trick — with a mathematical lineage from de Bruijn → Huet → Moore → Boyer → Passmore.

Overview

Gilbreath's principle is a remarkable property of card shuffles:

Take a deck of cards where colors alternate (red, black, red, black, ...). Cut the deck into two piles. Riffle shuffle the piles together. Then, when the shuffled deck is taken from the top in adjacent pairs, each pair contains one red and one black card.

This seems almost magical — no matter how the shuffle is performed, the pairing property always holds (provided the bottom cards of the two piles are different colors).

The result has a distinguished history in formal verification: de Bruijn taught Huet the trick, Huet taught Moore, Moore taught Boyer, and Boyer taught Passmore. Each generation formalized it in their proof system of choice.

The Model

Cards and Decks

type color = Red | Black
type deck = color list
 
let opposite_color (x : color) (y : color) = x <> y
 
let rec alternating_colors (x : deck) =
  match x with
  | [] | [_] -> true
  | x :: ((y :: _) as tl) ->
    opposite_color x y && alternating_colors tl
 
let rec paired_colors (x : deck) =
  match x with
  | [] | [_] -> true
  | x :: y :: rst ->
    opposite_color x y && paired_colors rst

Valid Shuffles

A valid shuffle interleaves two decks while preserving the relative order of cards within each pile:

let rec valid_shuffle (x : deck) (y : deck) (z : deck) : bool =
  match x, y, z with
  | [], [], [] -> true
  | [], y, z -> y = z
  | x, [], z -> x = z
  | x1 :: xs, y1 :: ys, z1 :: zs ->
    (x1 = z1 && valid_shuffle xs y zs)
    || (y1 = z1 && valid_shuffle x ys zs)
  | _ -> false
[@@adm x,y]

Computational Exploration

Before attempting the proof, ImandraX can explore the problem computationally. The instance command finds concrete examples of valid shuffles:

instance (fun x y z ->
  List.length z >= 5 && valid_shuffle x y z)
 
instance (fun x y z ->
  List.length z >= 10
  && List.length x >= 5
  && List.length y >= 3
  && valid_shuffle x y z)

These generate concrete shuffles that we can inspect — verifying that the paired-colors property holds in each case and building intuition before the general proof.

Auxiliary Theorems

Two clean lemmas establish that appending piles (without interleaving) always produces a valid shuffle:

theorem f2 x y = valid_shuffle x y (List.append x y)
[@@by auto] [@@rw]
 
theorem f3 x y = valid_shuffle x y (List.append y x)
[@@by auto] [@@rw]

These are proved fully automatically and used as rewrite rules.

Verification

Warm-Up: Alternating Implies Paired

theorem alt_is_paired (x : deck) =
  alternating_colors x ==> paired_colors x
[@@by induct ~on_fun:[%id paired_colors] ()] [@@rewrite]

Custom Induction Scheme

The main theorem requires a custom induction scheme that considers all ways two cards can be drawn from the shuffled result:

let rec wild_induct (x : deck) (y : deck) (z : deck) =
  if z = [] || List.tl z = [] then 1
  else
    let tl x = if x = [] then [] else List.tl x in
    wild_induct (tl @@ tl x) y (List.tl (List.tl z))
    + wild_induct (tl x) (tl y) (List.tl (List.tl z))
    + wild_induct x (tl @@ tl y) (List.tl (List.tl z))
[@@adm z]

This scheme considers three cases for each pair of cards drawn from z: both from x, one from each, or both from y.

The Main Theorem

theorem main x y z =
  valid_shuffle x y z
  && alternating_colors x
  && alternating_colors y
  && x <> []
  && y <> []
  && opposite_color (List.hd x) (List.hd y)
  ==>
  paired_colors z
[@@by induct ~on_fun:[%id wild_induct] ()] [@@timeout 120]

If two non-empty alternating decks with opposite-colored bottom cards are shuffled together, the result is always paired — regardless of how the shuffle is performed.

Results

The proof demonstrates several advanced ImandraX features:

• Custom induction schemes — wild_induct captures a non-obvious recursion pattern needed for the proof
• Parameterized waterfall — induct ~on_fun triggers ImandraX's full waterfall automation using the custom scheme
• Computational exploration — instance queries let us visualize valid shuffles before attempting the proof:

instance (fun x y z ->
  List.length z >= 10
  && List.length x >= 5
  && List.length y >= 3
  && valid_shuffle x y z)

References

• Source: gilbreath.iml
• Norman Gilbreath's original card trick (1958)