# Zulip Chat Archive

## Stream: lean4

### Topic: to_additive

#### Johan Commelin (Jan 07 2021 at 06:28):

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 (Jan 07 2021 at 06:32):

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 (Jan 07 2021 at 06:56):

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

#### Johan Commelin (Jan 07 2021 at 06:56):

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

#### Mario Carneiro (Jan 07 2021 at 07:02):

We need theorems named `add_assoc`

and `mul_assoc`

independent of any behind the scenes shenanigans

#### Mario Carneiro (Jan 07 2021 at 07:02):

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

#### Mario Carneiro (Jan 07 2021 at 07:04):

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

#### Mario Carneiro (Jan 07 2021 at 07:06):

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 (Jan 07 2021 at 07:13):

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 (Jan 07 2021 at 07:22):

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 (Jan 07 2021 at 07:23):

Isn't it going to be `SemiGroup.mul`

? And then you need coercions to kick in?

#### Johan Commelin (Jan 07 2021 at 07:24):

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

#### Floris van Doorn (Jan 07 2021 at 07:38):

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 (Jan 07 2021 at 07:43):

Hmm, thanks for that quote.

#### Floris van Doorn (Jan 07 2021 at 07:46):

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 (Jan 07 2021 at 07:50):

Imagine having `topologicalGroup`

, `topologicalCommGroup`

, `hausdorffTopologicalGroup`

`compactSecondCountableTopologicalRing`

, ...

#### Mario Carneiro (Jan 07 2021 at 08:06):

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 (Jan 07 2021 at 08:09):

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 (Jan 07 2021 at 08:10):

(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 (Jan 07 2021 at 08:20):

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 (Jan 07 2021 at 10:06):

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 (Jan 07 2021 at 12:00):

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 (Jan 07 2021 at 12:11):

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 (Jan 07 2021 at 12:14):

Ah, that's true...

#### Kyle Miller (Jan 08 2021 at 20:09):

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 (Jan 08 2021 at 20:40):

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 (Jan 09 2021 at 10:19):

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 (Jan 10 2021 at 15:38):

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 (Jan 10 2021 at 16:41):

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 (Jan 11 2021 at 06:40):

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 (Jan 11 2021 at 07:11):

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 (Jan 11 2021 at 07:11):

@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 (Jan 11 2021 at 07:15):

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

#### Nick Scheel (Jan 11 2021 at 07:17):

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 (Jan 11 2021 at 07:51):

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

#### Nick Scheel (Jan 11 2021 at 08:24):

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 (Jan 11 2021 at 13:06):

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 (Jan 11 2021 at 13:14):

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 (Jan 12 2021 at 15:15):

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 (Jan 20 2021 at 19:29):

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 (Jan 20 2021 at 19:48):

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 (Jan 20 2021 at 19:53):

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 (Jan 20 2021 at 19:59):

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

#### Kyle Miller (Jan 20 2021 at 19:59):

Yeah, that's what I was referring to.

#### Kyle Miller (Jan 20 2021 at 20:52):

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:

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 (Jan 20 2021 at 21:39):

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 (Jan 21 2021 at 18:43):

@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 (Apr 24 2021 at 23:09):

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 (Apr 25 2021 at 02:53):

nevermind thx Mario `instance : Semiring Bool := {}`

Last updated: May 07 2021 at 13:21 UTC