Ergonomics: linarith does not work on Nat alias

Stream: lean4

[Siddharth Bhat]

Consider the MWE:

/-- Type of tensor dimensions and indexes into tensor dimensions. -/
abbrev Index := ℕ
theorem nat (a b : ℕ) (H : a < b) : a < 2 * b := by linarith
/-- linarith failed to find a contradiction -/
theorem index_check_fail (a b : Index) (H : a < b) : a < 2 * b := by { linarith; sorry }
theorem index_check (a b : Index) (H : a < b) : a < 2 * b := by simp[Index] at *; linarith

I would not call this a problem, as it is alleviated by defining a custom linarith_index (simoIndex and then applylinarith). Still, this took be aback when I encountered it.

I wonder if linarith is designed to smoothly incorporate such a use-case, and has a different solution builtin?

[Kevin Buzzard]

I don't think anything works on an alias -- that's the point of type aliases right? i.e. this is working as expected.

[Gabriel Ebner]

Usually, abbrev is transparent to most kinds of automation. Simp, type-class search, etc., will just see through it. I think it would make sense for linarith to see through it as well.

[Jireh Loreaux]

Was it implemented with a hardcoded Nat for performance reasons though?

[Kevin Buzzard]

Oh I see, if this was inlined then it really would work. I spoke too soon -- sorry.