Double TC extends

Stream: lean4

[Gabriel DORIATH DÖHLER]

Lets say that we want to define Ring from its two projections on Monoid:

class Monoid (a : Type u) where
  e : a
  mop : a -> a -> a
  properties : ...

class Ring (a : Type u) where
  toAddMonoid : Monoid a
  toMulMonoid : Monoid a
  (add := toAddMonoid.mop)
  (mul := toMulMonoid.mop)
  (zero := toAddMonoid.e)
  (one := toMulMonoid.e)
  opp : ...
  properties : ...

But it would be nicer to use the extends syntax (I think it will automatically add an instance to deduce Monoid from Ring) :

class Monoid ...

class Ring (a : Type u) extends Monoid a, Monoid a where
  (toAddMonoid := toMonoid)
  (toMulMonoid := toMonoid_1)
  -- The same as before
  (add := toAddMonoid.mop)
  (mul := toMulMonoid.mop)
  (zero := toAddMonoid.e)
  (one := toMulMonoid.e)
  opp : ...
  properties : ...

Lean generates the fields Ring.toMonoid (as expected) and Ring.toMonoid_1.
So it works just as expected? Well, not really...
When defining a Ring instance, we can specify toMonoid but not toMonoid_1 and then lean chooses toMonoid_1 := toMonoid.
What am I doing wrong?

[Gabriel DORIATH DÖHLER]

Oups I forgot to test one thing: toMonoid_1 isn't available in the definition of Ring. So some of the handy notations like muland one create errors and should instead be declared separately.

[Gabriel Ebner]

You might want to look at how we do this in mathlib: https://github.com/leanprover-community/mathlib4/blob/3d0564ad89b3996f73a499f24f8f92e7b1778323/Mathlib/Algebra/Ring/Basic.lean#L18

We have separate hierarchies for "additive" and "multiplicative" structures (depending on whether you write them with + or *) and then Ring can extend semigroup twice (once additive, once multiplicative, so there's no clash). It's the same in Lean 3.

[Kevin Buzzard]

I am not an expert in this typeclass stuff but you have defined Monoid to be a class here so lean will expect at most one instance of Monoid α for type class inference to function properly, and you are giving it two. The way we work around this in lean 3 is that we define... What Gabriel just said

[Kevin Buzzard]

I remember at the time thinking that having two group heirarchies was crazy but now I think it's a stroke of genius. Often in an introductory group theory class someone might intentionally use some exotic character to denote the group law, but in practice mathematicians either use + or * and furthermore they often have a very good reason for their choice

[Yakov Pechersky]

You could do something like "extends Monoid a, Monoid (additive a)"?

[Yakov Pechersky]

But then the fields clash anyway