# WLOG reasoning and Proof Assistants

The possibility of using proof assistants in combinatorics has been mentioned here and in more detail here. I'm interested in automating that part of some discrete problems which reduces the search space "without loss of generality" by exploiting various symmetries.

I'll mention for context a couple of problems I'm interested in:

(1) Counting (doubly) diagonal latin squares invites reduction of a search space by the centralizer of a specific permutation. A latin square of size $$n\times n$$ has the numbers $$1,2,\ldots,n$$ in each row and each column without repetition. Such a square is doubly diagonal iff the main diagonal and the anti-diagonal also have each $$n$$ distinct entries. For example:

$$\begin{array}{|c|c|c|c|} \hline 1 & 4 & 2 & 3 \\ \hline 3 & 2 & 4 & 1 \\ \hline 4 & 1 & 3 & 2 \\ \hline 2 & 3 & 1 & 4 \\ \hline \end{array} \;\text{ and }\; \begin{array}{|c|c|c|c|c|} \hline 1 & 2 & 3 & 4 & 5 \\ \hline 5 & 3 & 4 & 1 & 2 \\ \hline 4 & 5 & 2 & 3 & 1 \\ \hline 2 & 4 & 1 & 5 & 3 \\ \hline 3 & 1 & 5 & 2 & 4 \\ \hline \end{array}$$

(2) An absorbing Markov chain might be naively formulated using many equivalent states and transitions, and this invites for some purposes (e.g. expected steps until an absorbing state is reached) pruning the search space by symmetries of states.

My intuition is that proving "without loss of generality" cases is similar to proving program correctness. Prolog code has often helped me with checking that "all bases are covered," but I experience a certain amount of frustration with reinventing the wheel because of the weak(!) datatyping in Prolog. So I'd be interested if setoids or some other construction would provide rigorous analysis of cases.

• @GuyCoder: When I searched a few years ago, I found a mention and a handful of counts in a book chapter of an "encyclopedia" on combinatorics. A more recent paper is "Enumerating Diagonal Latin Squares of Order Up to 9" by Kochemazov and Zaikin (2020). Enumerating means listing them out, not merely counting them. They contributed the counts OEIS A274806. Feb 24, 2022 at 14:20
• @GuyCoder: I left a brief comment there, about symmetries that help to count or list solutions for $n=4$. Larger orders involve deeper symmetries described in Centralizer of a specific permutation. Feb 25, 2022 at 16:36