Zulip Chat Archive

Stream: lean4

Topic: to_additive


view this post on Zulip 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?
  • ...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 07 2021 at 06:56):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 07 2021 at 07:02):

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

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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 ++

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 07 2021 at 07:23):

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

view this post on Zulip Johan Commelin (Jan 07 2021 at 07:24):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 07 2021 at 07:43):

Hmm, thanks for that quote.

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Jan 07 2021 at 07:50):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (Jan 07 2021 at 12:14):

Ah, that's true...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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.)

view this post on Zulip 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 ...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 11 2021 at 07:15):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 11 2021 at 07:51):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Kyle Miller (Jan 20 2021 at 19:59):

Yeah, that's what I was referring to.

view this post on Zulip 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:

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)))))))

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip Scott Viteri (Apr 25 2021 at 02:53):

nevermind thx Mario instance : Semiring Bool := {}


Last updated: May 07 2021 at 13:21 UTC