dsimp before rw

Stream: mathlib4

[Winston Yin]

I've noticed that it is often necessary to write dsimp only before rw could work. See this PR but it's also been happening in other places. Should we do something about this?

[Eric Wieser]

Do you mean "it's necessary in lean4 where it wasn't in lean3"?

[Eric Wieser]

(· • ·) a looks suspicious there; I think the lean 3 version is (•) a, and that isn't a faithful port

[Mario Carneiro]

I've been meaning to fix mathport to translate that idiom to (a • ·) instead, although that's still not faithful

[Eric Wieser]

(the previous thread about this)

[Eric Wieser]

Can't we just do the literal translation?

[Mario Carneiro]

what, HasSMul.smul a? That's a clear pessimization

[Mario Carneiro]

Mathport's first priority is to make code that looks natural, even over code that works. If we wanted something that works but is ugly we would use binport instead or pp.all

[Mario Carneiro]

which is why I would like to fix this in core so that the natural thing also works, and mathport's optimistic translation doesn't have to change

[Eric Wieser]

Unless the fix to core comes soon, it would likely be easiest to do the literal translation and then do a cleanup pass over ported code once it lands

[Eric Wieser]

Otherwise pessimization is happening to ported proofs

[Mario Carneiro]

The majority of the time stuff like (· • ·) works just fine: inside definitions, proofs, and simp arguments. If you run into a case where it doesn't work (I've been waiting to get an MWE for this, so far it's only been a theoretical concern) then you have the option of fixing the proof or using HasSMul.smul a or anything else. All such options would need to come with a porting note anyway because they are all pessimizations, so I would like a human to do this.

[Mario Carneiro]

But mathport should be using the most optimistic setting rather than assuming it's never going to work and pessimizing the 99% because of the 1% of the time that it doesn't work

[Mario Carneiro]

Finally, the "literal translation" isn't literal at all. What is literally in the source is (•), and that's what synport sees and tries to reproduce. It only has a vague idea of what this expands to and who knows what namespaces are open so the identifier resolution needed to write HasSMul.smul correctly is a lot more fraught.

[Mario Carneiro]

a much more reliable way to get mathport to produce that identifier would be to write it out in mathlib3

[Kevin Buzzard]

Yeah, so in the linked PR (just for those who are catching up, like me) the issue is that in Lean 3 #check ((*)a) b gives a * b but in Lean 4 #check (a * ·) b gives (fun x ↦ a * x) b, so dsimp is occasionally necessary before a rewrite.

[Kevin Buzzard]

This issue has also shown up here. Is there no way of constructing some f from * and a such that f b is syntactically a * b in Lean 4, a la ((*)a) in Lean 3?

[Eric Wieser]

Yes, it's HMul.mul a

[Eric Wieser]

But you can't use the * notation, which is Mario's objection to using that spelling

[Kevin Buzzard]

I guess HMul.mul a is pretty ugly; however ((*)a) is actually incomprehensible as well I guess, it's just that we're more used to it.

[Eric Wieser]

The argument for (*) a in mathlib3 instead of λ x, a * x is precisely that it avoids the need for the dsimps mentioned in this thread; it's not about concision

[Eric Wieser]

This is particularly noticable when using apply mul_right_injective in a proof, which needs a dsimp afterwards if the second spelling is used to state docs#mul_right_injective.

[Eric Wieser]

Note that even the docs use the has_mul.mul spelling, so my opinion is that we should use the same spelling in mathlib4 rather than trying to clean things up during the port.

[Mario Carneiro]

I think someone should just open an issue so we can stop discussing workarounds