(Fin r -> A) -> r

Stream: Is there code for X?

[Vivek Rajesh Joshi]

Is there a function that takes a function defined on Fin r and returns r? Couldn't find it on Loogle

[Eric Wieser]

In almost every situation where you might want such a function, you can use r directly since it's already in your context

[Vivek Rajesh Joshi]

I need to get the row length of a Matrix (Fin r) (Fin s) Rat. I can't use s, because that's what I'm trying to prove: that the row length is equal to the number of columns

[Martin Dvořák]

What is the type of your term?

[Vivek Rajesh Joshi]

Could you please specify, what term?

[Martin Dvořák]

Vivek Rajesh Joshi said:

the row length is equal to the number of columns

This doesn't sound like a theorem.

[Martin Dvořák]

Vivek Rajesh Joshi said:

Could you please specify, what term?

You have a matrix of a certain type, right? Can you post a #mwe please?

[Vivek Rajesh Joshi]

Yeah, the type of my matrix is Matrix (Fin r) (Fin s) Rat

[Martin Dvořák]

So you want to prove that s = s. The proof is rfl. This smells like #xy.

[Vivek Rajesh Joshi]

I'm having some trouble formalising the statement itself, so I don't have much to show for my attempt so far. I'll show an example of what I'm trying to prove:

def mat := !![1,2,3;4,5,6;7,8,9]
#eval (List.ofFn (mat 1)).length == (List.ofFn mat.transpose).length

[Martin Dvořák]

You're having trouble to state it because you don't have a theorem to be stated.

[Vivek Rajesh Joshi]

I do, but I'm unable to state it for empty matrices. This is what I have:

import Mathlib.Data.Matrix.Notation

lemma rowLengthOfMatEqNumCol (M : Matrix (Fin r) (Fin s) Rat) :
  (List.ofFn (M 0)).length = s := by
  sorry

[Vivek Rajesh Joshi]

The 0 is problematic because r could be 0

[Kyle Miller]

Maybe use Fin (r + 1) instead, to make sure it's not zero?

[Martin Dvořák]

Or maybe you want to say the following?

example {m n : ℕ} (A : Matrix (Fin m) (Fin n) α) :
    ∀ i : Fin m, (List.ofFn (A i)).length = (List.ofFn A.transpose).length := by
  sorry

[Martin Dvořák]

This statement is an equivalent way to say it. It has a one-token proof:

example {m n : ℕ} (A : Matrix (Fin m) (Fin n) α) (i : Fin m) :
    (List.ofFn (A i)).length = (List.ofFn A.transpose).length := by
  simp

[Vivek Rajesh Joshi]

Kyle Miller said:

Maybe use Fin (r + 1) instead, to make sure it's not zero?

Yeah, and handle the empty case separately. I could try it.

[Vivek Rajesh Joshi]

Martin Dvořák said:

This statement is an equivalent way to say it. It has a one-token proof:

example {m n : ℕ} (A : Matrix (Fin m) (Fin n) α) (i : Fin m) :
    (List.ofFn (A i)).length = (List.ofFn A.transpose).length := by
  simp

Ohh nice. That should solve it, thanks!

[Martin Dvořák]

It doubt I gave you anything useful.

[Vivek Rajesh Joshi]

No, this actually answered my initial question too. Seems like simp just uses List.length_ofFn, which was what I asked for in the beginning.
I'm new to the whole formalisation process, and I realise this might not be the best way to implement what I want. But at least this gets me closer to what I want to finally implement, and I can worry about optimising it later.

[Martin Dvořák]

Is your use case that you want to prove a certain identity by arranging some data into a matrix in two different ways A and B where you prove A.transpose = B and then utilize something like the example above? If so, just by being able to state A.transpose = B you already know their sizes coïncide at compile time, so no need to prove anything that actually takes the matrices as an input.

[Martin Dvořák]

Another similarly vacuous example is the following:

import Mathlib.Data.Matrix.Notation

example {R C T : Type} [fC : Fintype C] (A : Matrix R C T) (i : R) :
    (fC.elems.val.map (A i)).toList.length = fC.elems.val.toList.length := by
  simp

Again, note that the only thing that matters is the instance [fC : Fintype C] which you already had. You can check that A is irrelevant by being able to state the very same thing without the matrix A at all:

import Mathlib.Data.Matrix.Notation

example {C T : Type} [fC : Fintype C] (A' : C → T) :
    (fC.elems.val.map A').toList.length = fC.elems.val.toList.length := by
  simp

[Vivek Rajesh Joshi]

There was a function in which I wanted to get the column corresponding to an element in a row, so I wanted to convert the type of the index of that element from Nat to Fin s where s is the number of columns, for which I had to prove that the index value is less than s. I interpret s as row length and proved so, but I later realised that in the function, s had the value of number of columns.
Looking back, there most likely is a much simpler way to do this. I'll see about it soon.
I think a part of the problem is that the function accepts 2 unrelated nested lists, which are supposed to be the list of rows and list of columns of the matrix.

[Martin Dvořák]

You have lists containing the indices of the matrix or lists containing the data of the matrix?

[Antoine Chambert-Loir]

Vivek Rajesh Joshi said:

The 0 is problematic because r could be 0

No it can't, because if you use M 0, you need to have 0 < r, hence r is not zero.
(Note that if r = 0, all the lines of M have length 1000.)

[Vivek Rajesh Joshi]

Martin Dvořák said:

You have lists containing the indices of the matrix or lists containing the data of the matrix?

They contain the data of the matrix

[Vivek Rajesh Joshi]

Antoine Chambert-Loir said:

Vivek Rajesh Joshi said:

The 0 is problematic because r could be 0

No it can't, because if you use M 0, you need to have 0 < r, hence r is not zero.
(Note that if r = 0, all the lines of M have length 1000.)

Doesn't the matrix !![] have type Matrix (Fin 0) (Fin 0) ?a?

[Antoine Chambert-Loir]

Yes, because !![]builds such a matrix and Lean is a typed language. My point was that mathematically you can't recognize between Matrix (Fin 0) (Fin 3145) and Matrix (Fin 2718) (Fin 0). One would represent the zero linear map $\mathbf R^{3145}\to 0$ and the other one the zero linear map $0 \to \mathbf R^{2718}$.