Formalisation of (algebraic) combinatorics in Coq/MathComp.
Florent Hivert Florent.Hivert@lisn.fr
Contributors:
This library was supported by additional discussions with:
The project was transferred to mathcomp on 2021-10-20.
basic theory of symmetric functions including
Schur function and Kostka numbers and the equivalence of the combinatorial and algebraic (Jacobi) definition of Schur polynomials
the classical bases, Newton formulas and various basis changes
the scalar product and the Cauchy formula
the Littlewood-Richardson rule using Schützenberger approach, it includes
the Robinson-Schensted correspondence
the construction of the plactic monoïd using Greene invariants
the Littlewood-Richardson and Pieri rules using the combinatorial (tableau) definition of Schur polynomials.
After A. Lascoux, B. Leclerc and J.-Y. Thibon, "The Plactic Monoid" in Lothaire, M. (2011), Algebraic combinatorics on words, Cambridge University Press With variant described in G. Duchamp, F. Hivert, and J.-Y. Thibon, Noncommutative symmetric functions VI. Free quasi-symmetric functions and related algebras. Internat. J. Algebra Comput. 12 (2002), 671–717.
the Murnaghan-Nakayama rule for converting power sum to Schur function, it includes
two recursive implementations building the tableau upward or downward
a skew version multiplying a Schur function by a power sum expanding the result on Schur functions.
the character theory of the symmetric Groups. We do not use representations but rather goes as fast as possible to Frobenius isomorphism and then uses computations with symmetric polynomials. It includes
cycle types for permutations (together with Thibaut Benjamin)
The tower structure and the restriction and induction formulas for class indicator (together with Thibaut Benjamin)
the structure of the centralizer of a permutation
Young character and Young Rule
the theory of Frobenius characteristic and Frobenius character formula
the Murnaghan-Nakayama rule for evaluating irreducible characters
the Littlewood-Richardson rule for inducing irreducible characters
the Hook-Length Formula for standard Young tableaux (together with Christine Paulin and Olivier Stietel). We follow closely
Greene, C., Nijenhuis, A. and Wilf, H. S. (1979) A probabilistic proof of a formula for the number of Young tableaux of a given shape. Adv. in Math. 31, 104–109.
the Erdös Szekeres theorem about increassing and decreassing subsequences
from Greene's invariants theorem.
various Combinatorial objects including
the Coxeter presentation of the symmetric group.
We formalize:
the factorization of the Vandermonde determinant as the product of differences.
the Tamari lattice on binary trees.
the formula for Catalan numbers counting binary trees and Dyck words.
I use a bijective proof using rotations. There is a generating function proof available in https://github.com/hivert/FormalPowerSeries which I plan to merge here at some points.
The documentation is now complete ! with the dependancy graph.
A presentation given at "Algebra and combinatorics at LaCIM, a conference for the 50th anniversary of the CRM", September 24-28, 2018, Montreal, Quebec, Canada. This presentation is targeted at combinatorialist.
Another presentation given at Specfun Inria seminar, march
a Why3 certified implementation of the LR-Rule (together with Jean Christophe Filliâtre). See the Why3 branch on Github.
Poset. See the posets branch on Github.
This library is based on
Here are the Opam packages I'm using
coq-hierarchy-builder 1.6.0
coq-mathcomp-ssreflect 2.1.0
coq-mathcomp-algebra 2.1.0
coq-mathcomp-field 2.1.0
coq-mathcomp-fingroup 2.1.0
coq-mathcomp-character 2.1.0
coq-mathcomp-multinomials 2.1.0