## Stream: general

### Topic: init.algebra.classes

#### Johan Commelin (Mar 22 2019 at 14:04):

What is the purpose of this file: https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/library/init/algebra/classes.lean
It is used almost nowhere as far as I can see. It seems to be a sort of start of an algebraic hierarchy that is even unbundlerred than the current one...

#### Patrick Massot (Mar 22 2019 at 14:05):

Yes, this is Leo starting a new hierarchy, but Mario wasn't convinced so he didn't use it

#### Patrick Massot (Mar 22 2019 at 14:06):

But it leads to higher order unification problems that are not easy to handle

#### Patrick Massot (Mar 22 2019 at 14:06):

And I should really be grading exams...

#### Johan Commelin (Mar 22 2019 at 14:10):

@Mario Carneiro Are those problems documented somewhere?

#### Simon Hudon (Mar 22 2019 at 15:28):

I have also found those classes useful for rewriting modulo associativity and commutativity

#### Simon Hudon (Mar 22 2019 at 15:28):

It is not flexible enough to cover associativity of composition in category theory though

#### Johan Commelin (Mar 22 2019 at 15:32):

I guess one could try to write smarter tactics to get around the higher order unification problem. If smart_rw sees that you want to rewrite using a lemma tagged with algebra, then it looks in the goal to find terms that are "tagged" with binop (I'm making this up right now) and will try to plug those terms into the right slot of the rw-lemma.

#### Simon Hudon (Mar 22 2019 at 15:50):

The issue is not when you use an associativity lemma to rewrite. The issue is when you have an expression like f ≫ g ≫ h ≫ i and a lemma that could rewrite g ≫ h into something else

#### Johan Commelin (Mar 22 2019 at 15:51):

Like is_left_id?

No

#### Simon Hudon (Mar 22 2019 at 15:52):

You need to rely on associativity but indirectly

#### Johan Commelin (Mar 22 2019 at 15:53):

Ok, in the thread that I linked to above, Patrick was already having issues with is_left_id

#### Simon Hudon (Mar 22 2019 at 15:53):

Ah ok, I didn't see that

Last updated: May 16 2021 at 05:21 UTC