More generic multinomial (Dagstuhl discussion)

[hivert]

With @amahboubi, @CohenCyril and @Sobernard we had a discussion about multivariate polynomials at Dagstuhl 18341. I'm creating an issue to keep a trace of our conclusions. Please feel free to amend and edit.

Here is the current status from what we understand:

Following a discussion we had, you started to develop monalg.v with the idea that multivariate polynomials could be implemented as the monoid algebra of the free commutative monoid. Having the notion of a generic monoid algebra allows for example to develop easily non-commutative polynomials as the algebra of the free monoid or Laurent polynomials as the algebra of the free commutative group... Moreover the base structure {malg G[K]} deals with linear combination of anything which is even not a monoid. The allows to build more general algebras. However it seems that you didn't had the time to rebase mpoly on to of that (or is it another issue ?).

Anyway, here is what we feel needs to be done:

1 - Rebase malg on top of finmap/finset 1.1 which is much easier to use. In particular, it allows to handle bigops seamlessly, without having to construct element in complicated finTypes
2 - Check that is is generic enough to handle various cases. I did some experiment on that in Dagstuhl, only admitting lemmas made difficult because of point 1 (See in shufflealg.v implementing the shuffle algebra). It is easy to uses and half of the files is generic enough that it can be contributed back here (ie: the construction of linear/bilinear maps).
3 - Rebase mpoly on top of malg
4 - Non commutative polynomials and refactorization of common code with polynomials
5 - One of the problem I had in Coq-Combi which is appears also in Sophie development is to combine polynomials on several sets of variables. So we wished to have a polynomials on any finite subset of a large (possibly infinite set) while being able to combine them. The typical application is to deals with polynomial which are symmetric only is subset of the set of variables.

Depending on the time, I'm interested to help. For example, I might start to handle task 1 soon. So please coordinate any effort with this plan.

[strub]

Hi,

Well done Sherlock(s). I hope it did not take too much cocaine to come with this reversed history.

I did not finish the merge because of lack of time. I'd like that to complete points 1, 2, 3 & 4 and to do a release before moving to extensions (like point 5). We (you & me) could meet in September on the Sili^W Saclay valley and address the first 4 points if you want. 2 (maybe 3) days of work should be enough.

[hivert]

Hi @strub.

I wanted to have a closer look at malg and finmap, so I started to hack in monalg.v. I'm happy to report that a large part of 1 is now done ! See this branch. Except at to point where I had no choice, I replaced all the bigops on finType msupp g by bigops on sequences. The two problematic points were:

• A use of [exists ...] to do some contrapose arguments. As far as I know, there is no equivalent in fset.
• A use of \max the lemmas in big_op.v are only stated on finType's and not on seq.

Also I didn't yet learnt about finmap's so I didn't change anything on them.

[amahboubi]

Hi,
in addition, my notes from that discussion also mention:
6 - it seems that malg still lacks the evaluation morphism
7 - some constants (e.g. malg, msupport) should probably be renamed
8 - in the end, isn't freeg.v made obsolete by monalg.v
9 - we should try to see if these construction can be used to construct the group algebras used in the representation theory part of MathComp.

I also had a few more details about Florent's item 5. I share them for the record (feel free to edit/correct/comment):

mpoly.v provides a datstructure for multivariate polynomials in n variables, where a monomial m is represented as a (finite) function from 'I_n to nat, returning the exponent of the i-th variable in m. This proved too rigid for both @hivert and @Sobernard, who needed to deal with multivariate polynomials seen as elements of R[X, X \in A][X, X\notin A] (pseudo-code here), for A a subset of the variables. The variables could be represented by the inhabitants of I_n, as suggested by the paper notation X_1,...,X_i, but ideally, we would like to allow for more liberal ways of indexing variables.
Here is the plan:

