# Zulip Chat Archive

## 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`

...

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

#### 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 `i`th 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.

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

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