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.
