Using subsingleton of fin 0

Stream: new members

[Yakov Pechersky]

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]

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]

#mwe

[Kenny Lau]

(the update_column in the first lemma requires decidable

[Kenny Lau]

wait that isn't the reason it fails

[Kenny Lau]

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]

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]

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]

convert update_col_column_empty M z v works for the first example.

[Reid Barton]

With update_col_column_empty' both instance arguments come separately from search.

[Reid Barton]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Reid Barton]

I guess the ' version is better.

[Yakov Pechersky]

Thanks!

[Reid Barton]

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]

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

[Reid Barton]

@[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 :=