duplicate lemma : nat_ne_top

Stream: general

[Jireh Loreaux]

It seems that ennreal.nat_ne_top and ennreal.coe_nat_ne_top are duplicates. I am planning on deleting the latter (because the former is shorter and we also have ennreal.top_ne_nat but no ennreal.top_ne_coe_nat), unless someone objects that coe should be in the name.

[Wrenna Robson]

We do have rather a few coe_nat lemmas here, and that's what I would have expected to call it.

[Wrenna Robson]

They are also not precisely the same - coe_nat is not a simp lemma and has n implicit, and nat_ne has it as a simp lemma and nat explicit. Which one do you plan to use?

[Eric Wieser]

At some point we probably ought to standardize on coe_nat vs nat_cast

[Eric Wieser]

especially since now lemmas like docs#int.coe_nat_one are defeq to docs#nat.cast_one

[Yaël Dillies]

The coe_nat naming convention was just for coe : ℕ → ℤ, right?

[Jireh Loreaux]

Sorry, perhaps I should have been clearer that they aren't quite exactly the same. A quick grep suggests that nat_ne_top is used 12 times (explicitly) but coe_nat_ne_top is used 8 times. Of course, who knows how many times the former is used inside simp. So, I would keep nat_ne_top as is, delete coe_nat_ne_top, and replace uses of the latter with the former. Reasoning:

1. The name doesn't need coe because it's clear from context (we're in ennreal namespace after all), and this does parallel some lemmas elsewhere in the file.
2. When used as a rewrite lemma, if the explicit argument can be inferred, then it will be. If you need to provide the argument, you can do so without @.

[Wrenna Robson]

Yeah, I see the logic of that. Are you going to rename the other coe_nat lemmas in ennreal?

[Jireh Loreaux]

If that's the consensus, I guess we could, but it should probably be a separate PR. Right now I'm just trying to deduplicate.

[Wrenna Robson]

Oh for sure.