Commit 2021-04-14 08:29 63801552

refactor(*): kill nat multiplication diamonds (#7084) An add_monoid has a natural ℕ-action, defined by n • a = a + ... + a, that we want to declare as an instance as it makes it possible to use the language of linear algebra. However, there are often other natural ℕ-actions. For instance, for any semiring R, the space of polynomials polynomial R has a natural R-action defined by multiplication on the coefficients. This means that polynomial ℕ has two natural ℕ-actions, which are equal but not defeq. The same goes for linear maps, tensor products, and so on (and even for ℕ itself). This is the case on current mathlib, with such non-defeq diamonds all over the place. To solve this issue, we embed an ℕ-action in the definition of an add_monoid (which is by default the naive action a + ... + a, but can be adjusted when needed -- it should always be equal to this one, but not necessarily definitionally), and declare a has_scalar ℕ α instance using this action. This is yet another example of the forgetful inheritance pattern that we use in metric spaces, embedding a topology and a uniform structure in it (except that here the functor from additive monoids to nat-modules is faithful instead of forgetful, but it doesn't make a difference). More precisely, we define

def nsmul_rec [has_add M] [has_zero M] : ℕ → M → M
| 0     a := 0
| (n+1) a := nsmul_rec n a + a
class add_monoid (M : Type u) extends add_semigroup M, add_zero_class M :=
(nsmul : ℕ → M → M := nsmul_rec)
(nsmul_zero' : ∀ x, nsmul 0 x = 0 . try_refl_tac)
(nsmul_succ' : ∀ (n : ℕ) x, nsmul n.succ x = nsmul n x + x . try_refl_tac)

For example, when we define polynomial R, then we declare the ℕ-action to be by multiplication on each coefficient (using the ℕ-action on R that comes from the fact that R is an add_monoid). In this way, the two natural has_scalar ℕ (polynomial ℕ) instances are defeq. The tactic to_additive transfers definitions and results from multiplicative monoids to additive monoids. To work, it has to map fields to fields. This means that we should also add corresponding fields to the multiplicative structure monoid, which could solve defeq problems for powers if needed. These problems do not come up in practice, so most of the time we will not need to adjust the npow field when defining multiplicative objects. With this refactor, all the diamonds are gone. Or rather, all the diamonds I noticed are gone, but if there are still some diamonds then they can be fixed, contrary to before. Also, the notation •ℕ is gone, just use •.