Zulip Chat Archive

Stream: maths

Topic: abel multiplication


view this post on Zulip Patrick Massot (May 29 2019 at 17:26):

It seems that abel works only for add_comm_group, not for comm_group. @Mario Carneiro, would that be easy to fix?

view this post on Zulip Mario Carneiro (May 29 2019 at 17:27):

It would basically need to apply additive to turn it into a multiplicative problem

view this post on Zulip Patrick Massot (May 29 2019 at 17:34):

Is it something you may do in the near future?

view this post on Zulip Mario Carneiro (May 29 2019 at 17:35):

not today. I'll look into it

view this post on Zulip Patrick Massot (May 29 2019 at 17:38):

Thanks!

view this post on Zulip Amelia Livingston (Nov 21 2019 at 20:30):

How would applying additive in a proof work in practice? I tried to do this a few months ago (so can't really remember how it went) but the only way I could get to work reliably in a use case where I wanted to be in tactic mode was to add the lemma

lemma to_add {α} [has_mul α] :
  @has_mul.mul α _ = @has_add.add (additive α) _ := rfl

and rw to_add as needed, which I liked because it wasn't too many extra characters, but is there a proper way?

view this post on Zulip Mario Carneiro (Nov 21 2019 at 21:44):

The intended use is to write out the desired statement directly, and apply the corresponding multiplicative theorem and have defeq work out the differences. algebra.group_power has a few examples with multiplicative

view this post on Zulip Amelia Livingston (Dec 08 2019 at 03:51):

(deleted, I found something that works)

view this post on Zulip Bryan Gin-ge Chen (Mar 07 2021 at 21:10):

I'd like to use abel for inf and sup in (semi)lattices. I'm envisioning using it to reorder / reassociate terms in e.g. a calc block before doing more rewriting. How hard would it be to generalize abel to this use case? I'm thinking of doing this in two steps: first set up some wrapper(s) like additive and then try to figure out if abel can be generalized to additive semigroups (since semilattices may not have top or bot).

For the first step, am I right that we can't reuse additive directly since all the instances are already set up to go to / from has_mul? Is there some more generic approach?

view this post on Zulip Eric Wieser (Mar 07 2021 at 21:11):

src#additive.has_add is implemented in terms of has_mul, so yes, you'd can't reuse that one and would need a new one

view this post on Zulip Bryan Gin-ge Chen (Mar 07 2021 at 21:13):

Hmm, maybe I should wait for #6045 to be merged before attempting this...

view this post on Zulip Alex J. Best (Mar 07 2021 at 21:20):

Are any of the comments in https://leanprover.zulipchat.com/#narrow/stream/263328-triage/topic/random.20issue.3A.20.232726/near/215139106 about #2726 helpful?

view this post on Zulip Bryan Gin-ge Chen (Mar 07 2021 at 21:28):

Yeah, that looks like what I had in mind! I think I should be able to set things up so I can write change statements like the examples you posted, but then abel requires add_comm_monoid which I might not have.


Last updated: May 06 2021 at 17:38 UTC