Zulip Chat Archive

Stream: general

Topic: init.algebra.classes


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

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

view this post on Zulip Patrick Massot (Mar 22 2019 at 14:06):

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

view this post on Zulip Patrick Massot (Mar 22 2019 at 14:06):

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

view this post on Zulip Patrick Massot (Mar 22 2019 at 14:06):

And I should really be grading exams...

view this post on Zulip Johan Commelin (Mar 22 2019 at 14:10):

@Mario Carneiro Are those problems documented somewhere?

view this post on Zulip Johan Commelin (Mar 22 2019 at 14:15):

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

view this post on Zulip Simon Hudon (Mar 22 2019 at 15:28):

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

view this post on Zulip Simon Hudon (Mar 22 2019 at 15:28):

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

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

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

view this post on Zulip Johan Commelin (Mar 22 2019 at 15:51):

Like is_left_id?

view this post on Zulip Simon Hudon (Mar 22 2019 at 15:52):

No

view this post on Zulip Simon Hudon (Mar 22 2019 at 15:52):

You need to rely on associativity but indirectly

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

view this post on Zulip Simon Hudon (Mar 22 2019 at 15:53):

Ah ok, I didn't see that


Last updated: May 16 2021 at 05:21 UTC