to_additive issues

Stream: mathlib4

[Jireh Loreaux]

to_additive has been through the ringer recently. Let me throw another punch or two.

In Algebra.Group.Defs the to_additive attributes for HPow are wrong which leads to errors when converting from pow to smul where it complains about HMul.hMul. The first issue is to recognize that the argument reordering is wrong for HPow.hPow (it should be 1 5). However, that doesn't lead to a complete fix because Pow is really the heterogeneous HPow under the hood.

I came up with a fix: Define a heterogeneous scalar multiplication class HSmul with field hSmul, then make • notation for HSmul.hSmul and provide an instance instHSmul to mirror things like instHPow. Of course, we could do the same thing for Vadd if we wanted / needed, but I feel this is less pressing. Then all the translation seems to work.

This allows the successful(∗) fix of the note lower in this file:

-- FIXME The lemmas in this section should be done by `to_additive` below, but it fails.

What do we think of this? Should I implement it?

[Jireh Loreaux]

Regarding the (∗): it actually doesn't work for succ_nsmul, but for a different reason. With the above fix implemented, to_additive fails when trying to additivize pow_succ into succ_nsmul because it sees the 1 and incorrectly changes it into 0 (here it is incorrect because it occurs as n + 1, so it really represents n.succ). Note that to_additive in Lean 3 correctly additivizes this declaration.

This happens despite the fact that there is a note in the file about add_monoids that:

/- In the definition, we use `n.succ` instead of `n + 1` in the `nsmul_succ'` and `npow_succ'` fields
to make sure that `to_additive` is not confused (otherwise, it would try to convert `1 : ℕ`
to `0 : ℕ`). -/

Moreover, even though in Lean 4 we still use n.succ in the definition of AddMonoid I think to_additive still manages to see a 1 somehow and converts it into a 0 (this is based on trying to port Algebra.Group.InjSurj and noting that with the fix in the previous post, to_additive fails to additivize in certain situations for what I believe to be this reason).

[Yaël Dillies]

What is HPow used for?

[Jireh Loreaux]

Lean 4 core has all kinds of heterogeneous operations HMul, HAdd, HPow and the notations are actually defined on these type classes, not on Mul, Add, and Pow, but the latter have instances of the former, so they inherit the notation.

[Jireh Loreaux]

If you wanted, you could use it get it a pow functions ℕ → ℚ → ℝ (with junk values for negative powers). I'm not saying we should do this, only that it's possible.

[Yaël Dillies]

so HSMul is HMul, right?

[Jireh Loreaux]

Well, yes and no? They are essentially the same (i.e., structures with a single function α → β → γ), but their respective functions get different notation • vs. *.

[Jireh Loreaux]

So they are the same and / or different in precisely the same ways as HMul, HAdd and HPow.

[Jireh Loreaux]

Anyway, I need to go to bed. Hopefully while I sleep a few hours people can discuss this a bit.

[Jireh Loreaux]

Just to emphasize one point about why I think we need this type class HSmul: if we don't have it, what is the additivization of instHPow (which is necessary to have)?

[Floris van Doorn]

I'll take a look today. 1 : ℕ should not be transformed to 0 by to_additive for a long time already.

[Yaël Dillies]

I don't think instHPow makes sense in this generality

[Floris van Doorn]

Did we discuss that we don't want to use HMul for scalar multiplication? If we do, HMul could be the additive analogue of HPow.

[Floris van Doorn]

There are currently multiple issues with not translating multiplicative things on ℕ with additive things (both in the code and in the attributes that are set).
Since numerals are encoded differently in Lean 4, we need some logic around those.
@Mario Carneiro: if I look through a fully elaborated expression, will all natural number literals (Expr.lit) be inside an application of OfNat.ofNat?

[Jireh Loreaux]

Floris, I saw the branch to_additive_fixes. FYI: it still is translating 1 : ℕ to 0. See the offshoot branch j-loreaux/HSmul and look at the first error in Algebra.Group.Defs where it tries to additivize pow_succ.

[Jireh Loreaux]

Shouldn't we just create a new type class HSmul for the new notation? It seems better to keep things separate instead of merging them under the hood (i.e., I think it's a bad idea to implement both Smul and Mul in terms of HMul, especially because at some point in time we might want an actual heterogenous multiplication; that is, a heterogenous operation which gets the * notation).

[Jireh Loreaux]

Yaël, can you explain why you don't think instHPow makes sense? I don't see any issue with it yet.

[Floris van Doorn]

Still todo:

• deal with literals in Nat (see my question here)

[Jireh Loreaux]

Oh sorry, I misread.

[Floris van Doorn]

I'm fine with keeping mul and smul separate. And if we do, I agree we need an HSmul.

[Yaël Dillies]

I thought the entire point of HMul was to unify mul and smul?

[Yaël Dillies]

Do we have any use for HMul?

[Jireh Loreaux]

Why would we want to unify them? Unless we're trying to unify notation? Types are cheap.

[Kyle Miller]

