NatCast

Stream: std4

[Joe Hendrix]

How can I find out more about the purpose of NatCast and it's helper function Nat.cast?

I noticed a simp rule in Std.Data.Int.Lemmas rewrites Int.ofNat to Nat.cast, so it seems like it's considered an important canonical representation (for a ring solver?). However, the documentation only references AddMonoidWithOne which isn't defined in std.

[Yury G. Kudryashov]

It's in Mathlib.

[Yury G. Kudryashov]

In Mathlib, we want to have a canonical function for the cast from Nat to a (semi)ring (or, more generally, an additive monoid with one).

[Yury G. Kudryashov]

So, we define NatCast typeclass and use it.

[Yury G. Kudryashov]

Not sure how much was (or going to be) moved to Std.

[François G. Dorais]

It might look like Int and Rat are the only potential use cases in Std but there's a bit more use cases behind the scenes. It's too early to tell but I predict a small amount of this will make its way into Std, probably in a backgroundish manner though.

[Joe Hendrix]

Yeah, I see both it and IntCast are very common in Mathlib. BitVec also could use it potentially.

I have pretty mixed feelings about the cast operations. The Nat coercion in Mathlib 3 was one of the blockers for using Mathlib3 in my projects with Lean 3, but this design seems to avoid the specific issues with that design. Using it means better compatibility with Mathlib, and I don't object to having this coercion as long as syntax is required.

I think my main concrete concern is that it means importing Std introduces the coercion Nat -> Int and simp rule for rewriting Int.ofNat. That seems unexpected given those types are purely in Lean core. For me, it lead to a bunch of proofs breaking when I upgraded an old project to the latest Lean and Std. It might be worth either considering this is important enough to put in Lean core or reconsider whether it really belongs in Std.

[Mario Carneiro]

I did not originally want to have this class in std, but it is important for compatibility with mathlib to only have one canonical representation for the function and after discussion we ended up with Nat.cast existing but not being any more than a notation typeclass as far as Std is concerned. (It is a notation typeclass, it enables the up arrow syntax.)

[Mario Carneiro]

Originally std would have these lemmas directly about Int.ofNat but the problem was that they did not interoperate well with mathlib lemmas and the simp set. If it is introducing issues relative to Init, we may need to push this class up to core. Do you have some concrete examples of problems / regressions you have observed?

[Mario Carneiro]

@Joe Hendrix

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Int.2EofNat.20and.20Nat.2ECast/near/314947732

[Mario Carneiro]

That seems unexpected given those types are purely in Lean core.

By the way, on this point, std does quite a lot with definitions from Init, in particular adding many lemmas. I think of definitions like Nat, String, List as morally part of std but a large part of the lemma-free fragment of their API is provided in core because of bootstrapping issues. If we ever get to a properly bootstrapped std then it would be in the same library.

[Joe Hendrix]

Thanks for the link to the discussion. The only issue I ran into tried upgrading a library that provided a tactic similar to zify had a lot of Int theorems using Int.ofNat. I think that's a one time cost though and the conflicts would have been unavoidable due to Std getting all these lemmas. I do still have some issues, but that's largely due to differences in rewrite rule orientations.

I think ideally packages will just use Std and so always see these theorems. If core starts needing Int lemmas then this should be made upstream to core.

[Eric Wieser]

Note that there was an idea floating around in mathlib to eliminate Nat.cast and Int.cast in favor of a single Algebra.cast; we even started that refactor in lean3, but it got reverted during the port

[Eric Wieser]

The idea is to avoid having both algebraMap Nat Int n and (Nat.cast n : Int) as spellings, because every time you have two spellings of the same thing and fail to declare one canonical, you double the number of lemmas you need