[WIP] replace the infrastructure of mpoly with monalg

[pi8027]

Currently, the Multinomials library has two representations of polynomials:

• mpoly.v: old, less general (e.g., variables must be an ordinal, variables must be commutative), but more results
• monalg.v: new, more general (e.g., variables can be any choiceType, the type of polynomials can be instantiated with commutative, non-commutative, and mixed commutative and non-commutative monomials), but fewer results

This PR is the first step in unifying these two representations: reimplementing mpoly.v using the infrastructure provided by monalg.v. By doing so, I expect that we can remove freeg.v and some part of mpoly.v, and that we can identify what is lacking in monalg.v.

Then, a later step would be to port the remaining results in mpoly.v (e.g., monomial ordering) to monalg.v with some generalizations (e.g., extending the monomial algebra hierarchy with monomial ordering, which allows us to choose the monomial order).

See also: #19

[pi8027]

Hi @CohenCyril @Tragicus @proux01, I hope to reimplement mpoly.v based on monalg.v here. Since it forces us to change the underlying representation of monomials and polynomials, it will be a breaking change anyway. Although we won't merge it very soon, it is something you should be aware of as maintainers of the downstream packages (CoqEAL and CAD).

[proux01]

Thanks for the heads up. It might well be a good opportunity for me to rewrite the multipoly refinement in CoqEAL, to target the structure used by ring/lra rather than those heavy maps on top of Stdlib. Or maybe CoqEAL will be subsumed by Trocq by then, who knows. Anyway, go ahead.

[pi8027]

Thanks for the heads up. It might well be a good opportunity for me to rewrite the multipoly refinement in CoqEAL, to target the structure used by ring/lra rather than those heavy maps on top of Stdlib. Or maybe CoqEAL will be subsumed by Trocq by then, who knows. Anyway, go ahead.

@proux01 I need the refinement from {malg R[cmonom I]} to sparse Horner forms. We may want to make sure that it can replace multipoly in CoqEAL. (I need the non-commutative counterpart too, but I came to the conclusion that Ncring_polynom ind the standard library is not very efficient, and I will probably define my own computation-oriented non-commutative polynomials.)

[pi8027]

I ported the first 1800 lines of mpoly.v, but I don't feel very motivated to do the rest (3000+ lines). Let me know if someone is willing to continue working on it.

[pi8027]

I see a few issues that make the porting non-trivial:

• the performance issue mentioned above
• There is some mismatch of datatypes between mpoly and monalg e.g., monomials represented as tuples or finfuns, the support of a polynomial (msupp) represented as a list or a fset. I had to modify the statements of some lemmas.
• The binary operation on monomials are denoted as addition and multiplication in mpoly and monalg, respectively. A lot of renaming and deprecation are needed on the mpoly side. (I prefer to do it in a separate PR.)

I'm taking a break from this PR until the 17th (which happens to be the next MC dev meeting).

[proux01]

@proux01 I need the refinement from {malg R[cmonom I]} to sparse Horner forms. We may want to make sure that it can replace multipoly in CoqEAL.

AFAIK, the only use of that refinement is in ValidSDP: https://github.com/validsdp/validsdp/blob/master/theories/validsdp.v
I can identify the following in there, that all look like very usual things (except maybe PCompose)

Class list_of_poly_of T monom polyT := list_of_poly_op :
  polyT -> seq (monom * T).
Definition max_coeff (p : polyT) : T :=
  foldl (fun m mc => max m (max mc.2 (-mc.2)%C)) 0%C (list_of_poly_op p).

Inductive p_real_cst :=
| PConstR0
| PConstQq (_ : bigZ) (_ : bigN)
| PConstIZR (_ : BinNums.Z)
| PConstRdiv (_ : p_real_cst) (_ : positive)
| PConstRopp (_ : p_real_cst)
| PConstRinv (_ : positive).

Inductive p_abstr_poly :=
  | PConst (_ : p_real_cst)
  | PVar (_ : nat)
  | POpp (_ : p_abstr_poly)
  | PAdd (_ : p_abstr_poly) (_ : p_abstr_poly)
  | PSub (_ : p_abstr_poly) (_ : p_abstr_poly)
  | PMul (_ : p_abstr_poly) (_ : p_abstr_poly)
  | PPowN (_ : p_abstr_poly) (_ : binnat.N)
  | PPown (_ : p_abstr_poly) (_ : nat)
  | PCompose (_ : p_abstr_poly) (_ : seq p_abstr_poly)
.

Fixpoint interp_poly_ssr (n : nat) (ap : abstr_poly) {struct ap} : {mpoly rat[n]} :=
  match ap with
  | Const t => (bigQ2rat t)%:MP_[n]
  | Var i =>
    match n with
    | O => 0%:MP_[O]
    | S n' => 'X_(inord i)
    end
  | Add a0 a1 => (interp_poly_ssr n a0 + interp_poly_ssr n a1)%R
  | Sub a0 a1 => (interp_poly_ssr n a0 - interp_poly_ssr n a1)%R
  | Mul a0 a1 => (interp_poly_ssr n a0 * interp_poly_ssr n a1)%R
  | PowN a0 n' => mpoly_exp (interp_poly_ssr n a0) n'
  | Compose a0 qi =>
    let qi' := map (interp_poly_ssr n) qi in
    match sumb (size qi' == size qi) with
    | right prf => 0%:MP_[n]
    | left prf =>
      comp_mpoly (tcast (eqP prf) (in_tuple qi'))
                 (interp_poly_ssr (size qi) a0)
    end
  end.

As I said, I'm fine with some breaking changes on that multipoly.v file in CoqEAL and having to do some porting work in validsdp. Not eveything needs to be exactly backward compatible and nice deprecations here.