int.coe_nat_inj

Stream: mathlib4

[Yaël Dillies]

docs3#int.coe_nat_inj was wrongfully aligned to Int.ofNat.inj. I know coe is supposed to be see-through now, but clearly it's not transparent enough:

import Mathlib.Init.Data.Int.Basic

example (m n : ℕ) : (↑(m - n) : ℤ) = m - n := by
  rw [Int.ofNat_sub]
  sorry

example (m n : ℕ) : Int.ofNat (m - n) = m - n := by
  rw [Int.ofNat_sub]
  sorry
/-
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ↑(?m.419 - ?m.418)
mn: ℕ
⊢ Int.ofNat (m - n) = ↑m - ↑n
-/

[Eric Wieser]

I think the problem is that those are not the same coe

[Eric Wieser]

The first one is OfNat.ofNat

[Eric Wieser]

By making coe's see-through, lemmas about coe now have to match syntactically rather than just by defeq

[Yaël Dillies]

So we should burn any use of Int.ofNat? The port hasn't done so at all, removing lemmas about coe in favor of Int.ofNat lemmas.

[Mario Carneiro]

not for lemmas with ofNat in the name...

[Yaël Dillies]

Sure. Replace "use" by "mathlib use" in my previous message.

[Mario Carneiro]

I think this is a remnant of the ad hoc port

[Mario Carneiro]

originally ofNat was the coercion

[Eric Wieser]

Yeah, that file has no porting header

[Yaël Dillies]

Mario Carneiro said:

not for lemmas with ofNat in the name...

Lemmas with ofNat in their name are usually about OfNat.ofNat, not Int.ofNat.

[Mario Carneiro]

*lemmas in the Int namespace with ofNat in the name

[Yaël Dillies]

I maintain:

Lemmas in the Int namespace with ofNat in their name are usually about OfNat.ofNat, not Int.ofNat.

[Yaël Dillies]

I agree it's bad, but that's how it is right now.

[Mario Carneiro]

this is empirically false, can you give an example?

[Yaël Dillies]

Most things that are aligned in Data.Int.Basic, eg docs#Int.ofNat_sub