addressing lean4#2220 (HPow elaboration)

Stream: mathlib4

[Kyle Miller]

#6852 is an experiment for addressing this lean4#2220 issue, in a bid to remove all these local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) fixes

It has a modification of the core elaborator for arithmetic operations. The short of it is that in x ^ y it'll use x for its type information when computing coercions, and it won't try to force y to have the same type. It's also got the mirror image of this logic for x • y, where it'll use y and ignore x.

[Kyle Miller]

An example:

variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)

#check m + r • n

Elaborating + means it looks at both sides to find a common coercion. Elaborating r • n means it looks only at n to find a common coercion. So we have m : M and n : N, and these both coerce to M. Hence, this elaborates as m + r • ↑n : M. Before, it would have elaborated as m + ↑(r • n) : M since SMul didn't participate in the protocol.

[Kyle Miller]

It'd be nice to get some eyes on the changes in #6852 to see if these are acceptable modifications. I generally referred back to mathlib3 to make sure the coercions ended up in the right places. I didn't remove all the local macro_rules, but I tried to do enough to understand the impact of the changes to the elaborator.

If we like how it looks, then I could start working on contributing the elaborator changes back to Lean 4.

[Notification Bot]

3 messages were moved here from #mathlib4 > syntax for powers? by Kyle Miller.

[Floris van Doorn]

This is very nice! The logic is probably also useful for the less commonly used docs#VAdd / +ᵥ.

[Kyle Miller]

In case you don't follow the #lean4 stream (link), there is now an RFC lean4#2854 and a PR lean4#2778 for fixing this lean4#2220 issue. There's a mathlib PR #8284 that removes all these local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) and adjusts things to elaborate correctly.

[Kyle Miller]

Something I have done in #8284 is also change HSMul to use the new leftact% elaborator, which makes it participate in the algorithm that figures out where all the coercions go.

This is technically a new feature, and I don't want to push it through as if it's just part of a big bundle of fixes. I personally think it's nice and it integrates smul into how other operators elaborate, but if we think it's not ready for mathlib this can be split into a separate PR. (There's still time to review this change to smul within this PR though, as lean#2854 hasn't been accepted yet. Pinging @Yury G. Kudryashov and @Eric Wieser whom I remember having mentioned HSMul problems in the past.)

Some fixes I inserted switch a coercion arrow to (... :) notation to avoid some timeouts. I'm not sure yet, but I think it's related to issue lean4#2831. It shouldn't be an issue with using leftact% per se.

[Yaël Dillies]

What's the situation here? I've just tried updating LeanAPAP and Prereqs.LpNorm completely broke.

[Yaël Dillies]

Every time there is a real ^ real expression, I get

maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

[Yaël Dillies]

Nevermind! I see the fix that made it to core was badly interfering with the temporary fix that Kyle gave me several months ago! Deleting the latter makes everything work :partying_face: