Matrix from dependent type `Vec n α`

Stream: new members

[Curious Joe]

Hi all!

I am trying to construct a matrix based on a dependent type Vec n α.
The matrix has type Vec n (Vec m α) where n and m are decided at runtime.
I am trying to construct the matrix Vec n (Vec m α) from a List (List α)
where for simplicity I set α := Nat.
However, I am having trouble with this.
My code is the following:

abbrev Vec (n : Nat) (a : Type) := { ls : List a // ls.length = n }
abbrev Matrix (n m : Nat) (a : Type) := Vec n (Vec m a)

def test_mat (mat : List (List Nat)) :=
  let m := mat[0]!.length
  let d : List (Option (Vec m Nat)) := mat.map (fun row =>
    let row_length := row.length
    if h1 : row_length = m then
      pure ⟨row, h1⟩
    else
      none
    )
  let df := d.filterMap id
  let n := df.length
  let mat : Matrix n m Nat := ⟨df, by decide⟩
  mat

def output_testmat := test_mat [[1, 2, 3], [4, 5, 6], [7, 8, 9]]
#eval output_testmat

At the let mat line I get the following error:

▶ 15:39-15:45: error:
expected type must not contain free or meta variables
  (List.filterMap id
        (List.map (fun row => if h1 : row.length = mat[0]!.length then pure ⟨row, h1⟩ else none) mat)).length =
    (List.filterMap id
        (List.map (fun row => if h1 : row.length = mat[0]!.length then pure ⟨row, h1⟩ else none) mat)).length

Does anyone have any good tips on how to proceed with this?
I rather not use anything from mathlib and instead construct the type for
myself.

Many thanks!

[Henrik Böving]

You could use something along the lines of

def test_mat (mat : List (List Nat)) : (n : Nat) × (m : Nat) × (Matrix n m Nat)

So you return the dimensions of the matrix that you build along with the matrix itself.

[Curious Joe]

Thanks a lot! That makes sense.
However, I still get the same error at the mat line:

▶ expected type (45:3-46:14)
mat : List (List Nat)
m : Nat := mat[0]!.length
d : List (Option (Vec m Nat)) := List.map
  (fun row =>
    let row_length := row.length;
    if h1 : row_length = m then pure ⟨row, h1⟩ else none)
  mat
df : List (Vec m Nat) := List.filterMap id d
n : Nat := df.length
⊢ (n : Nat) × (m : Nat) × Matrix n m Nat

▶ 45:42-45:48: error:
expected type must not contain free or meta variables
  (List.filterMap id
        (List.map (fun row => if h1 : row.length = mat[0]!.length then pure ⟨row, h1⟩ else none) mat)).length =
    (List.filterMap id
        (List.map (fun row => if h1 : row.length = mat[0]!.length then pure ⟨row, h1⟩ else none) mat)).length

[Curious Joe]

Okay so I managed to construct a solution that is good enough for me although
it feels a bit hacky :D
I use a Monad transformer and a config where I hardcode the matrix dimensions
upfront.
The #eval output_testmat yields output:

▶ 34:1-34:6: information:
Except.ok { n := 3, m := 3, fields := [[1, 2, 3], [4, 5, 6], [7, 8, 9]] }

Code:

abbrev Vec (n : Nat) (a : Type) := { ls : List a // ls.length = n }
abbrev Matrix (n m : Nat) (a : Type) := Vec n (Vec m a)

structure MatrixWrapper where
  n : Nat
  m : Nat
  fields: Vec n (Vec m Nat)
deriving Repr

structure Config where
  n : Nat
  m : Nat

def test_mat (mat : List (List Nat)) : ReaderT Config (Except String)
  MatrixWrapper := do
  let conf ← read
  let n := conf.n
  let m := conf.m
  let p1 : List (Option (Vec m Nat)) := mat.map (
    fun row =>
      if h1 : row.length = conf.m then
        pure ⟨row, h1⟩
      else
        none
  )
  let p2 := p1.filterMap id
  if h2 : p2.length = n then
    let mat : Vec n (Vec m Nat) :=  ⟨p2, h2⟩
    pure {n := n, m := m, fields := mat : MatrixWrapper}
  else
    throw "something"

def output_testmat := test_mat [[1, 2, 3], [4, 5, 6], [7, 8, 9]] {n := 3, m := 3}
#eval output_testmat