Zulip Chat Archive

Stream: general

Topic: Vectors & matrices in Lean


view this post on Zulip Andrew Helwer (Mar 28 2020 at 22:02):

Can anyone point me to where & how vectors & matrices are defined in lean?

view this post on Zulip Simon Hudon (Mar 28 2020 at 22:04):

In mathlib data.matrix.basic

view this post on Zulip Andrew Helwer (Apr 07 2020 at 16:20):

Are there good examples anywhere for the basics of how to use & manipulate this definition?

view this post on Zulip Johan Commelin (Apr 07 2020 at 16:22):

No I'm afraid... we don't have much linalg in terms of matrices...

view this post on Zulip Johan Commelin (Apr 07 2020 at 16:22):

So your best bet is to read that file (and PR some docs if you want/can!)

view this post on Zulip Johan Commelin (Apr 07 2020 at 16:23):

Also, you can search for data.matrix.basic to see which files import the definition of matrix

view this post on Zulip Patrick Massot (Apr 07 2020 at 16:25):

Or else you can have a look at the output of leanproject import-graph --from data.matrix.basic matrix.pdf

view this post on Zulip Patrick Massot (Apr 07 2020 at 16:26):

The fact that ring_theory.algebra import matrices is a bit misleading...

view this post on Zulip Bryan Gin-ge Chen (Apr 07 2020 at 16:29):

I suppose one could fire up leancrawler and look for declarations that actually rely on the matrix definition...

view this post on Zulip Patrick Massot (Apr 07 2020 at 16:30):

True.

view this post on Zulip Patrick Massot (Apr 07 2020 at 16:30):

Merging leanproject, format_lean and leancrawler is still on my TODO list...

view this post on Zulip Ryan Lahfa (Apr 07 2020 at 16:59):

Patrick Massot said:

Merging leanproject, format_lean and leancrawler is still on my TODO list...

Wow, leancrawler looks amazing

view this post on Zulip Patrick Massot (Apr 07 2020 at 16:59):

This is what produced the big graph at https://leanprover-community.github.io/lean-perfectoid-spaces/

view this post on Zulip Ryan Lahfa (Apr 07 2020 at 17:03):

I really liked this graph and wondered if I could produce snapshots of those for arbitrary theorem in mathematics

view this post on Zulip Patrick Massot (Apr 07 2020 at 17:04):

This will be much easier when leancrawler will be part of leanproject. But this requires time, and I'm already spending way too much time on Lean tooling.

view this post on Zulip Ryan Lahfa (Apr 07 2020 at 17:05):

Patrick Massot said:

This will be much easier when leancrawler will be part of leanproject. But this requires time, and I'm already spending way too much time on Lean tooling.

I'm quite proficient in Python, is there a way to give a hand?

view this post on Zulip Patrick Massot (Apr 07 2020 at 17:08):

The current blocking stuff is on the Lean meta-programming side I'm afraid.

view this post on Zulip Ryan Lahfa (Apr 07 2020 at 17:12):

@Patrick Massot Well, I'm interested into looking at the C++ internals of Lean, but not now, I don't have enough confidence on such piece of software :)

view this post on Zulip Patrick Massot (Apr 07 2020 at 17:12):

This has nothing to do with C++.

view this post on Zulip Ryan Lahfa (Apr 07 2020 at 17:13):

Patrick Massot said:

This has nothing to do with C++.

You mean the meta-programming in Lean (e.g. tactics building, etc.) ?

view this post on Zulip Patrick Massot (Apr 07 2020 at 17:13):

Yes.

view this post on Zulip Ryan Lahfa (Apr 07 2020 at 17:15):

Patrick Massot said:

Yes.

Are there any docs beyond tactics writing (which I know I already asked you about it) on the general meta-programming language/engine? I have seen that Lean 4 has something which looks a bit what Rust has for macros and I'm used to these kinds of meta-programming stuff

view this post on Zulip Scott Morrison (Apr 07 2020 at 23:18):

@Ryan Lahfa , what have you read already? https://doi.org/10.1145/3110278 is a great start.

view this post on Zulip Ryan Lahfa (Apr 08 2020 at 09:45):

Scott Morrison said:

Ryan Lahfa , what have you read already? https://doi.org/10.1145/3110278 is a great start.

Nothing more than Lean reference manual https://leanprover.github.io/reference/lean_reference.pdf and the mathlib docs. Will bookmark this :) — thank you!

view this post on Zulip Sebastien Gouezel (Apr 11 2020 at 07:38):

I just tried leanproject import-graph (on my windows machine), and I get (from a powershell shell)

PS C:\Users\Sebastien\Desktop\mathlib> leanproject import-graph --from data.fintype.basic fintype.pdf
[WinError 2] "dot" not found in path.

and from a Cygwin shell

Sebastien@DESKTOP-51UASBS /cygdrive/c/Users/Sebastien/Desktop/mathlib
$ leanproject import-graph --from data.fintype.basic fintype.pdf
expected string or bytes-like object

view this post on Zulip Yury G. Kudryashov (Apr 11 2020 at 07:40):

It needs dot from graphviz to produce pdfs

view this post on Zulip Sebastien Gouezel (Apr 11 2020 at 07:42):

OK, let me install graphviz and report back. Thanks!

view this post on Zulip Yury G. Kudryashov (Apr 11 2020 at 07:44):

fintype-graph.pdf

view this post on Zulip Yury G. Kudryashov (Apr 11 2020 at 07:45):

Do you want to remove something from this graph?

view this post on Zulip Sebastien Gouezel (Apr 11 2020 at 07:51):

Works like a charm, thanks!

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 07:57):

I hope this graph clarifies whatever you were wondering about :-)

view this post on Zulip Sebastien Gouezel (Apr 11 2020 at 08:01):

With the right --from and the right --to, yes, the tool is extremely informative.


Last updated: May 12 2021 at 04:19 UTC