Permutation Factorization in Coq

The goal of this project is to develop a verified functional implementation of the algorithms by O. Schreier, C. Sims, and T. Minkwitz using Coq. The combined algorithm is able to efficiently give solutions to the permutation word problem: given a group G generated by a set of permutations A, determine if a permutation g lies in G, and if so produce a word in A that is equivalent to g. A short but comprehensive explanation of these algorithms can be found in the following articles: 1, 2. These articles have been archived in the doc folder for future reference.

Puzzles

This is a list of permutation puzzles that can be used as examples. Note that the first three puzzles only work well on computer screens, while the latter three exist as physical objects.

1. Cruzzle I gave this name to a simple kind of turning puzzle. An image is cut into a grid where the rows and columns can revolve around. I found that some small instances, like 3×5, are more difficult than some larger ones.

2. Twiddle This puzzle is part of Simon Tatham's Portable Puzzle Collection, see 3. It manipulates a grid by rotating four adjacent squares. I am curious how its complexity compares to Cruzzle.

3. Inversion This puzzle is part of te same collection as Twiddle, see 4. You can manipulate a grid by inverting a square and all direct neighbors. This puzzle can be solved much more efficiently using row reduction modulo 2.

4. Topspin This puzzle is used as case study in 2. It works by rotating a sequence of numbers and reversing a fixed segment of them. This puzzle could be extended by adding other sequence manipulations.

5. Sliding The classic sliding puzzle is well known. It manipulates a grid by removing one square and then moving adjacent squares into the empty space. The 15 puzzle can be generated by 3-cycles.

6. Rubik Rubik's cube is perhaps the most famous of all permutation puzzles. It can be extended to many scales and dimensions, but in its most elegant form it already has approximately 43 quintillion combinations.

Composing functions versus adding puzzle moves

Applying permutation functions is just like executing moves in a puzzle; they both interchange certain values. But there is an important difference: function composition and puzzle moves are applied in the opposite order! For example, suppose σ and π represent permutations. When applying σ after π, we would write σ ∘ π. Curiously, the way to obtain the same result by executing σ and π as puzzle moves is to first execute σ and then execute π; from left to right! This beautifully motivates the right to left composition of functions.

But why is this? A simple way to think about this is as follows. Suppose σ represents a certain configuration of the puzzle, and we want to apply the move π. The resulting configuration is not π ∘ σ, but σ ∘ π. What will be the new value at n? First we determine what index the move π places at n. Then we determine what the current value at that index is, so: n ↦ σ(π(n)).