Matrix operations

Stream: new members

[li sheng]

I am new to lean .Who can tell me an example , in which we input two matrices and multiply them using standard library as in python ? A=Matrix([[1,2],[3,4]]),B=Matrix ([[1,1],[0,0]]),A*B=? in lean .Thanks !

[li sheng]

Is there anyone who will give me an example of matrix multiplication ? Input two specific matrices and multiply them. Thanks!

[Eric Wieser]

docs#matrix.mul

[Eric Wieser]

Aka M ⬝ N

[li sheng]

Is there anyone who will give me an example of matrix multiplication ? Input two specific matrices and multiply them. Thanks!

[Eric Wieser]

If you're brand new to lean that might not help all that much - if so, can you elaborate on your question a little?

[Eric Wieser]

Oh i see there's a copy of this thread in #new members - can an admin move this one?

[Notification Bot]

This topic was moved here from #general > Matrix operations by Bryan Gin-ge Chen

[Anne Baanen]

The matrix library is not optimized for these purposes, but you can do a bit of computing with them:

import data.matrix.notation
open_locale matrix

-- There's no `repr` defined for matrices, so the following line outputs a big pile of unreadable syntax.
-- #eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) : matrix _ _ ℤ)

#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) 0 0 : ℤ) -- -3
#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) 0 1 : ℤ) -- 5
#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) 1 0 : ℤ) -- -5
#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) 1 1 : ℤ) -- 7

[Anne Baanen]

You can fix the "no has_repr" issue as follows:

import data.matrix.notation
open_locale matrix

instance [has_repr α] : has_repr (fin n → α) :=
{ repr := λ f, "![" ++ (string.intercalate ", " ((list.fin_range n).map (λ n, repr (f n)))) ++ "]" }

instance [has_repr α] : has_repr (matrix (fin m) (fin n) α) :=
(infer_instance : has_repr (fin m → fin n → α))

#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) : matrix _ _ ℤ) -- ![![-3, 5], ![-5, 7]]

#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) 0 0 : ℤ) -- -3
#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) 0 1 : ℤ) -- 5
#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) 1 0 : ℤ) -- -5
#eval ((![![1, 2], ![3, 4]] ⬝ ![![1, -3], ![-2, 4]]) 1 1 : ℤ) -- 7

[li sheng]

This looks ugly! I think there should have a better one in lean.

[Eric Wieser]

Can we add those has_repr to data/matrix/notation.lean?

[Anne Baanen]

li sheng said:

This looks ugly! I think there should have a better one in lean.

Feel free to implement your own if you think it's ugly! Just replace the (infer_instance : has_repr (fin m → fin n → α)) line with { repr := λ M, your_string_goes_here } and have fun :)

[Anne Baanen]

Eric Wieser said:

Can we add those has_repr to data/matrix/notation.lean?

Sure, I'll make a PR after dinner!

[Eric Wieser]

!![a, b; c, d] might be a slightly less ugly notation for matrices, inspired by Matlab. I don't know how hard it is to tell lean how to use that.

[li sheng]

@Anne Baanen Thank you for your solution,I will try it and find other solutions!

[Eric Wieser]

@li sheng, what specifically is it you find ugly?

[Eric Wieser]

What would you like to be able to write instead?

[li sheng]

I want to use docs#matrix.mul! !![1,2;3,4] looks nice !

[Johan Commelin]

The snippets above use matrix.mul already.

[li sheng]

docs#matrix.mul provides us with plenty of functions,we can "encapsulate" them for convenient computations.

[Yakov Pechersky]

The nice thing about the current matrix notation is that it supports 1, 2, 3,... dimensional "matrices".

[Yakov Pechersky]

Semicolons limit you to 2D

[Eric Wieser]

I suggested !! because it doesn't rule out the existing notation

[Anne Baanen]

Opened #7953.

[Patrick Massot]

li sheng said:

I am new to lean .Who can tell me an example , in which we input two matrices and multiply them using standard library as in python ? A=Matrix([[1,2],[3,4]]),B=Matrix ([[1,1],[0,0]]),A*B=? in lean .Thanks !

I'm afraid you'll be very disappointed by Lean if this is your first question. In an ideal world, a proof assistant would be able to do everything a computer algebra system such as Sage is doing and then add proofs on top of that. Unfortunately we are very far away from this. Up to now these are almost disjoint worlds. Use Sage for computations and Lean for proofs.

[Kevin Buzzard]

Yes -- Lean is not a good "computer" at the minute -- it is designed to prove theorems, not do computations.

[Eric Wieser]

Eric Wieser said:

!![a, b; c, d] might be a slightly less ugly notation for matrices, inspired by Matlab. I don't know how hard it is to tell lean how to use that.

I implemented !ₘ[1, 2; 3, 4] in #14665

[Eric Wieser]

This PR has now split into #14991 and #14992, which respectively add !![a, b; c, d] notation (without the type cast) and type casting as matrix.of ![![a, b], ![b, c]] (without the !! notation). I'll fix the conflicts in whichever one doesn't go in first.