Trying to simplify using OfNat and NatCast

Stream: mathlib4

[Terence Tao]

I'm having a weird problem using simp to simplify casting to the natural numbers in a custom class. Here is a MWE:

import Mathlib

class MyNat where
  data : Type

instance {n:ℕ} : OfNat MyNat n where
  ofNat := sorry

instance : NatCast MyNat where
  natCast n := sorry

@[simp]
theorem MyNat.ofNat_eq_coe {n:ℕ} : OfNat.ofNat n = (n:MyNat) := sorry

@[simp]
theorem MyNat.ofNat_inj (n m:ℕ) : (n:MyNat) ≠ (m:MyNat) ↔ n ≠ m := by sorry

example : (5:MyNat) ≠ (3:MyNat) := by
  simp_rw [MyNat.ofNat_eq_coe, MyNat.ofNat_inj]
  norm_num

Here I have some custom class MyNat which is supposed to contain the natural numbers as a subset. Using an OfNatinstance, I can define (n:MyNat) for any numeral n, and using a NatCast instance, I can define (n:MyNat) for any n: ℕ. Assuming these casts are compatible and injective, I can then prove things like (5:MyNat) ≠ (3:MyNat) using simp_rw as indicated above. But for some reason, simp itself does not work.

It seems that the issue has to do with a subtle difference between say @OfNat.ofNat MyNat 5 instOfNatMyNat and @OfNat.ofNat MyNat 5 instOfNatAtLeastTwo; simp_rw tends to generate the former while simp generates the latter. If I try to introduce more simp lemmas to handle the former then I tend to generate infinite simp loops, e.g.,

import Mathlib

class MyNat where
  data : Type

instance {n:ℕ} : OfNat MyNat n where
  ofNat := sorry

instance : NatCast MyNat where
  natCast n := sorry

@[simp]
theorem MyNat.ofNat_eq_coe {n:ℕ} : OfNat.ofNat n = (n:MyNat) := sorry

@[simp]
theorem MyNat.ofNat_eq_coe' {n:ℕ} [n.AtLeastTwo] : @OfNat.ofNat MyNat n instOfNatAtLeastTwo  = (n:MyNat) := sorry

@[simp]
theorem MyNat.ofNat_inj (n m:ℕ) : (n:MyNat) ≠ (m:MyNat) ↔ n ≠ m := by sorry

example : (5:MyNat) ≠ (3:MyNat) := by
  simp [ne_eq] -- creates infinite loop

Is there an idiomatic way to support casting both numerals and Nat into a custom class in such a way that one can establish facts such as (5:MyNat) ≠ (3:MyNat) through simp (or norm_num)? For my application I don't expect to be able to make MyNat decidable enough that decide becomes an option.

[Eric Wieser]

I think the lemma you want to write is

@[simp]
theorem MyNat.ofNat_eq_coe {n:ℕ} : ((ofNat(n) : Nat) : MyNat) = ofNat(n) := sorry

[Eric Wieser]

In general, the rule is "if n appears in an ofNat() application somewhere, it should do so everywhere"

[Eric Wieser]

The other trap you're running into here is that if you populate these two instances with sorry, then they will always form a diamond

[Eric Wieser]

Fixing those issues, the infinite loop still persists though:

import Mathlib

class MyNat where
  data : Type

instance {n:ℕ} : OfNat MyNat n where
  ofNat := ⟨Fin n⟩

instance : NatCast MyNat where
  natCast n := ⟨Fin n⟩

@[simp]
theorem MyNat.ofNat_eq_coe {n:ℕ} : ofNat(n) = ((ofNat(n) : ℕ) : MyNat) := sorry

@[simp]
theorem MyNat.natCast_inj (n m:ℕ) : (n : MyNat) = (m : MyNat) ↔ n = m := by sorry

example : (5:MyNat) ≠ (3:MyNat) := by
  simp only [ne_eq] -- infinite loop, but the lemmas above alternate between introducing and removing casts!

[Eric Wieser]

This works though:

example : (5:MyNat) ≠ (3:MyNat) := by
  simp_rw [ne_eq, MyNat.ofNat_eq_coe, MyNat.natCast_inj]
  norm_num

[Terence Tao]

Yeah, for some reason simp_rw dodges all the issues. But then I have to specify all the lemmas and can't rely on the @[simp] tag, which is annoying.

[Eric Wieser]

This is the lemma you actually want:

@[simp]
theorem MyNat.ofNat_inj (n m:ℕ) :
    (ofNat(n) : MyNat) = (ofNat(m) : MyNat) ↔ ofNat(n) = ofNat(m) := by sorry

example : (5:MyNat) ≠ (3:MyNat) := by
  simp

[Eric Wieser]

The problem above is that MyNat.ofNat_eq_coe is a bad simp lemma, as it makes things more complex

[Terence Tao]

I based it off of docs#Int.ofNat_eq_coe which is a @[simp] lemma that seems to work just fine

[Eric Wieser]

That lemma is a trick, it is about docs#Int.ofNat (the constructor) not docs#OfNat.ofNat (the typeclass field)

[Terence Tao]

OK that explains why I got derailed

[Terence Tao]

Thanks!