Type conversion by simp doesn't make sense

Stream: new members

[Vivek Rajesh Joshi]

This is a problem I have isolated from my code, where simp is converting a matrix into a natural number. I can't figure out what theorem it uses either, because simp? just says Try this : simp only . Why is this happening, and how do I fix it?

example (i j : Fin m) : (1 : Matrix (Fin m) (Fin m) Rat) i j = 1 ∨ (1 : Matrix (Fin m) (Fin m) Rat) i j = 0 := by
  simp

[Mauricio Collares]

Here, the goal after the simp is OfNat.ofNat 1 i j = 1 ∨ OfNat.ofNat 1 i j = 0. Note that OfNat.ofNat takes a nat and returns an object of the appropriate type. In other words, it is "equivalent" to the type ascription : Matrix (Fin m) (Fin m) Rat you provided. In VS Code, you can hover over the term in the infoview to see its type.

[Mauricio Collares]

The "ugly" version of OfNat.ofNat 1 in this case, with all the implicits, is (@OfNat.ofNat.{0} (Matrix.{0, 0, 0} (Fin m) (Fin m) Rat) (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)), the first argument being the output type.

[Kevin Buzzard]

in other words, simp is not doing what you're saying it does, 1 means "the matrix 1", i.e. the identity matrix.

[Ruben Van de Velde]

Yeah, but simp should not be introducing those explicit ofNat calls

[Mauricio Collares]

That's a good point. simp is turning the term (@OfNat.ofNat.{0} (Matrix.{0, 0, 0} (Fin m) (Fin m) Rat) 1 ...) into (@OfNat.ofNat.{0} (Matrix.{0, 0, 0} (Fin m) (Fin m) Rat) (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) ...) (where ... denotes equal terms in set_option pp.all true), so it is inserting an extra ofNat from Nat to Nat.

[Vivek Rajesh Joshi]

Okay, now I understand what OfNat.ofNat means. Thanks!

[Mauricio Collares]

Minimized:

def Matrix := Nat → Nat → Nat

instance one : OfNat Matrix (nat_lit 0) := ⟨fun i j => 0⟩

example : (0 : Matrix) 0 0 = 0 := by
  dsimp only
  -- unsolved goals
  -- ⊢ OfNat.ofNat 0 0 0 = 0

[Mauricio Collares]

Leo fixed this in lean4#4481