The Coq mailing list

[Bruno Le Floch <blflatex AT gmail.com>]

Dear Cyril and Florent,

Thank you both.  I will delve into mathcomp over the next month or so
(Coq is not my main occupation unfortunately) and ask further questions
if I cannot find more specific things.  It is good to know that it has
linear algebra and graph theory.  Trees are not really needed: it just
happens that the graphs I'll end up with are trees.

On 01/11/2018 03:37 PM, Florent Hivert wrote:
> On Thu, Jan 11, 2018 at 03:39:16PM +0100, Cyril Cohen wrote:
>> I am not aware of any Coq development about ((semi-)simple) Lie algebras 
>> and
>> their classification.
> 
>> Unfortunately, I don't know much about semi-simple Lie algebra, so I cannot
>> anticipate precisely your needs, but if you are willing to give me more
>> details, I could tell you what exists or not in the mathematical components
>> library. You can also read the headers of theory files (such as
>> mathcomp/algebra/matrix.v, mathcomp/algebra/mxalgebra.v,
>> mathcomp/ssreflect/fingraph.v, ...) to check if what notions it covers.
> 
> I think I should mention my developement Coq-Combi [1] based on math-comp,
> whose main goal was to formally prove the Littlewood-Richardson rule, and 
> the
> Frobenius isomorphisms between symmetric functions and the character ring of
> symmetric-group. It's maybe not the same corpus of material, but If we 
> believe
> the Fulton-Harris book, there are closely related subjects.

They are definitely closely related, although my understanding is that
the relation holds for gl(n) or more generally A-type Lie algebras
su(n), sl(n), but that B,C,D,E,F,G type Lie algebras are more
complicated.  There are probably analogues of the Littlewood-Richardson
rule for all of these cases.

> It's not clear if you can reuse something from it (maybe partitions), but
> conceptually it's not very far. Also I'm close enough to people who
> implemented the Root System/Cartan/Coxeter/Lie theory in the computer 
> algebra
> system sage and there might probably be design choice which where good on 
> one
> side and can be reused.

We have been using Sage for other parts of the project so I'll
definitely take a very close look.  It seems to have a lot of things.

> Anyway, I would be interested to discuss, about such development if not to
> help.

Thanks!  If the project is not done by this fall we can probably talk in
person (I'll do a physics postdoc in ENS next year).

Best,

Bruno