Int.ofNat and Nat.Cast

Stream: mathlib4

[Chris Hughes]

There are problems in the port of Data.Int.Order.Basic caused by a clash between Nat.Cast and Int.ofNat, both are coercions Int to Nat. In Lean3 I think we made the decision to always use Nat.Castin Lean3, I guess we're making the same decision in Lean4? I'm not up to date with all of this.

[Eric Wieser]

In Lean3 we didn't need to make the decision, we just used coe as the head symbol of the simp-normal form

[Chris Hughes]

Which one is coe?

[Chris Hughes]

Both are coercions in Lean4

[Eric Wieser]

It doesn't matter in Lean 3, typeclass search can unify them because the typeclass instances are defeq. simp matches the head symbol and concludes it's worth a try

[Eric Wieser]

I would guess in the long term we maybe want to use an algebra.coe symbol for all of Nat.cast, Int.cast, algebraMap, subgroup.subtype, ...

[Eric Wieser]

Which is essentially the refactor that @Anne Baanen was trying to make in Lean 3

[Chris Hughes]

The two coercions are not defeq Int.ofNat is a constructor of Int and Nat.Cast is defined by induction on Nat

[Eric Wieser]

That's not true in Lean 3

[Eric Wieser]

docs4#Nat.Cast

[Eric Wieser]

Here they're made defeq: https://github.com/leanprover-community/mathlib/blob/42343ce564ba64b4dc636953c5a1882c95523680/src/data/int/basic.lean#L49

[Chris Hughes]

I forgot about that.

[Chris Hughes]

So the correct thing to do is just make sure Int.ofNat is not a coercion in Lean4

[Mario Carneiro]

That's not an option though, because it's in core (made into a @[coe] in Std) and I don't see Nat.cast making it to Std without a big refactor

[Mario Carneiro]

That would regress the behavior of lean-without-mathlib way too much

[Eric Wieser]

We can add a simp lemma that sends ofNat to Nat.cast, and maybe set the Nat.cast priority higher?

[Mario Carneiro]

you should just not use theorems about ofNat after Nat.cast is defined

[Mario Carneiro]

and that

[Mario Carneiro]

I thought the simp lemma already existed

[Mario Carneiro]

and it does have higher priority

[Mario Carneiro]

(well, it's probably the same priority but it is defined later)

[Eric Wieser]

I suspect the simp lemma causes loops in Lean3, since the RHS unifies with the LHS after matching explicit arguments; but maybe that's not how it works.

[Mario Carneiro]

well the setup work for the casts is mostly new code anyway

[Mario Carneiro]

import Mathlib.Data.Int.Basic

example : Int.ofNat x = Nat.cast x := by simp?
-- Try this: simp only [Int.ofNat_eq_cast]

[Chris Hughes]

I'd still rather not use the coe notation here. It's very confusing when a rw doesn't work because it's the wrong ↑. Both are printed with an ↑

[Gabriel Ebner]

I think the best course of action would be to remove the @[coe] attribute from Rat.ofInt and Int.ofNat in std4. It's hard to do anything about core, but std4's mission is to be unopinionated and leave decisions to libraries downstream. And if std4's decisions conflict with mathlib, then they clearly aren't unopinionated.

[Gabriel Ebner]

That's not an option though, because it's in core (made into a @[coe] in Std) and I don't see Nat.cast making it to Std without a big refactor

NB: all that's necessary is to move the NatCast/IntCast classes to std4. That should be a fairly small change (small enough that I don't see any technical reasons it couldn't be in core even).

[Mario Carneiro]

Hm, that's a good point. I will see whether we can move NatCast to std and give it an Int.ofNat instance, would that still cause a conflict?

[Mario Carneiro]

the existing Coe Nat Int instance in core should be mostly harmless once it is overridden in std

[Mario Carneiro]

std4#63

[Scott Morrison]

Are you planning on testing this with mathlib4, or would you like someone else to do that?

[Mario Carneiro]

I can do it if no one gets to it in the next few hours

[Scott Morrison]

mathlib4#972 tests that std4#63 works.

[Scott Morrison]

I think the port of Data.Int.Order.Basic, mathlib4#938, could merge that into it and proceed, if someone wants to do that.

[Scott Morrison]

@Mario Carneiro, std4#63 will need main merged into it before I can properly fix mathlib4#972. I've merged main into std4#63 as std4#66.

[Mario Carneiro]

I'm inclined to keep the name ofNat in the lemmas for the time being, because these still aren't the correct Nat.cast lemmas, and they certainly aren't about Int.cast