There are two potential reasons to want to unify them. (1) Then we have a reasonable way to write left actions and right actions (I'd like to see bimodules properly handled notationally), (2) there is special elaborator support for HMul, though I don't really know the details (maybe we can use the binop% elaboration helper for an HSmul too? then this wouldn't be an advantage)

[Jireh Loreaux]

I don't see why this requires unification. We could accomplish this with an HSmul and it has the added benefit that we keep things separate. We can add the elaboration support if we want of course.

[Yaël Dillies]

But why would we want HSmul? This doesn't represent anything that HMul doesn't represent already.

[Jireh Loreaux]

I'm pushing this for two reasons: (1) I think it will be easier to plug in to to_additive, but perhaps more importantly (2) it safeguards against what I think could be very painful refactors down the road.

[Yaël Dillies]

HMul is to Mul what HMul is to SMul.

[Jireh Loreaux]

Disagree.

[Yaël Dillies]

So I don't think we want HPow at all.

[Jireh Loreaux]

Hmul is still for *, but heterogeneous.

[Kyle Miller]

So long as HSMul is fully generic in the two inputs and the output like HMul, I think I'm on board with it. It's a good way to indicate "this is an action of some sort", and I think it should work for both left and right actions.

(We might still have some HMul instances for certain kinds of actions, like for scalar multiplication on pi types, since that's more of a lift of the scalar using const. Is it a scalar action, or is it a coercion to the pi structure?)

[Kevin Buzzard]

Yaël Dillies said:

But why would we want HSmul? This doesn't represent anything that HMul doesn't represent already.

has_one doesn't represent anything that has_zero doesn't represent already but that's not an argument for removing has_one. We're talking about a notational typeclass here, right?

[Jireh Loreaux]

Yes

[Kyle Miller]

Another thing about mul and smul is that mul is generally associative but smul isn't (usually because of type reasons; but a group acting on itself by conjugation is a nonassociative action, for example).

[Sebastien Gouezel]

Any idea why the heterogeneous multiplication HMul was introduced in Lean 4?

[Kevin Buzzard]

I think Leo saw we were using smul and decided to see if it was worth generalising to mul?

[Kyle Miller]

The examples I've seen are generally scalar multiplication of vectors. When writing programs, it seems like it's also useful for multiplications where you could insert a coercion, but it might be more efficient to use the uncoerced type directly.

[Johan Commelin]

I think it's fair to say that Hmul (m : Nat) (n : Int) : Int is a very specific kind of smul. And also that there might be some sense in supporting it.

[Johan Commelin]

So I can imagine using Hmul for algebras.

[Johan Commelin]

But still keeping smul around for general actions.

[Scott Morrison]

Floris van Doorn said:

If I look through a fully elaborated expression, will all natural number literals (Expr.lit) be inside an application of OfNat.ofNat?

Yes.

[Frédéric Dupuis]

Sebastien Gouezel said:

Any idea why the heterogeneous multiplication HMul was introduced in Lean 4?

Matrix multiplication is one obvious place where it would be nice (and the one Leo gave when talking about this new feature).

[Jireh Loreaux]

Just for reference, I can even think now of a situation where I might want HAdd: in operator algebraic K-theory one constructs K_0 (almost) as the Grothendieck group of a semigroup of projections which lie in matrix algebras (of varying sizes) over the algebra in question. So one might want to add something in M_n(A) to something in M_k(A) and get something in M_{n+k}(A).

[Jireh Loreaux]

Point being, let's have the heterogeneous versions in general; there's little harm if they never get used.

[Yaël Dillies]

No but you corroborate my point here: We might want HMul and HAdd, but

1. they appear in situations similar to smul, so we might as well get rid of smul
2. Nobody can come up with an actual use case for HPow

[Jireh Loreaux]

No, I still disagree with this. My point about HAdd was this: in case you didn't know about operator algebraic K-theory, you might think that HAdd is not necessary (of course, you may have your own examples), but then I gave a counterexample. Look, mathlib has a rule about not overgeneralizing when there is some cost; however, when it's essentially free, and it's conceivable that it has a use, there's no reason not to generalize.

I believe HPow and HSmul fall into this category. In fact, I already gave a potential use for HPow, you've just ignored it: ℕ → ℚ → ℝ. Again, I'm not arguing that we want that particular HPow instance, only that we might.

Moreover, I think we should not make things overlap just because it's convenient. So smul should not use HMul under the hood, because the latter is the typeclass for *, not •.

[Scott Morrison]

The * vs \bu difference seems quite important. :-)

[Yaël Dillies]

I wouldn't call your example of possible use of HPow "actual" :big_smile:

[Yaël Dillies]

My point is not that we shouldn't generalise. My point is that generalising doesn't mean what you claim it does.

[Jireh Loreaux]

Look, I propose creating the HSMul class for now so that I can fix to_additive translating pow to smul without potentially clobbering HMul. If later we wish to change Lean 4 core to remove HPow and we can convince the devs, fine, we can do that when the time comes. Can I have thumbs up or thumbs down from people on this?

[Jireh Loreaux]

mathlib4#706

[Jireh Loreaux]

Sorry, I thought it built properly on my machine, but apparently not. I'll fix it shortly.

[Jireh Loreaux]

I have no idea why the abel test is failing on this PR. Help appreciated @Mario Carneiro (of course you're welcome to ignore this ping; it is Thanksgiving after all)

[Jireh Loreaux]

Okay, I think I have some idea. I think the issue is that the case matching on abel only handles SMul but now it needs to handle HSMul (in Mathlib.Tactic.Abel.eval). If someone wants to have a go at fixing it, be my guest, but it's bedtime for me.

[Jireh Loreaux]

This now has a :check: