Semiring definition

Stream: mathlib4

[Martin Dvořák]

In the definition of a semiring

class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α

is the MonoidWithZero α requirement redundant?

[Robin Arnez]

Well, it's redundant in the sense that all the properties about + and * that constitute a Semiring are already in NonUnitalSemiring + NonAssocSemiring. However, for type-class resolution MonoidWithZero is used here to infer Monoid and MonoidWithZero from Semiring and Monoid and thus MonoidWithZero introduces a new operation: a ^ n for n : ℕ.

[Martin Dvořák]

Monoid could be an instance, couldn't it?
Why is it better to have it in the Semiring definition?

[Aaron Liu]

So that semiring inherits an npow field

[Martin Dvořák]

Why not to do something like

import Mathlib

class Semiring' (α : Type) extends NonUnitalSemiring α, NonAssocSemiring α

def myPow {α : Type} [Semigroup α] (_1 : α) (a : α) : ℕ → α
| 0 => _1
| n+1 => myPow _1 a n * a

instance (α : Type) [Semiring' α] : Monoid α where
  npow n a := myPow (1 : α) a n

example {T : Type} [Semiring' T] (x : T) : x ^ 3 * x ^ 2 = x ^ 5 := by
  noncomm_ring

but cleaner?

[Aaron Liu]

because it breaks the whole point of the npow field

[Aaron Liu]

the point is that you should be able to set it to what you want

[Adam Topaz]

Yeah, to expand a bit, we have such an npow field (and analogously zpow for groups) to be able to have these pow operations with good definitional properties. We then also include proofs saying that the pow operations agree (propositionally!) with the recursive definition. In practice these have default values so that you can choose whether or not to define an npow or just use the recursive version

[Aaron Liu]

for example if I have this better definition I want to use

def Int.betterPow (a : Int) (b : Nat) : Int :=
  if b % 2 = 0 ∨ 0 ≤ a then (a.natAbs ^ b : Nat)
  else -(a.natAbs ^ b : Nat)

[Aaron Liu]

I should be able to override the default implementation

[Martin Dvořák]

Thanks for explanation!