## Stream: new members

### Topic: Using subsingleton of fin 0

#### Yakov Pechersky (Jul 15 2020 at 23:27):

Why doe the second proof not work? I couldn't find the mismatch with pp.all.

import linear_algebra.nonsingular_inverse
import data.equiv.fin

variables {R : Type*} [field R] {n : ℕ} {n' : Type} [fintype n']

open matrix

@[simp] lemma update_col_column_empty [subsingleton n'] (M : matrix (fin n) n' R) {z : n'} {v : fin n → R} :
update_column M z v = λ i j, v i :=
begin
ext i j,
have : z = j,
exact subsingleton_iff.mp (by apply_instance) z j,
rw this,
simp only [update_column_self],
end

example (M : matrix (fin n) (fin 0) R) {z : fin 0} {v : fin n → R} :
update_column M z v = λ i j, v i :=
begin
haveI : subsingleton (fin 0) := by apply_instance,
rw @update_col_column_empty R _ n (fin 0) _ _ M z v,
sorry
end


#### Yakov Pechersky (Jul 15 2020 at 23:34):

A [decidable_eq n'] instance was missing in the first lemma which makes the second one work. Yet the first lemma doesn't seem to need decidable_eq...

#mwe

#### Kenny Lau (Jul 16 2020 at 05:51):

(the update_column in the first lemma requires decidable

#### Kenny Lau (Jul 16 2020 at 05:53):

wait that isn't the reason it fails

#### Kenny Lau (Jul 16 2020 at 05:53):

the reason it fails is because update_column expects the row type and the column type to be the same, yet your M has column type fin n and row type n'

#### Yakov Pechersky (Jul 16 2020 at 17:12):

I was on a branch of mathlib (#3403), sorry. Here is a #mwe

import linear_algebra.matrix
import data.equiv.fin

universes u v

section updatedef
variables {m n : Type u} {α : Type v} {i : n} {j : m} {b : m → α} {c : n → α} [fintype n] [fintype m]
variables {A : matrix n m α}

/-- Update, i.e. replace the ith column of matrix A with the values in b. -/
def update_column [decidable_eq m] (A : matrix n m α) (j : m) (b : n → α) : matrix n m α :=
λ i, function.update (A i) j (b i)

@[simp] lemma update_column_self [decidable_eq m] : update_column A j c i j = c i :=
function.update_same j (c i) (A i)

end updatedef

section lemmas
variables {n : Type} {α : Type v} [fintype n]

-- this has no [decidable_eq n] yet update_column does not complain
@[simp] lemma update_col_column_empty
{n' : ℕ} [subsingleton n] (M : matrix (fin n') n α) (z : n) (v : fin n' → α) :
update_column M z v = λ i j, v i :=
begin
ext i j,
have : z = j,
exact subsingleton_iff.mp (by apply_instance) z j,
rw this,
simp only [update_column_self],
end

-- no [decidable _eq n] used here
example {n' : ℕ} (M : matrix (fin n') (fin 0) α) {z : fin 0} {v : fin n' → α} :
update_column M z v = λ i j, v i :=
begin
haveI h : subsingleton (fin 0) := by apply_instance,
ext i j,
rw @update_col_column_empty α _ n' (fin 0) _ _ h M z v,
sorry,
end

-- this has a [decidable_eq n]
@[simp] lemma update_col_column_empty'
{n' : ℕ} [subsingleton n] [decidable_eq n] (M : matrix (fin n') n α) (z : n) (v : fin n' → α) :
update_column M z v = λ i j, v i :=
begin
ext i j,
have : z = j,
exact subsingleton_iff.mp (by apply_instance) z j,
rw this,
simp only [update_column_self],
end

-- now simp works
example {n' : ℕ} (M : matrix (fin n') (fin 0) α) {z : fin 0} {v : fin n' → α} :
update_column M z v = λ i j, v i := by simp only [update_col_column_empty']

end lemmas


#### Reid Barton (Jul 16 2020 at 17:32):

It's a problem with coherence of instances. There are two different ways to construct decidable_eq (fin 0).
update_col_column_empty is using the instance subsingleton -> decidable_eq, but it's not the instance inferred in the first example.

#### Reid Barton (Jul 16 2020 at 17:32):

convert update_col_column_empty M z v works for the first example.

#### Reid Barton (Jul 16 2020 at 17:34):

With update_col_column_empty' both instance arguments come separately from search.

#### Reid Barton (Jul 16 2020 at 17:34):

(By the way, do you really want fin 0? you can also prove the example by fin_zero_elim z.)

#### Yakov Pechersky (Jul 16 2020 at 17:35):

That makes sense. Which version of the lemma should I keep then?

#### Yakov Pechersky (Jul 16 2020 at 17:35):

You're right about fin 0. But for fin 1 the issue would rear its head again

#### Reid Barton (Jul 16 2020 at 17:45):

I guess the ' version is better.

Thanks!

#### Reid Barton (Jul 16 2020 at 17:49):

What might be even better is to use {}s for the decidable_eq n argument. The logic is normally you will infer from the use site what the instance will be, because it appears in the expression update_column M z v. However you can't infer subsingleton because that does not appear in the conclusion of the theorem.

#### Yakov Pechersky (Jul 16 2020 at 18:13):

I am not sure what you mean by {}. Can you show an example please?

#### Reid Barton (Jul 16 2020 at 18:14):

@[simp] lemma update_col_column_empty'
{n' : ℕ} [subsingleton n] {h : decidable_eq n} (M : matrix (fin n') n α) (z : n) (v : fin n' → α) :
update_column M z v = λ i j, v i :=


Last updated: May 16 2021 at 05:21 UTC