abel multiplication

Stream: maths

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

Is it something you may do in the near future?

[Mario Carneiro]

not today. I'll look into it

[Patrick Massot]

Thanks!

[Amelia Livingston]

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?

[Mario Carneiro]

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

[Amelia Livingston]

(deleted, I found something that works)

[Bryan Gin-ge Chen]

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?

[Eric Wieser]

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

[Bryan Gin-ge Chen]

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

[Alex J. Best]

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?

[Bryan Gin-ge Chen]

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.