• starting from T : choiceType, finmap/finset provides a construction for finite sets of elements in T. Let A be such a finite set.
• malg provides a construction freemon (pseudocode) of free (commutative) monoids generated by a (not necessarily finite) subset of a choiceType.
• malg provides a construction of the polynomial expressions with coefficients in a given type on a free commutative monoid. So we have (pseudo code) R[(freemon A)] the type of polynomial expressions with coefficients in R "on" the free monoid generated by A. We also have R[(freemon T)] the type of polynomial expressions with coefficients in R "on" the free monoid generated by T. Type R[(freemon A)] is a subtype of type R[(freemon T)]. As soon as R is equipped with a ring structure, R[(freemon A)] is the expected ring of polynomials.

[strub]

Hi @amahboubi,

As you noticed, there is a lot of legacy / to be deprecated code (and also uncommitted code, but this is something you couldn't see). In a nutshell, freeg.v is here for mpoly.v (both have been written at a time where finmap was not in the field) & mpoly.v is going to be deprecated by monalg.v (or at least is going to be built & generalized using monalg.v). As I said in the first message, I'd like to get rid of this legacy code (i.e. to finish what I started) before moving to extension & renaming. I do think this is a 2-3 day work.

Regarding your plan, this is already the direction taken in monalg.v. For instance, if you go at the end of the file, you can see an alternative definition of {mpoly R[n]} as {malg R['X_{1..n}]} where 'X_{1..n} is {cmonom 'I_n}, i.e. the free commutative monoid over 'I_n. So the construction {malg R[{cmomon T}]} with T a choiceType is already there --- let's write it {mpoly R[T]}.

What is missing is simply to take the contents of mpoly.v and to backport it to either {malg R[T]} or {mpoly R[T]}. This is where lies the 2-3 days of work (most of the time, the proof is agnostic regarding the set of variables).

[hivert]

I'm just adding a pointer here saying that point 1 is mostly done in my #20 pull request. Please fix/expand/comment.

[CohenCyril]

To followup on my #20 (comment) and point 6. from @amahboubi, here is what I believe should be done with regard to the evaluation morphism and @hivert #20 (comment). My point was to try to be as close as possible to the categorical presentation of the adjunction between a free algebra and a forgetful functor.

Define

malg_lift (R : ringType) (X : choiceType) (L : lmodType R) (f : X -> L) : {malg R[X]} -> L.

It should be (canonically) linear. Moreover malg_lift f : {malg R[X]} -> A should be canonically an algebra morphism (lrmorphism from ssralg), as soon as f : M -> A is a monoid morphism from the monoid M to the R-algebra A seen as a multiplicative monoid.
Note that it can be instantiated to A := R^o to derive a simple ring morphism instead. This should cover @hivert #20 (comment) desired morphisms, and subsume https://github.com/hivert/Coq-Combi/blob/Shuffle/theories/Dendri/shufflealg.v#L27-L66, am I right?

Now to get evaluation one just needs to precompose malg_lift with mon_lift where

mon_lift (X : choiceType) (M : monoidType) (f : X -> M) : {monoid X} -> M.

which should be canonically a monoid morphism, and where {monoid X} is the free monoid on X.
So that eval : (X -> A) -> {malg R[{monoid X}]} -> A := malg_lift \o mon_lift is the evaluation algebra morphism. Again this can be specialized to A := R^o...

Various comments:

• In the current state of the code, monoids do not exist (there is an extra "integrity hypothesis" unitm), so the hierarchy begins with monomType. Moreover, monomial morphisms are specialized with a codomain in ringType, which is still compatible with what I said, (replacing M: monoidType by ringType in the type of mon_lift). Should we also insert monoidType? Should we introduce general monoid morphisms?
• malg is more an initial algebra than a monomial algebra in the general case, that is one reason for @amahboubi point 7, and sage just call such thing algebra, so I am rooting for {alg R[X]} as a potential renaming.
• I am not sure the special case of zmodType should be dealt with at all, since {malg R[X]} is parametrized by R... I believe we should do it only if one wanted to reimplement the abelian group freeg X := {malg int[X]}.

edited after reading #20 (comment)

[hivert]

• I just generalized {malg R[B]} to M : lmodType R in https://github.com/hivert/Coq-Combi/blob/Shuffle/theories/Dendri/shufflealg.v#L27-L66 and this works again (upto the two missing proof that are not yet done because I was waiting for the new malg version). I think what you called malg_lift is exactly my linmalg.
• +1 to the renaming of malg. The proposition of having {alg R[X]} is consistent with what we have in Sage under the name of Algebra functorial construction.

[hivert]

Finally I found some time to finish and complete my shufflealg experiments. So if I understand correctly it contains the theory of malg_lift (under the name of linmalg). However since I switched to the new malg and finished the proofs, various lemmas become extremely slow to apply, including lemmas as simple as addrC (commutativity of addition in a ring). I've no idea on how to investigate or solve such problems. Maybe I should lock some definitions. Any suggestion ?

[CohenCyril]

I've no idea on how to investigate or solve such problems. Maybe I should lock some definitions. Any suggestion ?

Could you point me to your slowdowns?

[hivert]

@CohenCyril : I manage to mitigate the slowdown by adding some lock. But this is still very slow. See the first line of the proof of lemma bla2. On my laptop it takes 20s whereas it was 1/2s at commit 54b3870c93d0cda14c693249f6d0ccc95d433681

[hivert]

@CohenCyril : I just hit a point where the slowdown completely stop me. But maybe this is a basic Coq problem. To reproduce the problem:

• You need to have Finmap 1.1 + the development version of multinomials
• You need the latest version of shufflealg.v. Note: that this file is independent from the rest of the repository.
• On my computer I have two version of finmap and multinomials installed. The devel version are installed are in Devel so I do:

From Devel Require Export finmap.
From Devel Require Import xfinmap ssrcomplements monalg.

You probably want to change that to

From mathcomp Require Export finmap.
From SsrMultinomials Require Import xfinmap ssrcomplements monalg.

• Then go until the STUCK Here comment. Coq takes minutes to match the location where I wan't to apply addrAC and I'd like to apply those lemmas several times.

Maybe my goal is a little too big, but I my experience, Coq should not be so slow.

[amahboubi]

Hi @hivert. How can I replay your shufflealg file? I have trouble understanding the dependencies. Also, I could not find the STUCK Here comment in the version the link points to: which line is the infamous one?

[hivert]

@amahoubi : Sorry, I was interrupted before the push and there where some missing infos. Please, see my edit.

[pi8027]

We had a meeting on this generalization work. From my point of view, the first things to do are:

• "3 - Rebase mpoly on top of malg" (I think this step is useful for identifying the abstraction layers currently lacking. We should replace 'X_{1..n} with {cmonom I}, but it seems not very straightforward since the latter uses finmap.)
• Extending the monomial algebra hierarchy (monomType and conomType) with monomial order. Later, we can consider extending them with the divisibility relation. (Cyril suggested making such structures equipped with two orderings, although I was thinking about splitting such a structure into a fully-bundled one and a semi-bundled one.)
• "6 - it seems that malg still lacks the evaluation morphism"

[amahboubi]

Hello @pi8027 , thanks for sharing this log. What kind of difficulties do you foresee in your first item (you seem to suggest that the dependency in finmap is an issue).

[amahboubi]

My own item zero in this todo list would be to document monalg.v. Makes sense?

[hivert]

My own item zero in this todo list would be to document monalg.v. Makes sense?

Very good idea !

[amahboubi]

OK, so I will try that and propose to get feedback.

[pi8027]

Hello @pi8027 , thanks for sharing this log. What kind of difficulties do you foresee in your first item (you seem to suggest that the dependency in finmap is an issue).

My understanding is that, when we replace tuples (from tuple.v, or equivalently finfuns) with finmaps, the finite support should be made explicit in each construct of a finmap rather than in its type. It prevents us from using the [multinom F | i < n] notation, adds extra burden to reason about bigops ranging over the support of a monomial, etc. A part of the difficulties also comes from the fact that I have never seriously used the finmap library (despite I'm an author). So I thought it would be better to investigate it with Cyril.

[pi8027]

My own item zero in this todo list would be to document monalg.v. Makes sense?

Yes, make sense.

[pi8027]

I did some refactoring of monalg.v in #80. I discovered that we can use mmap as the evaluation morphism, but it currently forces the codomain of this morphism to be commutative (see mmap_rmorphism). @CohenCyril's suggestion (#19 (comment)) seems to be a possible solution.