This PR changes the notation for naming formal variables associated to recursive polynomial-like objects.

Registration is done only once per each polynomial-like functor.

Usage:

register_poly_vars "[" "]" Polynomial Polynomial.C Polynomial.X
register_poly_vars (mv := true) "[" "]" MvPolynomial MvPolynomial.C MvPolynomial.X
name_poly_vars R[a,b][C]
name_poly_vars _[x,y,z]

_[[x,y,z]] allows for the hole to be substituted by any base ring, so (x : R[[x,y,z]]) will be valid syntax.

There has been some discussion about its implementation:

• It has been suggested that R[x,y][z] should mean that R[x,y] is a subring, i.e. x should live in R[x,y], but in my implementation x lives in the big ring R[x,y][z]. There are two ways to get the other behaviour:
  • One can do R[x,y] and then (R[x,y])[z].
  • One can do R[a,b] and R[x,y][z]. I personally prefer this one because we should make it clearer that they are different rings.
• There has been some discussion over what R means. In my implementation, if you ever refer to a variable called R, then R is fixed to that variable, meaning that if you later define a variable with the same name, R will still refer to the old variable. Also, this does not respect namespace, meaning that if you refer to Foo.bar[x,y], and later open Foo, you will not be able to access the declared ring with bar[x,y].

I have not mass deployed the new syntax at every possible location, I plan to do that in a future PR following this.

Zulip: #mathlib4 > Notation for polynomial variables

This is a refactor of the currently existing Mathlib.Tactic.namePolyVarsOver. More explicitly, the current invocation name_poly_vars x,y over R is now poly_variable R[x,y]. The behaviours inherited from name_poly_vars are:

• We do not synthesize the necessary instances (such as [CommRing R]) at the point of declaration, but only when the new notations are used.
• We refer to an explicit term (R in the examples) which is "fixed", in the sense that:
  • it is only valid for R explicitly, and not any other variable such as S.
  • it has built-in hygiene, so if you shadow the variable by declaring a new variable (R : Type*), it will still refer to the old one.

And the new behaviours are:

• Currently only x and y are new notations, but in the new tactic the whole ring R[x,y] is also available as notation.
• Currently only the forward direction (i.e. elaboration, going from x to MvPolynomial.X 0) is implemented, but in the new tactic we also implement the backward direction, printing MvPolynomial.X 0 back as x (and MvPolynomial (Fin 2) R is printed as R[x,y]).
• Support beyond just MvPolynomial.
• Support for nested polynomial-like rings, such as R[x,y][t][[z]] for PowerSeries (Polynomial (MvPolynomial (Fin 2) R)).