<h1 id="rocq-combi">Rocq-Combi</h1>
<p>Formalisation of algebraic combinatorics in Rocq/MathComp.</p>
<p><a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.1-mcmaster.yml"><img">https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.1-mcmaster.yml"><img src="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2FCoq-Combi%2Factions%2Fworkflows%2Fnix-action-rocq-9.1-mcmaster.yml%2Fbadge.svg">https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.1-mcmaster.yml/badge.svg"
alt="Nix CI for bundle rocq-9.1-mcmaster" /></a> <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.1-mc2.5.0.yml"><img">https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.1-mc2.5.0.yml"><img src="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2FCoq-Combi%2Factions%2Fworkflows%2Fnix-action-rocq-9.1-mc2.5.0.yml%2Fbadge.svg">https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.1-mc2.5.0.yml/badge.svg"
alt="Nix CI for bundle rocq-9.1-mc2.5.0" /></a> <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.0-mc2.5.0.yml"><img">https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.0-mc2.5.0.yml"><img src="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2FCoq-Combi%2Factions%2Fworkflows%2Fnix-action-rocq-9.0-mc2.5.0.yml%2Fbadge.svg">https://github.com/math-comp/Coq-Combi/actions/workflows/nix-action-rocq-9.0-mc2.5.0.yml/badge.svg"
alt="Nix CI for bundle rocq-9.0-mc2.5.0" /></a></p>
<h1 id="authors">Authors</h1>
<p>Florent Hivert <a href="mailto:Florent.Hivert@lisn.fr"
class="email">Florent.Hivert@lisn.fr</a></p>
<p>Contributors:</p>
<ul>
<li>Thibaut Benjamin (representation theory of the symmetric
groups)</li>
<li>Jean Christophe Filliâtre (Why3 implementation)</li>
<li>Christine Paulin (SSreflect binding for ALEA + hook length
formula)</li>
<li>Olivier Stietel (hook length formula)</li>
<li>Cyril Cohen (MathComp compatibility + nix)</li>
<li>Pierre Roux (MathComp compatibility + nix)</li>
</ul>
<p>This library was supported by additional discussions with:</p>
<ul>
<li>Kazuhiko Sakaguchi (port on MathComp2 / Hierarchy Builder)</li>
<li>Georges Gonthier</li>
<li>Assia Mahoubi</li>
<li>Pierre Yves Strub</li>
<li>the SSReflect mailing list</li>
</ul>
<p>The project was transferred to mathcomp on 2021-10-20.</p>
<h1 id="contents">Contents</h1>
<ul>
<li><p>basic <strong>theory of symmetric functions</strong>
including</p>
<ul>
<li><p><em>Schur function</em> and <em>Kostka numbers</em> and the
equivalence of the combinatorial and algebraic (Jacobi) definition of
Schur polynomials</p></li>
<li><p>the classical bases, <em>Newton formulas</em> and various basis
changes</p></li>
<li><p>the scalar product and the <em>Cauchy formula</em></p></li>
</ul></li>
<li><p>the <strong>Littlewood-Richardson</strong> rule using
Schützenberger approach, it includes</p>
<ul>
<li><p>the <em>Robinson-Schensted</em> correspondence</p></li>
<li><p>the construction of the <em>plactic monoïd</em> using <em>Greene
invariants</em></p></li>
<li><p>the <em>Littlewood-Richardson</em> and <em>Pieri</em> rules using
the combinatorial (tableau) definition of Schur polynomials.</p></li>
</ul>
<p>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.</p></li>
<li><p>the <strong>Murnaghan-Nakayama</strong> rule for converting power
sum to Schur function, it includes</p>
<ul>
<li><p>two recursive implementations building the tableau upward or
downward</p></li>
<li><p>a skew version multiplying a Schur function by a power sum
expanding the result on Schur functions.</p></li>
</ul></li>
<li><p>the <strong>character theory of the symmetric Groups</strong>. We
do not use representations but rather goes as fast as possible to
Frobenius isomorphism and then uses computations with symmetric
polynomials. It includes</p>
<ul>
<li><p><em>cycle types</em> for permutations (together with Thibaut
Benjamin)</p></li>
<li><p>The tower structure and the <em>restriction and induction
formulas</em> for class indicator (together with Thibaut
Benjamin)</p></li>
<li><p>the structure of the <em>centralizer</em> of a
permutation</p></li>
<li><p>Young character and <em>Young Rule</em></p></li>
<li><p>the theory of Frobenius characteristic and <em>Frobenius
character formula</em></p></li>
<li><p>the <em>Murnaghan-Nakayama</em> rule for evaluating irreducible
characters</p></li>
<li><p>the <em>Littlewood-Richardson</em> rule for inducing irreducible
characters</p></li>
</ul></li>
<li><p>the <strong>Hook-Length Formula</strong> for standard Young
tableaux (together with Christine Paulin and Olivier Stietel). We follow
closely</p>
<p>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.</p></li>
<li><p>the <strong>Erdös Szekeres theorem</strong> about increassing and
decreassing subsequences</p>
<p>from Greene’s invariants theorem.</p></li>
<li><p>various <strong>Combinatorial objects</strong> including</p>
<ul>
<li>integer partitions and compositions, together with Young’s and
dominance lattices</li>
<li>skew partition, horizontal, vertical and ribbon border strip</li>
<li>tableaux, standard tableaux, skew tableaux</li>
<li>subsequences, integer vectors</li>
<li>standard words, permutations and the standardization map</li>
<li>Yamanouchi word</li>
<li>binary trees, Dyck words and Catalan numbers</li>
<li>set partition and refinement order</li>
</ul></li>
<li><p>the <strong>Coxeter presentation of the symmetric
group</strong>.</p>
<p>We formalize:</p>
<ul>
<li>presentation of the symmetric group generated by elementary
transpositions</li>
<li>Matsumoto theorem saying that two reduced words give the same
permutation iff they are equivalent under braid relations</li>
<li>the Coxeter length and the inversion set</li>
<li>the dual Lehmer code of a permutation</li>
<li>the weak permutohedron lattice</li>
</ul></li>
<li><p>the <strong>factorization</strong> of the Vandermonde determinant
as the product of differences.</p></li>
<li><p>the <strong>Tamari lattice</strong> on binary trees.</p></li>
<li><p>the formula for <strong>Catalan numbers</strong> counting binary
trees and Dyck words.</p>
<p>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.</p></li>
</ul>
<h1 id="documentation">Documentation</h1>
<ul>
<li><p>The <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://math-comp.github.io/combi/1.0.0/toc.html">documentation</a" rel="nofollow">https://math-comp.github.io/combi/1.0.0/toc.html">documentation</a>
is now complete ! with the <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://math-comp.github.io/combi/1.0.0/index.html">dependancy" rel="nofollow">https://math-comp.github.io/combi/1.0.0/index.html">dependancy
graph</a>.</p></li>
<li><p>A <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://dl.acm.org/doi/10.1145/3703595.3705885">paper</a" rel="nofollow">https://dl.acm.org/doi/10.1145/3703595.3705885">paper</a> and the
associated <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://www.lri.fr/~hivert/Conf/CPP2025.pdf">slides</a" rel="nofollow">https://www.lri.fr/~hivert/Conf/CPP2025.pdf">slides</a>, in CPP
’25: Proceedings of the 14th ACM SIGPLAN International Conference on
Certified Programs and Proofs</p></li>
<li><p>A <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/raw/master/doc/Talk-CRM/CRM.pdf">presentation</a">https://github.com/math-comp/Coq-Combi/raw/master/doc/Talk-CRM/CRM.pdf">presentation</a>
given at “<a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"http://www.crm.umontreal.ca/2018/Algebre18/index_e.php">Algebra" rel="nofollow">http://www.crm.umontreal.ca/2018/Algebre18/index_e.php">Algebra
and combinatorics at LaCIM</a>, a conference for the 50th anniversary of
the CRM”, September 24-28, 2018, Montreal, Quebec, Canada. This
presentation is targeted at combinatorialist.</p></li>
<li><p>Another <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/raw/master/doc/Talk/INRIA.pdf">presentation</a">https://github.com/math-comp/Coq-Combi/raw/master/doc/Talk/INRIA.pdf">presentation</a>
given at <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://specfun.inria.fr/seminar/">Specfun</a" rel="nofollow">https://specfun.inria.fr/seminar/">Specfun</a> Inria
seminar, march</p>
<ol start="2015" type="1">
<li>This presentation is targeted at proof-assistant specialist.</li>
</ol></li>
</ul>
<h1 id="various-unstableunfinished-experiments">Various
unstable/unfinished experiments:</h1>
<ul>
<li><p>a <strong>Why3 certified implementation</strong> of the LR-Rule
(together with Jean Christophe Filliâtre). See the <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/tree/Why3">Why3">https://github.com/math-comp/Coq-Combi/tree/Why3">Why3 branch on
Github</a>.</p></li>
<li><p>Poset. See the <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/tree/posets">posets">https://github.com/math-comp/Coq-Combi/tree/posets">posets branch
on Github</a>.</p></li>
</ul>
<h1 id="installation">Installation</h1>
<p>This library is based on</p>
<ul>
<li><p><a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/math-comp">SSReflect/MathComp">https://github.com/math-comp/math-comp">SSReflect/MathComp 2</a>
Library version 2.5.0 or more recent.</p></li>
<li><p>This branch is <em>not</em> compatible with version MathComp
2.4.0.</p></li>
<li><p>For MathComp 2.4.0, use the <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/tree/MathComp-2.4.0">MathComp-2.4.0</a">https://github.com/math-comp/Coq-Combi/tree/MathComp-2.4.0">MathComp-2.4.0</a>
branch.</p></li>
<li><p>For MathComp 2.3.0, use the <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/tree/MathComp-2.3.0">MathComp-2.3.0</a">https://github.com/math-comp/Coq-Combi/tree/MathComp-2.3.0">MathComp-2.3.0</a>
branch.</p></li>
<li><p>For MathComp 2.2.0, use the <a href="/sitelet?url=https%3A%2F%2Fgithub.com%2Fmath-comp%2Fmath-comp.github.io%2Ftree%2Fmaster%2F%253Ca%2520href%3D"https://github.com/math-comp/Coq-Combi/tree/MathComp-2.2.0">MathComp-2.2.0</a">https://github.com/math-comp/Coq-Combi/tree/MathComp-2.2.0">MathComp-2.2.0</a>
branch.</p></li>
</ul>
<p>Here are the Opam packages I’m using</p>
<pre><code>rocq-hierarchy-builder        1.9.1
rocq-mathcomp-ssreflect       2.5.0
rocq-mathcomp-algebra         2.5.0
rocq-mathcomp-field           2.5.0
rocq-mathcomp-fingroup        2.5.0
rocq-mathcomp-character       2.5.0
coq-mathcomp-multinomials     2.4.0</code></pre>