Example Code of Matrix Rank

Stream: Is there code for X?

[Max Bobbin]

Is there an example code of proving a matrix's rank using matrix.rank? I was looking at the matrix.lean file in the test folder, but couldn't find anything.
This is an mwe of an example of what I am trying to do if that helps point me to an example.
Edit: Fixed mwe so it had imports

import data.matrix.rank
example : matrix.rank !![(1 : ℚ),0;0,1;1,-1] = 2 :=

[Heather Macbeth]

That's not a #mwe, you need imports.

[Max Bobbin]

Heather Macbeth said:

That's not a #mwe, you need imports.

Sorry, updated. Forgot about the imports

[Kevin Buzzard]

Lean is not a computer algebra package (yet); you could prove this by showing the rank was <= 2 and >= 2, but there's no tactic as far as I know which will do it for you.

[Max Bobbin]

Kevin Buzzard said:

Lean is not a computer algebra package (yet); you could prove this by showing the rank was <= 2 and >= 2, but there's no tactic as far as I know which will do it for you.

Good to know, thank you!

[Max Bobbin]

Kevin Buzzard said:

Lean is not a computer algebra package (yet); you could prove this by showing the rank was <= 2 and >= 2, but there's no tactic as far as I know which will do it for you.

What is needed to get Lean to a point where it can also operate like a computer algebra package? Is that something Lean 4 will be more adapt to?

[Scott Morrison]

Lean4 is not particularly better than Lean3 for things like this, except possibly that actually computing LU decompositions (row reductions) could be implemented faster.

[Scott Morrison]

I think the first tactic one would want here is something like lu_decomposition, which looks for a matrix in the goal, and replaces it with its LU decomposition. (And maybe asserts the relevant facts about the pieces of the decomposition.)

[Scott Morrison]

As far as I'm aware no one has done this, but it would be a great project. (Preferably at this point it should be done in Lean4 rather than in Lean3, so we don't have to port it, but this requires waiting a little.)

[Scott Morrison]

(I guess the other advantage of Lean4 here is that really this tactic should be implemented by calling out to some existing fast library for computing matrix decompositions, and this is much more viable from Lean4 than from Lean3.)

[Kevin Buzzard]

LU is another one of those things where the decomposition can be done without proofs and then the check that it's correct can be done formally

[Scott Morrison]

(Making it particularly suitable for calling out to existing optimised fast libraries!)

[Reid Barton]

The only problem with using an existing fast library is it then becomes embarrassing when the slowest part of the whole procedure is just turning an expr into a matrix of numbers or whatever

[Eric Wieser]

(For what it's worth, I have some code that does the convert-to-expr step here)

[Anne Baanen]

@Alex J. Best has been working on doing matrix operations like these in Sage and importing and verifying them in Lean (no LU decomposition yet, IIRC)

[Alex J. Best]

Yes I think we did RREF, but it should be only a small change to do LU instead