Zulip Chat Archive

Stream: mathlib4

Topic: Int.ofNat and Nat.Cast


Chris Hughes (Dec 09 2022 at 17:47):

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 (Dec 09 2022 at 17:49):

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 (Dec 09 2022 at 17:50):

Which one is coe?

Chris Hughes (Dec 09 2022 at 17:50):

Both are coercions in Lean4

Eric Wieser (Dec 09 2022 at 17:50):

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 (Dec 09 2022 at 17:51):

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 (Dec 09 2022 at 17:51):

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

Chris Hughes (Dec 09 2022 at 17:54):

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

Eric Wieser (Dec 09 2022 at 18:04):

That's not true in Lean 3

Eric Wieser (Dec 09 2022 at 18:05):

docs4#Nat.Cast

Eric Wieser (Dec 09 2022 at 18:05):

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

Chris Hughes (Dec 09 2022 at 18:38):

I forgot about that.

Chris Hughes (Dec 09 2022 at 18:40):

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

Mario Carneiro (Dec 09 2022 at 18:45):

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 (Dec 09 2022 at 18:46):

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

Eric Wieser (Dec 09 2022 at 18:46):

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

Mario Carneiro (Dec 09 2022 at 18:46):

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

Mario Carneiro (Dec 09 2022 at 18:46):

and that

Mario Carneiro (Dec 09 2022 at 18:46):

I thought the simp lemma already existed

Mario Carneiro (Dec 09 2022 at 18:47):

and it does have higher priority

Mario Carneiro (Dec 09 2022 at 18:47):

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

Eric Wieser (Dec 09 2022 at 18:47):

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 (Dec 09 2022 at 18:48):

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

Mario Carneiro (Dec 09 2022 at 18:50):

import Mathlib.Data.Int.Basic

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

Chris Hughes (Dec 12 2022 at 12:02):

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 (Dec 12 2022 at 16:55):

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 (Dec 12 2022 at 16:58):

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 (Dec 13 2022 at 06:15):

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 (Dec 13 2022 at 06:17):

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

Mario Carneiro (Dec 13 2022 at 07:01):

std4#63

Scott Morrison (Dec 13 2022 at 07:39):

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

Mario Carneiro (Dec 13 2022 at 08:21):

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

Scott Morrison (Dec 13 2022 at 09:59):

mathlib4#972 tests that std4#63 works.

Scott Morrison (Dec 13 2022 at 10:00):

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 (Dec 13 2022 at 11:23):

@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 (Dec 13 2022 at 11:43):

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


Last updated: Dec 20 2023 at 11:08 UTC