Lean4 and multidimensional arrays

Stream: lean4

[Miguel Raz Guzmán Macedo]

Lean4's type class resolution is great for numerical linear algebra because operations on heterogenous types, aka structured matrices, can benefit immensely from type class resolution by calling specific algorithms for specific combinations of type.
As an example, think about the difference of multiplying two matrices A, B where they are 1e6 x 1e6 dense Float matrices or sparse Float matrices.

What are the Lean4 plans with regards to numerical linear algebra? I wasn't able to find any examples of multidimensional arrays in the manual.

[Mario Carneiro]

You could represent multidimensional arrays as arrays of arrays?

[Miguel Raz Guzmán Macedo]

With C or Fortran element alignment?

[Mario Carneiro]

neither, I guess it would have a pointer indirection

[Miguel Raz Guzmán Macedo]

That can't be good.

[Mario Carneiro]

If you want to ensure a flat array, then use a big array and add operations to view it as a 2d array

[Miguel Raz Guzmán Macedo]

Yeah, that's what I'm thinking.

[Miguel Raz Guzmán Macedo]

How could I get Matlab-y syntax for access then? I want def (a : Array Nat) := #[1 , 2; 3, 4] to represent a 2x2 matrix s.t. a[1,1] = 4.

[Miguel Raz Guzmán Macedo]

Also, wow, how do you answer so fast @Mario Carneiro , do you have notifications on for every channel? :sweat_smile:

[Mario Carneiro]

I am everywhere

[Miguel Raz Guzmán Macedo]

Quick question for ya:
If I have

def a := #[1,2,3]

and I have a double function, can I just write

map double a

to get #[1, 4, 6]?

Is there a way I can avoid writing Array.map double a?

[Miguel Raz Guzmán Macedo]

Oh, I think

#[1,2,3].map square

does what I want.

[Mario Carneiro]

Well, I managed to find 2 or 3 other bugs in lean in the process, but I managed to get this to work:

import Lean
open Lean Macro

structure Array₂ (A : Type u) : Type u :=
  rows : Nat
  cols : Nat
  buf : Array A
  e : rows * cols = buf.size

def Array₂.get {A} (a : Array₂ A)
  (i : Fin a.rows) (j : Fin a.cols) : A :=
a.buf.get ⟨i * a.cols + j, sorry⟩

def List.toArray₂ {A} (cols : Nat) (l : List A) : Array₂ A :=
  let rows := l.length / cols
  let buf := (l.take (rows * cols)).toArray
  ⟨rows, cols, buf, sorry⟩

syntax "#[" sepBy(sepBy(term, ", "), "; ") "]" : term

macro_rules | `(#[ $[$elems,*];* ]) => do
  let rows := elems.size
  if rows = 1 then throwUnsupported
  let some a ← pure $ elems.get? 0 | throwUnsupported
  let cols := a.getElems.size
  let mut args := #[]
  for a in elems do
    let x := a.getElems
    unless x.size = cols do throwUnsupported
    args := args.append x
  `(List.toArray₂ $(quote cols) [ $args,* ])

macro arr:term "[" i:term "," j:term "]" : term =>
  `(Array₂.get $arr ⟨$i, by decide⟩ ⟨$j, by decide⟩)

#eval #[1, 2; 3, 4][1, 1]

[Miguel Raz Guzmán Macedo]

Awesome!