Zulip Chat Archive

Stream: new members

Topic: extracting entries from matrices


view this post on Zulip Apurva Nakade (Jul 23 2020 at 13:15):

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

view this post on Zulip Apurva Nakade (Jul 23 2020 at 13:16):

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

view this post on Zulip Jalex Stark (Jul 23 2020 at 13:17):

I think A is expecting a pair of fin k

view this post on Zulip Jalex Stark (Jul 23 2020 at 13:17):

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

view this post on Zulip Anne Baanen (Jul 23 2020 at 13:18):

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

view this post on Zulip Apurva Nakade (Jul 23 2020 at 13:18):

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

view this post on Zulip Markus Himmel (Jul 23 2020 at 13:20):

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

view this post on Zulip Apurva Nakade (Jul 23 2020 at 13:24):

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

view this post on Zulip Yakov Pechersky (Jul 23 2020 at 13:43):

Are you always adding on an edge, or inserting?


Last updated: May 14 2021 at 23:14 UTC