17
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ @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. $\endgroup$
    – hardmath
    Feb 24, 2022 at 14:20
  • $\begingroup$ @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. $\endgroup$
    – hardmath
    Feb 25, 2022 at 16:36

1 Answer 1

10
$\begingroup$

John Harrison had a nice paper about “wlog” reasoning and the logical requirements behind it. The paper talks about various ways in which these can be automated. This is in HOL Light, and I know there is an analogous tactic in HOL4. Given how foundationally simple HOL is, I expect the logic works in other systems too.

$\endgroup$
1
  • $\begingroup$ Thanks, this is very on point. $\endgroup$
    – hardmath
    Feb 24, 2022 at 1:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.