LeftInverse does not recognize functions

Stream: new members

[Yunong Shi]

I am trying to write some simple ancillary functions for Matrix type conversion between Matrix (Fin i × Fin j) (Fin m × Fin n) α and Matrix (Fin (i * j)) (Fin (m * n)) α. I want to show that my two conversion functions are LeftInverse, as defined in Mathlib.Logic.Equiv.Fin. However, the term LeftInverse matrix_fin_flat_map_inv matrix_fin_flat_map gives an error:

function expected at
  LeftInverse
term has type
  ?m.705

I know that the two arguments are functions. What is the problem?

Here is my code (the error happens at the return type declaration of the last function matrix_fin_flat_map_left_inv):

import Mathlib.Data.Matrix.Basic
import Mathlib.Logic.Equiv.Fin
import Mathlib.Data.Nat.Basic

def matrix_fin_flat_map {i j m n: Nat} {α : Type v} (M: Matrix (Fin i × Fin j) (Fin m × Fin n) α): Matrix (Fin (i * j)) (Fin (m * n)) α :=
  Matrix.of fun (x: Fin (i * j)) (y: Fin (m * n)) =>  M (finProdFinEquiv.invFun x) (finProdFinEquiv.invFun y)

def matrix_fin_flat_map_inv {i j m n: Nat} {α : Type v}  (M: Matrix (Fin (i * j)) (Fin (m * n)) α): Matrix (Fin i × Fin j) (Fin m × Fin n) α :=
  Matrix.of fun (x: Fin i × Fin j) (y: Fin m × Fin n) =>  M (finProdFinEquiv.toFun x) (finProdFinEquiv.toFun y)

def matrix_fin_flat_map_left_inv: LeftInverse matrix_fin_flat_map_inv matrix_fin_flat_map := fun M => by
      apply Matrix.ext
      intro x y
      simp [matrix_fin_flat_map, matrix_fin_flat_map_inv, finProdFinEquiv.left_inv]
      simp [finProdFinEquiv]
      simp [Fin.divNat]
      simp only [Fin.modNat, Fin.mk_eq_mk]
      simp [add_comm]
      congr 2
      all_goals congr
      all_goals try rw [Nat.add_mul_div_left]
      rw [Nat.div_eq_of_lt, Nat.zero_add]
      apply x.2.2
      have H : 0 < j := Nat.pos_of_ne_zero  fun H => Nat.not_lt_zero x.2.1 <| H ▸ x.2.2
      exact H
      all_goals try apply Nat.mod_eq_of_lt
      apply x.2.2
      rw [add_left_eq_self]
      rw [Nat.div_eq_of_lt]
      all_goals try apply y.2.2
      have H2 : 0 < n := Nat.pos_of_ne_zero  fun H2 => Nat.not_lt_zero y.2.1 <| H2 ▸ y.2.2
      exact H2

[Eric Wieser]

You presumably want docs#Function.LeftInverse ?

[Eric Wieser]

Lean doesn't know that you mean to look in the Function namespace

[Eric Wieser]

Probably you actually want docs#Matrix.reindex though

[Yunong Shi]

Eric Wieser said:

You presumably want docs#Function.LeftInverse ?

Yeah, I actually used docs#Function.LeftInverse. I thought I used the one in Mathlib.Logic.Equiv.Fin. #Matrix.reindex makes a ton of sense! Thanks!

But what about the error here? Why is LeftInverse complaining...

[Ruben Van de Velde]

Do you need open Function?

[Yunong Shi]

Ruben Van de Velde said:

Do you need open Function?

I didn't, and Lean can understand LeftInverse.

[Winston Yin (尹維晨)]

Just add open Function and see if problem persists. My guess is, autoimplicit has declared LeftInverse to be some random type, since Lean doesn’t recognise it.

[Yunong Shi]

Winston Yin (尹維晨) said:

Just add open Function and see if problem persists. My guess is, autoimplicit has declared LeftInverse to be some random type, since Lean doesn’t recognise it.

Worked (turned to another error)! Thanks!

[Eric Wieser]

set_option autoImplicit false will make Lean actually tell you when this type of mistake happens