init.algebra.classes

Stream: general

[Johan Commelin]

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]

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

[Patrick Massot]

I use it in https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean

[Patrick Massot]

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

[Patrick Massot]

And I should really be grading exams...

[Johan Commelin]

@Mario Carneiro Are those problems documented somewhere?

[Johan Commelin]

Aaah, I just found: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/is_left_id.20rw.20mystery

[Simon Hudon]

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

[Simon Hudon]

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

[Johan Commelin]

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]

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]

Like is_left_id?

[Simon Hudon]

No

[Simon Hudon]

You need to rely on associativity but indirectly

[Johan Commelin]

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

[Simon Hudon]

Ah ok, I didn't see that