Scalar actions in Lean's mathlib

Eric Wieser
Cambridge University Engineering Department

slides: eric-wieser.github.io/fmm-2021 2021-07-31

Introduction

Lean 3^*: A dependently-typed language suitable for theorem proving
Mathlib^†: A coherent library of formalized mathematics for Lean 3, assembled via an ongoing collaborative effort from over 170 contributors across disciplines.
This presentation: A case study in the use of the has_scalar typeclass in Mathlib, and difficulties arising around compatibility of actions and around instance diamonds.

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von RaumerThe Lean Theorem Prover (System Description) The mathlib CommunityThe Lean Mathematical Library

IntroductionWhat are typeclasses?

Declaration with class


              class has_mul (G : Type*) := (mul : G → G → G)  -- in Lean

              infix * := has_mul.mul


              class semigroup (G : Type*) extends has_mul G :=  -- in Mathlib
              (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))

Usage with […]


              lemma mul_assoc₂ {G : Type*} [semigroup G] (a b c d : G) :
                a * (b * (c * d)) = ((a * b) * c) * d :=
              by rw [mul_assoc, mul_assoc]

Instantiation with instance


              instance (α : Type*) : semigroup (list α) :=
              { mul := list.append,  -- list.append [a, b] [c, d] = [a, b, c, d]
                mul_assoc := list.append_assoc }

Before we look at has_scalar, I'll give a quick summary of what typeclasses are and how they work, using the even simpler example of multiplication.
Typeclasses are a way of equipping types with canonical operators and axioms which apply to those operators. Working with them breaks down into three parts.

The first part is defining the typeclass itself. Lean defines a typeclass has_mul G, which provides a definition of multiplication for the type G, along with the usual notation.
Mathlib provides a stronger typeclass semigroup G, which requires additionally that the multiplication on G be associative.

The second part is using the typeclass. By including semigroup G in our argument list for mul_assoc_two in square brackets, we have access to a multiplications operator and the proof that it is associative. In turn, Lean will automatically search for a semigroup structure any time someone uses our lemma.

The final part is providing instances of the typeclass. As an example, we can show that lists form a semigroup under concatenation. Having done this, we can now apply our mul_assoc_two lemma to lists.

IntroductionWhat are scalar actions?

The has_scalar typeclass:


              class has_scalar (M : Type*) (α : Type*) := (smul : M → α → α)

              infixr ` • `:73 := has_scalar.smul

Notation: m • a₁ = a₂.


              class mul_action (M : Type*) (α : Type*) [monoid M]
                extends has_scalar M α :=
              (one_smul : ∀ a : α, (1 : M) • a = a)
              (mul_smul : ∀ (m₁ m₂ : M) (a : α), (m₁ * m₂) • a = m₁ • m₂ • a)

The has_scalar typeclass looks similar to the has_mul we just saw, but is parameterized by two types not one. It provides a heterogenerous operator over these two types called smul, which applies an action defined by the first argument of type M on the second argument of type alpha. We say that the type alpha has an action by M.

Just as a multiplication that satisfies no properties is uninteresting, so is a scalar action. In practice, we almost always work with the mul_action typeclass, which describes monoid and group actions by adding two proof fields.

Mathlib provides numerous stronger typeclasses which in turn extend mul_action adding additional proof fields, notably module and algebra. The graph here shows the inheritance heirarchy of these typeclasses.

Elementary actions

Elementary actions Left-multiplication

A simple action: a • b = a * b


            variables {α : Type*}

            instance has_mul.to_has_scalar [has_mul α] :
              has_scalar α α := { smul := (*) }

Stronger versions


              instance monoid.to_mul_action [monoid α] :
                mul_action α α :=
              { one_smul := one_mul, mul_smul := mul_assoc }

Elementary actions Left-multiplication

Stronger versions


                instance has_mul.to_has_scalar [has_mul α] :
                  has_scalar α α := { smul := (*) }


                instance monoid.to_mul_action [monoid α] :
                  mul_action α α :=
                { one_smul := one_mul, mul_smul := mul_assoc }


                instance semiring.to_module [semiring α] :
                  module α α :=
                { zero_sfmul := zero_mul, add_smul := add_mul,
                  smul_zero := mul_zero, smul_add := mul_add }

