extracting entries from matrices

Stream: new members

[Apurva Nakade]

Given a matrix A, I want to define a new matrix obtained by adding a row and column to A.
I tried the following but it fails because of type mismatch. Dunno how to fix it.

import data.fintype.basic
import data.matrix.basic

open_locale matrix

def matrix_extension {k : ℕ} (A : matrix (fin k) (fin k) ℕ) : matrix (fin (k+1)) (fin (k+1)) ℕ
:=
λ i j,
match i.val, j.val with
| 0, 0     := 1
| 0, _     := 0
| _, 0     := 0
| (x+1), (y+1) := A x y
end

[Apurva Nakade]

A x y doesn't work because A is expecting a pair of fintype

[Jalex Stark]

I think A is expecting a pair of fin k

[Jalex Stark]

does something like A ⟨x, _ ⟩ ⟨y, _⟩ work?

[Anne Baanen]

Instead of writing a match statement, you can also try fin.cons : α -> (fin n -> α) -> fin (n+1) -> α.

[Apurva Nakade]

Jalex Stark said:
It says don't know how to synthesize placeholder
context:

[Markus Himmel]

Here is one way to do it using a match, but @Anne Baanen's way is almost certainly better.

import data.fintype.basic
import data.matrix.basic

open_locale matrix

def matrix_extension {k : ℕ} (A : matrix (fin k) (fin k) ℕ) : matrix (fin (k+1)) (fin (k+1)) ℕ
:=
λ i j,
match i, j with
| ⟨0, _⟩, ⟨0, _⟩       := 1
| ⟨0, _⟩, _            := 0
| _, ⟨0, _⟩            := 0
| ⟨x+1, hx⟩, ⟨y+1, hy⟩ := A ⟨x, nat.lt_of_succ_lt_succ hx⟩ ⟨y, nat.lt_of_succ_lt_succ hy⟩
end

[Apurva Nakade]

Thank you!!!

This definitely works, with the added bonus that I understand what's going on :P
I will give it a try using fin.consas well

[Yakov Pechersky]

Are you always adding on an edge, or inserting?