to_additive

Stream: lean4

[Johan Commelin]

One thing I would like to experiment with (but I won't have time until teaching is done ~ 4 weeks from now) is the add-vs-mul stuff.

• Does fully-bundled + unification hints make it easier to have only Group?
• What are the 37 problems we will hit, when there are 2 paths from Semiring to Monoid?
• Can we have notation agnostic Group/Semiring/Monoid, and use the new macro system to have nice and readable notation anyway?
• ...

[Mario Carneiro]

What advantage does a notation agnostic Group have, if the theory is still being duplicated for add/mul? It would just mean 3 copies instead of 2, and with really awkward naming and notation for one of them

[Johan Commelin]

No... I would want to know if it's possible to do with just 1 copy.

[Johan Commelin]

Are there new Lean features that we can leverage to make that happen, and still have readable code?

[Mario Carneiro]

We need theorems named add_assoc and mul_assoc independent of any behind the scenes shenanigans

[Mario Carneiro]

so we are already committed to some amount of duplication, even if it's only instantiating one as the other

[Mario Carneiro]

we already have the means to create readable, non-duplicated code that generates 2 copies, via @[to_additive]

[Mario Carneiro]

but we could invest in a tactic to allow applying e.g. mul_assoc even when the application does not use mul, both to make the proof of the additive version not require replaying the whole proof, and also to allow using it in situations that use neither notation, e.g. \comp or ++

[Johan Commelin]

Mario Carneiro said:

We need theorems named add_assoc and mul_assoc independent of any behind the scenes shenanigans

Why exactly do we need this? It's not clear to me that in theory we can't get away with assoc.

[Floris van Doorn]

I don't know what problems we are trying to solve with bundled structures + canonical instances, but I think that typeclasses are way nicer.

Suppose I write everything multiplicative for now (not worrying about additive stuff). Suppose I want to rewrite with mul_assoc. I'm looking for (_ * _) * _. What does * mean here? Group.mul, i.e. one of the fields for Group? That of course doesn't work, since I will also have CommGroup.mul, Ring.mul etc.

[Johan Commelin]

Isn't it going to be SemiGroup.mul? And then you need coercions to kick in?

[Johan Commelin]

But the issue you're raising has certainly been solved in mathcomp

[Floris van Doorn]

While I won't discourage any experiments with any of this, I would not put your hopes too high.

Here is a paper that is about packed classes, used in mathcomp: https://arxiv.org/pdf/2002.00620.pdf

Here is a paragraph from page 2:

In spite of its success, the packed classes methodology is hard to master
for library designers and requires a substantial amount of work to maintain as
libraries evolve. For instance, the strict application of packed classes requires
defining quadratically many implicit coercions and unification hints in the number of structures.
To give some figures, the MathComp library 1.10.0 uses this
methodology ubiquitously to define the 51 mathematical structures depicted in
Fig. 1, and declares 554 implicit coercions and 746 unification hints to implement their inheritance.
Moreover, defining new intermediate structures between
existing ones requires fixing their subclasses and their inheritance accordingly;
thus, it can be a challenging task

[Johan Commelin]

Hmm, thanks for that quote.

[Floris van Doorn]

This "quadratically many implicit coercions and unification hints" is pretty bad, but I'm not even sure if that is the worst. We can limit the number of classes we have by having multiple classes on 1 type, e.g. [fintype F] [field F]. If you do everything bundled you need to define a bundled structure for every combination. For example, in Figure 1 you see that there is ringType, groupType and fieldType, but also finRingType, finGroupType, countRingType, decFieldType, etc.
I think that requires exponentially many structures, which would be already be way too large for the current size of mathlib.

[Floris van Doorn]

Imagine having topologicalGroup, topologicalCommGroup, hausdorffTopologicalGroup compactSecondCountableTopologicalRing, ...

[Mario Carneiro]

I don't think the "quadratically many implicit coercions and unification hints" is actually that bad. That's the amount of extra setup you have to do to set up the hierarchy itself; it is basically precomputing all shortcut instances. The benefit is that the equivalent of typeclass instance searches become way shorter. Plus I think it would be quite reasonable, if we were to implement this strategy, to have a similar "hierarchy builder" tactic to what mathcomp itself uses (now, after a long manual history)

[Mario Carneiro]

Floris van Doorn said:

Imagine having topologicalGroup, topologicalCommGroup, hausdorffTopologicalGroup compactSecondCountableTopologicalRing, ...

I believe the coq answer to this is mixins. They work pretty similar to the instances like second_countable A that we already use

[Mario Carneiro]

(None of this is to say that I advocate switching, but I can believe that lean 4 makes it possible to actually build a working mathcomp style hierarchy)

[Floris van Doorn]

My impression was that mixins were used only to define new bundled structures, but I might be wrong with that. But if I'm wrong, then I'm wondering why they duplicated all their structures with finite structures.
If you use a mixin in a theorem statement, it better be a type class (right?). And now you're doing both type-class inference and unification hints.

[Johan Commelin]

Of course we've also been floating around this idea of having [[topological_group G]] do something like:

• Observe that [topological_group G] needs G : Type*, [topological_space G] and [group G] to make sense.
• Check if G exists as variable. If not, add it (at least locally).
• Use typeclass resolution to check if [topological_space G] can be derived from the current environment. If not, add the assumption locally.
• Idem dito for [group G].

@Sebastian Ullrich does :up: sound like something that is in scope for a macro?

[Sebastian Ullrich]

This could potentially be an elaborator in the binder category, though none of these exist ATM. Note that your second point should be covered by https://leanprover.github.io/lean4/doc/autobound.html. AFAIR, @Leonardo de Moura and I consciously decided not to auto-bind typeclass instance arguments since it's hard to tell whether a user deliberately elided them or thinks they should be implied by the current assumptions, in which case we would unexpectedly add new ones. Perhaps a new notation for that isn't the worst idea, especially when it can be implemented and experimented with outside of core.

[Sebastien Gouezel]

I can read that you only autobound "a single lower case or greek letter". We tend to use upper case letters as types (or weird letters such as 𝕜, for which I don't know how it counts). Is this something we will be able to customize in mathlib?

[Sebastian Ullrich]

Ah, that's true...

[Kyle Miller]

Along these lines, I was wondering about having "abbreviation classes." These would be classes that extend some number of classes and have no members themselves, and whenever they appear they should behave as if they are replaced by all the classes they extend.

A bit more precisely,

abbreviation class Foo (α : Type*) extends C1 α, C2 α, C3 α

indicates that a [Foo α] should mean [C1 α] [C2 α] [C3 α], and whenever a class extends Foo, it would actually extend these three classes. Under the hood, there should be an actual class for Foo that records the instances, so the typeclass resolution can be more easily cached -- there would be an instance for Foo α whenever instances for the classes being extended exist, so abbreviation class should mean something like:

class Foo (α : Type*) extends C1 α, C2 α, C3 α
instance (α : Type*) [C1 α] [C2 α] [C3 α] : Foo α := {}

It can't be exactly this because it would create infinite loops in typeclass resolution: Foo provides, for example, a C1 instance, so if you need a C1 instance then typeclass resolution would try to find a Foo instance, which needs a C1 instance, and so on. The automatic instance for abbreviation classes needs to be special in some way to prevent this infinite loop.

What this feature would support is having all algebraic structures being mixins of basic operations and axioms. The Lean 3 mockup below illustrates how a commutative monoid would automatically be a monoid, a commutative semigroup, and a semigroup. This is just because [comm_monoid α] would be roughly equivalent to saying [has_mul α] [has_mul_assoc α] [has_one α] [has_mul_one α] [has_mul_comm α] (though, again, you'd probably only want to pass a single comm_monoid instance argument in the implementation). This setup should also make it easier to generate automatic universal algebra constructions (forgetful functors are completely trivial, and the right adjoints to these should be macro-ize-able -- I've done them by hand for a few cases).

namespace flat_structures
universes u v

/- from core:
class has_one      (α : Type u) := (one : α)
class has_mul      (α : Type u) := (mul : α → α → α)
-/

class has_mul_assoc (α : Type u) [has_mul α] :=
(mul_assoc : Π (a b c : α), a * b * c = a * (b * c))

class has_mul_one (α : Type u) [has_mul α] [has_one α] :=
(one_mul : Π (a : α), 1 * a = a) (mul_one : Π (a : α), a * 1 = a)

class has_mul_comm (α : Type u) [has_mul α] :=
(mul_comm : Π (a b : α), a * b = b * a)

abbreviation class semigroup (α : Type u) extends has_mul α, has_mul_assoc α
abbreviation class monoid (α : Type u) extends semigroup α, has_one α, has_mul_one α
abbreviation class comm_semigroup (α : Type u) extends semigroup α, has_mul_comm α
abbreviation class comm_monoid (α : Type u) extends monoid α, has_mul_comm α

section inferences
variables (α : Type u) [comm_monoid α]
example : semigroup α := infer_instance
example : monoid α := infer_instance
example : comm_semigroup α := infer_instance  -- Cannot infer this using usual `extends`
end inferences

end flat_structures

[Kyle Miller]

Abbreviation classes make it easier to use a certain solution to the so-called "expression problem," where functions can specify exactly which properties of an object they make use of. Furthermore, it seems it allows property classes to be refactored without changing user code.

[Sebastian Ullrich]

Kyle Miller said:

It can't be exactly this because it would create infinite loops in typeclass resolution

Not an issue for the Lean 4 typeclass inference

[Jacques Carette]

Wait until you also want to put loops, racks, quandles, squags, dioids, spindles and shelfs in the same library, in a backwards compatible manner. Just because they are not yet 'mainstream' mathematics makes them no less mathematics.

It's also quite fun to formalize the very large set of modal logics out there. It's a fun exercise in meta-mathematics, because any mathematician that values elegance in the least bit will bridle at the amount of duplication they're forced to do in any system that does handle (6+ dimensional!) diamonds seamlessly.

The problem with assoc that @Mario Carneiro mentions is huge. And it of course is not specific to assoc, but a symptom of every law: they end up needing to be either human-duplicated, or the 'renaming' problem involved in transporting them from their origin to their use site (where there might be multiple uses) is quite large. I've implemented a couple of hacky solutions in 2 of my systems - and I would not recommend either of those 'solutions' to anyone.

[tiny rant: The thing with proof systems is that the effort of doing all the proofs is quite significant, so that tends to swallow all the air available, and that's not unreasonable. The problem is that it doesn't leave room left for people to notice just how much duplication there is in their tapestry of theories, definitions and lemmas. end rant]

[Kyle Miller]

We at least have docs#shelf, docs#rack, and docs#quandle (and the conjugation quandle docs#quandle.conj of a group) -- I've heard of loops and spindles, but the other two must be made up! :smile: (Note: shelves are only halfheartedly implemented, and they're only left shelves.)

Just to add some more complexity to your list, how about also having biracks and biquandles in the same library? (It would be nice to eventually have these: they are actually studied in quantum topology to describe factorizations in quantum groups.)

[Nick Scheel]

I’ve always thought that in DTTs, classes should take their operations as parameters, because the identities, inverses, and laws are propositionally-uniquely determined from that, and of course the type can be unification-inferred from the operation (or vice-versa: you need to fix the type to say the operation). That is, instead of Group Nat you would have Group Nat (+) (or maybe just Group (+)). I think it might even play nicely with has_add and has_mul, which are allowed to pick canonical operations for types, while Group would always be told its operation. But of course I don’t spend enough time in proof assistants these days to evaluate my proposal myself ...

[Kevin Buzzard]

I have been surprised myself about how effective the lean approach to this has been. It makes code more readable and seems to have surprisingly few disadvantages.

[Johan Commelin]

@Nick Scheel I think the problem with that approach is that it leads to exponential blow-up in term sizes. Let me try to find the blogpost that explains that.

[Johan Commelin]

@Nick Scheel voila: https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html

[Nick Scheel]

Oh I was just going to ask if it was that post. My understanding is that the style discussed there is just Group A not Group A (+), i.e. mathlib’s current style.

[Johan Commelin]

@Nick Scheel no, it seems to be the other way round

[Nick Scheel]

Oh, I see. I misunderstood arguments vs superclasses. I was only proposing that the operation be an argument, and the rest of the hierarchy would be superclasses (or fields), so it would only be quadratic, I believe.

[Eric Wieser]

Am I right in thinking that the blow-up is irrelevant as long we define AddGroup A := Group A (+) at some level in the API, and use that for higher-level things?

[Eric Wieser]

From that blog post:

Taking the superclasses as indices instead of embedding them as fields simplifies typeclass search and is necessary to support diamonds in the hierarchy

This sounds like a coq problem that may not translate to lean, unless I'm missing something - my impression is only Op, Unit and Inv need to be arguments, which means that instead of a monster term like Group A (_ : Monoid A (_ : SemiGroup A (*)) 1 inv) as that blog seems to suggest, we can use a shorter Group A (*) 1 inv - so the blow-up does not increase with the depth of the heirarchy, it just increases by one over what we currently have

[Leonardo de Moura]

BTW, I added an example showing how to use unification hints and type classes simultaneously. It creates a bridge between the bundled (Magma in the example) and unbundled (Mul in the example) worlds.
https://github.com/leanprover/lean4/blob/master/tests/lean/unifHintAndTC.lean#L46-L53
Disclaimer: we don't need this feature to implement Lean. So, we don't know how reliable it is.

[Kyle Miller]

Thanks to Lean 4's typeclass resolution algorithms, it's possible to make typeclasses that represent when certain operations and axioms are available for a type -- there's no difference between a commutative monoid and a monoid with commutative multiplication. The pattern automatically gives you the full poset of algebraic structures with the given operations and axioms.

Before going to that code, I should mention that I tried combining multiplication and addition into single classes with things like

class HasComm (α : Type u) (op : α → α → α) : Prop where
    comm : ∀ x y, op x y = op y x
export HasComm (comm)

class HasMulComm (α : Type u) [Mul α] extends HasComm α HMul.hMul
def mulComm [Mul α] [h : HasMulComm α] := h.comm

class HasAddComm (α : Type u) [Add α] extends HasComm α HAdd.hAdd
def addComm [Add α] [h : HasAddComm α] := h.comm

but the issue I ran into is that you get name conflicts when you try to extend both HasMulComm and HasAddComm.

Anyway, here's the algebraic hierarchy I was experimenting with. The pattern is to (1) split off all axioms as classes and (2) give the constructors for the algebraic objects the instance attribute so that they are automatically constructed when all the axioms are available. If it's not too expensive, you can add instances when certain collections of axioms imply others to help "coerce" algebraic objects. Below I made it so that a Ring is a Semiring by adding the instance that a Ring has ZeroMul.

/- from core:
class OfNat (α : Type u) (n : Nat) where
  ofNat : α
class Mul (α : Type u) where
  mul : α → α → α
class Add (α : Type u) where
  add : α → α → α
-/

class Inv (α : Type u) where
    inv : α → α

postfix:max "⁻¹" => Inv.inv

class One (α : Type u) where
    one : α
export One (one)

instance [One α] : OfNat α (natLit! 1) where
    ofNat := one

class Zero (α : Type u) where
    zero : α
export Zero (zero)

instance [Zero α] : OfNat α (natLit! 0) where
    ofNat := zero

class MulComm (α : Type u) [Mul α] : Prop where
    mulComm : {a b : α} → a * b = b * a
export MulComm (mulComm)

class MulAssoc (α : Type u) [Mul α] : Prop where
    mulAssoc : {a b c : α} → a * b * c = a * (b * c)
export MulAssoc (mulAssoc)

class OneUnit (α : Type u) [Mul α] [One α] : Prop where
    oneMul : {a : α} → 1 * a = a
    mulOne : {a : α} → a * 1 = a
export OneUnit (oneMul mulOne)

class AddComm (α : Type u) [Add α] : Prop where
    addComm : {a b : α} → a + b = b + a
export AddComm (addComm)

class AddAssoc (α : Type u) [Add α] : Prop where
    addAssoc : {a b c : α} → a + b + c = a + (b + c)
export AddAssoc (addAssoc)

class ZeroUnit (α : Type u) [Add α] [Zero α] : Prop where
    zeroAdd : {a : α} → 0 + a = a
    addZero : {a : α} → a + 0 = a
export ZeroUnit (zeroAdd addZero)

class InvMul (α : Type u) [Mul α] [One α] [Inv α] : Prop where
    invMul : {a : α} → a⁻¹ * a = 1
export InvMul (invMul)

class NegAdd (α : Type u) [Add α] [Zero α] [Neg α] : Prop where
    negAdd : {a : α} → -a + a = 0
export NegAdd (negAdd)

class ZeroMul (α : Type u) [Mul α] [Zero α] : Prop where
    zeroMul : {a : α} → 0 * a = 0
export ZeroMul (zeroMul)

class Distrib (α : Type u) [Add α] [Mul α] : Prop where
    leftDistrib : {a b c : α} → a * (b + c) = a * b + a * c
    rightDistrib : {a b c : α} → (a + b) * c = a * c + b * c
export Distrib (leftDistrib rightDistrib)

class Domain (α : Type u) [Mul α] [Zero α] : Prop where
    eqZeroOrEqZeroOfMulEqZero : {a b : α} → a * b = 0 → a = 0 ∨ b = 0
export Domain (eqZeroOrEqZeroOfMulEqZero)

class Semigroup (α : Type u) extends Mul α, MulAssoc α
attribute [instance] Semigroup.mk

class AddSemigroup (α : Type u) extends Add α, AddAssoc α
attribute [instance] AddSemigroup.mk

class Monoid (α : Type u) extends Semigroup α, One α, OneUnit α
attribute [instance] Monoid.mk

class AddMonoid (α : Type u) extends AddSemigroup α, Zero α, ZeroUnit α
attribute [instance] AddMonoid.mk

class CommSemigroup (α : Type u) extends Semigroup α, MulComm α
attribute [instance] CommSemigroup.mk

class CommMonoid (α : Type u) extends Monoid α, MulComm α
attribute [instance] CommMonoid.mk

class Group (α : Type u) extends Monoid α, Inv α, InvMul α
attribute [instance] Group.mk

class AddGroup (α : Type u) extends AddMonoid α, Neg α, NegAdd α
attribute [instance] AddGroup.mk

class Semiring (α : Type u) extends AddMonoid α, Monoid α, AddComm α, ZeroMul α, Distrib α
attribute [instance] Semiring.mk

class Ring (α : Type u) extends AddGroup α, Monoid α, AddComm α, Distrib α
attribute [instance] Ring.mk

class CommRing (α : Type u) extends Ring α, MulComm α
attribute [instance] CommRing.mk

class IntegralDomain (α : Type u) extends CommRing α, Domain α
attribute [instance] IntegralDomain.mk

section test1
variables (α : Type u) [h : CommMonoid α]
example : Semigroup α := inferInstance
example : Monoid α := inferInstance
example : CommSemigroup α := inferInstance
end test1

section test2
variables (β : Type u) [CommSemigroup β] [One β] [OneUnit β]
example : Monoid β := inferInstance
example : CommMonoid β := inferInstance
example : Semigroup β := inferInstance
end test2

section test3
variables (β : Type u) [Mul β] [One β] [MulAssoc β] [OneUnit β]
example : Monoid β := inferInstance
example : Semigroup β := inferInstance
end test3

theorem negZero [AddGroup α] : -(0 : α) = 0 := by
    rw [←addZero (a := -(0 : α)), negAdd]

theorem subZero [AddGroup α] {a : α} : a + -(0 : α) = a := by
    rw [←addZero (a := a), addAssoc, negZero, addZero]

theorem negNeg [AddGroup α] {a : α} : -(-a) = a := by {
    rw ←addZero (a := - -a);
    rw ←negAdd (a := a);
    rw ←addAssoc;
    rw negAdd;
    rw zeroAdd;
}

theorem addNeg [AddGroup α] {a : α} : a + -a = 0 := by {
    have h : - -a + -a = 0 := by { rw negAdd };
    rw negNeg at h;
    exact h
}

theorem addIdemIffZero [AddGroup α] {a : α} : a + a = a ↔ a = 0 := by
    apply Iff.intro
    focus
        intro h
        have h' := congrArg (λ x => x + -a) h
        simp at h'
        rw [addAssoc, addNeg, addZero] at h'
        exact h'
    focus
        intro h
        subst a
        rw addZero

instance [Ring α] : ZeroMul α := by {
    apply ZeroMul.mk;
    intro a;
    have h : 0 * a + 0 * a = 0 * a := by { rw [←rightDistrib, addZero] };
    rw addIdemIffZero (a := 0 * a) at h;
    rw h;
}

example [Ring α] : Semiring α := inferInstance

[Eric Wieser]

This looks like exactly the design that someone complained gives exponential blow-up due to every type in the heirarchy being indexed by all the previous types. Perhaps that applies only to Coq / whatever language the blog they linked complained about

[Kyle Miller]

I think a difference is that this is able to cache intermediate instances. If you have a Ring and a MulComm, then the term for CommRing is that pair of instances -- it doesn't have to go all the way down to the basic operations and axioms every time. There is a "fast path" for coercion depending on which objects you extend to define the new object. (I'd only looked at a couple of terms to see whether the exponential blowup happened. By my non-expert eye it didn't look like it happened, but I'm really not sure. It probably would happen when the object being coerced doesn't have a nearby common ancestor.)

[Eric Wieser]

To be clear, the blow up I'm recalling is in term size, not typeclass search duration

[Kyle Miller]

Yeah, that's what I was referring to.

[Kyle Miller]

Here's a quick test of this. I added instances for products of groups, mirroring the one in the article, and then I printed out #reduce of the instance with set_option pp.all true. I then counted the characters in the message (excluding spaces, since the pretty printer does indenting) and got this graph:

image.png

Code:

section prod

instance [Mul α] [Mul β] : Mul (α × β) where
    mul p p' := (p.1 * p'.1, p.2 * p'.2)

instance [Inv α] [Inv β] : Inv (α × β) where
    inv p := (p.1⁻¹, p.2⁻¹)

instance [One α] [One β] : One (α × β) where
    one := (1, 1)

theorem Product.ext : {p q : α × β} → p.1 = q.1 → p.2 = q.2 → p = q
    | (a, b), (c, d) => by simp; intro h; subst a; intro h; subst b; rfl

instance [Semigroup α] [Semigroup β] : Semigroup (α × β) where
    mulAssoc := by
        apply Product.ext
        apply mulAssoc
        apply mulAssoc

instance [Monoid α] [Monoid β] : Monoid (α × β) where
    oneMul := by
        apply Product.ext
        apply oneMul
        apply oneMul
    mulOne := by
        apply Product.ext
        apply mulOne
        apply mulOne

instance [Group α] [Group β] : Group (α × β) where
    invMul := by
        apply Product.ext
        apply invMul
        apply invMul

end prod

def test1 {G : Type _} [Group G]: Group (G) := inferInstance
def test2 {G : Type _} [Group G]: Group (G × G) := inferInstance
def test3 {G : Type _} [Group G]: Group (G × G × G) := inferInstance
def test4 {G : Type _} [Group G]: Group (G × G × G × G) := inferInstance
def test5 {G : Type _} [Group G]: Group (G × G × G × G × G) := inferInstance
def test6 {G : Type _} [Group G]: Group (G × G × G × G × G × G) := inferInstance
def test7 {G : Type _} [Group G]: Group (G × G × G × G × G × G × G) := inferInstance
def test8 {G : Type _} [Group G]: Group (G × G × G × G × G × G × G × G) := inferInstance

set_option pp.all true
#reduce @test8

This is what the term for test8 looked like:

fun {G} [inst : Group.{u_1} G] =>
  @Group.mk.{u_1}
    (Prod.{u_1, u_1} G
      (Prod.{u_1, u_1} G
        (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G)))))))
    (@instMonoidProd.{u_1, u_1} G
      (Prod.{u_1, u_1} G
        (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))))
      (@Group.toMonoid.{u_1} G inst)
      (@Group.toMonoid.{u_1}
        (Prod.{u_1, u_1} G
          (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))))
        (@instGroupProd.{u_1, u_1} G
          (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))) inst
          (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))
            inst
            (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))) inst
              (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G)) inst
                (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G G) inst (@instGroupProd.{u_1, u_1} G G inst inst))))))))
    (@instInvProd.{u_1, u_1} G
      (Prod.{u_1, u_1} G
        (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))))
      (@Group.toInv.{u_1} G inst)
      (@Group.toInv.{u_1}
        (Prod.{u_1, u_1} G
          (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))))
        (@instGroupProd.{u_1, u_1} G
          (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))) inst
          (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))
            inst
            (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))) inst
              (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G)) inst
                (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G G) inst (@instGroupProd.{u_1, u_1} G G inst inst))))))))
    (@instGroupProd.proof_1.{u_1, u_1} G
      (Prod.{u_1, u_1} G
        (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))))
      inst
      (@instGroupProd.{u_1, u_1} G
        (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))) inst
        (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))))
          inst
          (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G))) inst
            (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G (Prod.{u_1, u_1} G G)) inst
              (@instGroupProd.{u_1, u_1} G (Prod.{u_1, u_1} G G) inst (@instGroupProd.{u_1, u_1} G G inst inst)))))))

[Eric Wieser]

Nevermind, I now see how this avoids the limitations of the versions I was thinking of - you're taking advantage of dependent types in the extends clause

[Leonardo de Moura]

@Kyle Miller Thanks. This is a useful experiment. I added it to the test suite. BTW, the internal expressions are much smaller since they are shared. Here is your example + code for computing the actual "number of Expr objects used by Lean"
https://github.com/leanprover/lean4/blob/c78a06d9a5553e8ffc5ffeeb7ba75fd271bc272e/tests/lean/run/KyleAlg.lean#L262-L278

[Scott Viteri]

Suppose I use this technique and fill out the appropriate instances for Bool. Is there a more efficient way of writing the following?

instance : Semiring Bool :=
 { zero := Zero.zero, one := One.one, mul := Mul.mul, add := Add.add, addComm := AddComm.addComm,
   oneMul := OneUnit.oneMul, mulOne := OneUnit.mulOne }

[Scott Viteri]

nevermind thx Mario instance : Semiring Bool := {}