Elementary actions Repeated addition

Another simple action, assuming [add_comm_monoid α]:

(3 : ℕ) • a = a + a + a


              def repeated_add [add_comm_monoid α] : ℕ → α → α
              | 0 a := 0
              | (n + 1) a := a + repeated_add n a

              instance nat_scalar [add_comm_monoid α] : has_scalar ℕ α :=
              { smul := repeated_add }


              instance nat_module [add_comm_monoid α] : module ℕ α := sorry
              instance nat_algebra [semiring α] : algebra ℕ α := sorry

Similarly given [add_comm_group α] / [ring α]:

(-3 : ℤ) • a = -(a + a + a)

Elementary actions Repeated addition

Example uses in mathlib:


              /-- The sum of a constant is a repeated addition. -/
              @[simp] theorem finset.sum_const {β α : Type*} [add_comm_monoid β]
                {s : finset α} (b : β) :
                ∑ x in s, b = s.card • b := sorry


            /-- An ordered additive commutative monoid is called `archimedean`
            if for any two elements `x`, `y` such that `0 < y` there exists a
            natural number `n` such that `x ≤ n • y`. -/
            class archimedean (α) [ordered_add_comm_monoid α] : Prop :=
            (arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)


              /-- Permuting the arguments of an alternating map scales the
              result by the sign of the permutation. -/
              theorem alternating_map.map_perm {R M N' ι : Type*}
                [semiring R] [add_comm_monoid M] [add_comm_group N]
                [module R M] [module R N] [decidable_eq ι] [fintype ι]
                (g : alternating_map R M N ι) (v : ι → M) (σ : equiv.perm ι) :
                g (v ∘ σ) = (σ.sign : ℤ) • g v := sorry

Elementary actions Elementwise multiplication

The $\mathbb{R}$-module structure on $\mathbb{R}^3$ (fin 3 → ℝ), $r \left[\begin{smallmatrix}x\mathstrut \\ y\mathstrut \\ z\mathstrut\end{smallmatrix}\right] = \left[\begin{smallmatrix}rx\mathstrut \\ ry\mathstrut \\ rz\mathstrut\end{smallmatrix}\right]$:

r • ![x, y, z] = ![r * x, r * y, r * z]


                  instance function.has_scalar (ι α : Type*) [has_mul α] :
                    has_scalar α (ι → α) :=
                  { smul := λ r v, (λ i, r * v i) }

The {$\mathbb{R}$, $\mathbb{R}_{\ge 0}$, $\mathbb{Q}$, …}-module structures on $\mathbb{R}^3$:

r • ![x, y, z] = ![r • x, r • y, r • z]

Derived actions

Derived actions Elementwise multiplication

r • ![x, y, z] = ![r * x, r * y, r * z]


                  instance function.has_scalar (ι α : Type*) [has_mul α] :
                    has_scalar α (ι → α) :=
                  { smul := λ r v, (λ i, r * v i) }

The {$\mathbb{R}$, $\mathbb{R}_{\ge 0}$, $\mathbb{Q}$, …}-module structures on $\mathbb{R}^3$:

r • ![x, y, z] = ![r • x, r • y, r • z]


              instance function.has_scalar' (ι M α : Type*) [has_scalar M α] :
                has_scalar M (ι → α) :=
              {smul := λ r v, (λ i, r • v i) }

Repeat for [mul_action M α], [module M α], …

Derived actions Compatibility constraints

has_scalar M (ι → α) was easy. has_scalar α (M →ₗ[R] N) is harder.


              instance {α R M N : Type*}
                [semiring R] [add_comm_monoid M] [add_comm_monoid N]
                [has_scalar α N] [module R M] [module R N] :
                has_scalar α (M →ₗ[R] N) :=
              { smul := λ a f,
                { to_fun := λ m, a • f m,
                  map_add' := λ m₁ m₂, (congr_arg _ $ f.map_add _ _).trans $
                    show a • (f m₁ + f m₂) = a • f m₁ + a • f m₂, from sorry,
                  map_smul' := λ r m, (congr_arg _ $ f.map_smul _ _).trans $
                    show a • r • f m = r • a • f m, from sorry } }

Now we have proof fields to fill out.


              instance {α R M N : Type*}
                [semiring R] [add_comm_monoid M] [add_comm_monoid N]
                [module α N] [module R M] [module R N] :
                has_scalar α (M →ₗ[R] N) :=
              { smul := λ a f,
                { to_fun := λ m, a • f m,
                  map_add' := λ m₁ m₂, (congr_arg _ $ f.map_add _ _).trans $
                    smul_add a (f m₁) (f m₂),
                  map_smul' := λ r m, (congr_arg _ $ f.map_smul _ _).trans $
                    show a • r • f m = r • a • f m, from sorry } }

Strengthening [has_scalar α N] to [module α N] closes the map_add' goal.


              instance {α R M N : Type*}
                [semiring R] [add_comm_monoid M] [add_comm_monoid N]
                [module α N] [module R M] [module R N] :
                has_scalar α (M →ₗ[R] N) :=
              { smul := λ a f,
                { to_fun := λ m, a • f m,
                  map_add' := λ m₁ m₂, (congr_arg _ $ f.map_add _ _).trans $
                    smul_add a (f m₁) (f m₂),
                  map_smul' := λ r m, (congr_arg _ $ f.map_smul _ _).trans $
                    show a • r • f m = r • a • f m, from sorry } }

Strengthening our existing assumptions doesn't help here.


              instance {α R M N : Type*}
                [semiring R] [add_comm_monoid M] [add_comm_monoid N]
                [module α N] [module R M] [module R N] [smul_comm_class α R N] :
                has_scalar α (M →ₗ[R] N) :=
              { smul := λ a f,
                { to_fun := λ m, a • f m,
                  map_add' := λ m₁ m₂, (congr_arg _ $ f.map_add _ _).trans $
                    smul_add a (f m₁) (f m₂),
                  map_smul' := λ r m, (congr_arg _ $ f.map_smul _ _).trans $
                    smul_comm a r (f m) } }

We need a new typeclass:


                class smul_comm_class (M N α : Type*)
                  [has_scalar M α] [has_scalar N α] : Prop :=
                (smul_comm : ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a)

Yury Kudryashovmathlib PR #4770: introduce smul_comm_class

The derived action on function types is straightforward, as the result of a smul f has no proof obligations. The same is not true when defining a scalar action on linear maps. We'll use this as an example of a typical workflow when defining more complex actions

Since our scalar action produces a linear map, our definition requires us to provide proofs the result is linear. We can make some progress on these proofs, but soon get stuck on the goals shown in the blue boxes.

The first of these goals is immediately recognizable as an axiom of a module, so we can close the goal by strenthening our assumption about the scalar action of alpha on N.

The second goals is harder, as it involves the interaction of two different scalar actions on N, and all the typeclasses we've seen so far are about a single action.

In this case, the solution is to define a new typeclass containing the statement we need; which is exactly what Yury did when adding the smul_comm_class typeclass. We can then add that to our assumptions, and our scalar action is complete.

Derived actions Compatibility constraints


            class smul_comm_class (M N α : Type*)
              [has_scalar M α] [has_scalar N α] : Prop :=
            (smul_comm : ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a)

Another similar typeclass:


            class is_scalar_tower (M N α : Type*)
              [has_scalar M N] [has_scalar N α] [has_scalar M α] : Prop :=
            (smul_assoc : ∀ (x : M) (y : N) (z : α), (x • y) • z = x • (y • z))

For example:


            -- the action of ℝ on ℂ³ factors through the action of ℂ on ℂ³
            instance : is_scalar_tower ℝ ℂ (fin 3 → ℂ) := by apply_instance

Valuable for working with field extensions*.

Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. NuccioA formalization of Dedekind domains and class groups of global fields

Algebras


              class is_scalar_tower (M N α : Type*)
                [has_scalar M N] [has_scalar N α] [has_scalar M α] : Prop :=
              (smul_assoc : ∀ (x : M) (y : N) (z : α), (x • y) • z = x • (y • z))


              class smul_comm_class (M N α : Type*)
                [has_scalar M α] [has_scalar N α] : Prop :=
              (smul_comm : ∀ (m : M) (n : N) (a : α), m • (n • a) = n • (m • a))

One way to construct an algebra instance in mathlib:


            def algebra.of_module (R A : Type*)
              [comm_semiring R] [semiring A] [module R A]
              (h₁ : ∀ (r : R) (x y : A), (r • x) * y = r • (x * y))
              (h₂ : ∀ (r : R) (x y : A), x * (r • y) = r • (x * y)) :
              algebra R A := sorry

x * y = x • y, so h₁ is is_scalar_tower R A A, and h₂ is smul_comm_class R A A!

Algebras


            def algebra.of_module (R A : Type*)
              [comm_semiring R] [semiring A] [module R A]
              (h₁ : ∀ (r : R) (x y : A), (r • x) * y = r • (x * y))
              (h₂ : ∀ (r : R) (x y : A), x * (r • y) = r • (x * y)) :
              algebra R A := sorry

x * y = x • y, so h₁ is is_scalar_tower R A A, and h₂ is smul_comm_class R A A!

Relaxing requirements of algebras:


              variables [comm_semiring R] [semiring A] [algebra R A]


                  variables
                    [comm_semiring R] [semiring A] [module R A]
                    [is_scalar_tower R A A] [smul_comm_class R A A]

An equivalent choice to above


                  variables
                    [comm_semiring R] [non_unital_non_assoc_semiring A] [module R A]
                    [is_scalar_tower R A A] [smul_comm_class R A A]

Useful^* when A behaves as a Lie algebra

Oliver Nash mathlib PR #7932: adjointness for the functor G ↦ monoid algebra k G when G carries only has_mul


                  variables
                    [comm_semiring R] [semiring A] [module R A]
                    [is_scalar_tower R A A] [smul_comm_class R A A]

An equivalent choice to above


                  variables
                    [monoid R] [semiring A] [distrib_mul_action R A]
                    [is_scalar_tower R A A] [smul_comm_class R A A]

Useful^† for actions by units, when R = units S.

Kexing Ying mathlib PR #7416: complex version of Sylvester’s law of inertia

Diamonds

Diamonds How typeclass diamonds originate

What does • in the following mean?


            variables (R : Type*) {ι A B : Type*}
            variables [add_comm_monoid A] [add_comm_monoid B]
            def double_nat (f : ι → A →+ B) := (2 : ℕ) • f


              variables [semiring R] [module R B]
              def double_any (f : ι → A →+ B) := (2 : R) • f

Is double_any ℕ = double_nat?

Paths taken: double_nat, double_any ℕ

Consider the following situation - we have an indexed collection of additive maps from A to B called f, and wish to scale it by the natural two. What does the action refer to here?

One thing it could mean is the module action inherited elementwise on each additive map, which in turn is inherited from the module structure on B.

The module structure on B is the natural number structure we looked at earlier derived from its additive structure.

But this natural number structure was available to us on the additive maps too...

and even directly on our collection of additive maps.
For this example there are three different paths to obtain the instance we need. We call this type of situation a "typeclass diamond", in reference to the shapes formed by the arrows.

To demonstrate why diamond matter, consider this similar definition, which scales by the two of some arbitrary semiring. Are these two definitions the same when we set R to N?

If we ask Lean, we find out that these two definitions took different paths

DiamondsTypes of equality

Propositional
- All $\mathbb{N}$-module structures must be equal, subsingleton (module ℕ α)
- Sufficient to satisfy the user that a • in the goal is one they meant.
Definitional
- Sufficient to satisfy Lean that a • in the goal is the • in other lemmas.

double_any ℕ = double_nat: propositional ✔, definitional ✘

Controlling definitional equality:^*


              class add_comm_monoid (M : Type*) :=
              (zero : M) (add : M → M → M)
              (nsmul : ℕ → M → M)  -- mathematically redundant
              (various_monoid_axioms : sorry)

Sébastien Gouëzelmathlib PR #7084: kill nat multiplication diamonds

Of course, just because the paths taken are different doesn't mean they're unequal. We need to remember that there are two types of equality in Lean; propositional, which is what a mathematician usually means when they say two things are equal, and definitional, which is what Lean uses when matching up terms.

Until very recently, while double_any was propositionally equal to double_nat, it was not definitionally equal. As a result, users of definitions like these could end up with an smul in their goal state which was not the one mathlib has lemmas about.

Sebastien contributed a fix to allow control of definitional equality in this situation by extending the axioms additive monoids, in this case by adding a new nsmul operation. Defining this operation correctly makes the diamond equal definitionally.

Future work

Future workRight actions

Left	Right
`(m₁ * m₂) • a = m₁ • m₂ • a` `a • b = a * b`	`a <• (m₁ * m₂) = a <• m₁ <• m₂` `a <• b = b * a`

Requirements and examples of actions

Choose op a • b = b <• a such that:


                (op m₂ * op m₁) • a = op m₂ • op m₁ • a

↔


                a <• (m₁ * m₂) = a <• m₁ <• m₂


              instance op_mul_action [monoid α] : mul_action (opposite α) α :=
              { smul := λ oa b, b * unop oa,  -- as opposed to `a * b`
                one_smul := mul_one,
                mul_smul := λ oa ob r, (mul_assoc _ _ _).symm }

Eric Wiesermathlib PR #7630: add has_scalar (opposite α) α instances.

Future workCompatibility of right actions

Bi-module require:

r • (m <• s) = (r • m) <• s

r • (op s • m) = op s • (r • m)

Lean assumptions:


              variables [module R M] [module (opposite S) M]
                        [smul_comm_class R (opposite S) M]

Enables work on sub-bimodules, two-sided ideals, …

No current typeclass: (a <• b) • c = a • (b •> c)
Needed for (a b c : α), {S : submonoid α} (a c : α) (b : S), (a b : α) (c : ι → α), …

Future workScalar actions in Lean 4

Lean 4^* generalizes has_mul.mul : α → α → α to HMul.hMul : α → β → γ
Possible replacements:
- notation: • → *
- left actions: has_scalar R M → HMul R M M
- right actions: has_scalar (opposite R) M → HMul M R M
- compatibility: is_scalar_tower R S M → HMulAssoc R S M
- compatibility: smul_comm_class R S M → HMulLeftComm R S M
It's likely best to wait for an initial port of Mathlib to Lean 4 before attempting this.

Leonardo de Moura and Sebastian UllrichThe lean 4 theorem prover and programming language

Future workMore diamonds

Non definitionally-equal diamonds remain in the algebra_map fields of:

Diamond instance	`algebra ℕ R`	`algebra ℤ R`	`algebra ℚ R`
Possible solution	`semiring.of_nat`	`ring.of_int`	`division_ring.of_rat`
	(and corresponding proof fields)

A recently discovered diamond:

Agrees definitionally on ↑(u₁ • u₂) but not ↑(u₁ • u₂)⁻¹.
✘ can be corrected with right actions!

There are other troublesome instance diamonds like the one we saw for the nat-module actions that need making definitionally equal. These apply to the stronger algebra structures for naturals, integers, and rationals, and manifest as non-definitionally equal algebra maps.

In a similar way to how Sebastien resolved these for the module instances, we could fix the definitionally equality by introducing a new data field to the various ring typeclasses, along with the constraints they must satisfy.

Two more problematic diamonds were discovered during the preparation of this presentation. Here we show the more interesting of these, which was the action of the units of a monoid on itself. This can either be found using the standard left-multiplication action (blue), or by chaining together the instances about actions on and by units (green). A nice way to fix the offending instance marked with ✘ would be to use right actions, which as mentioned earlier are not fully developed in mathlib.

Questions?

More about mathlib:
leanprover-community.github.io

Slides for this presentation:
eric-wieser.github.io/fmm-2021