Zulip Chat Archive

Stream: new members

Topic: Using subsingleton of fin 0


view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Jul 16 2020 at 05:50):

#mwe

view this post on Zulip Kenny Lau (Jul 16 2020 at 05:51):

(the update_column in the first lemma requires decidable

view this post on Zulip Kenny Lau (Jul 16 2020 at 05:53):

wait that isn't the reason it fails

view this post on Zulip 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'

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jul 16 2020 at 17:32):

convert update_col_column_empty M z v works for the first example.

view this post on Zulip Reid Barton (Jul 16 2020 at 17:34):

With update_col_column_empty' both instance arguments come separately from search.

view this post on Zulip 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.)

view this post on Zulip Yakov Pechersky (Jul 16 2020 at 17:35):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 16 2020 at 17:45):

I guess the ' version is better.

view this post on Zulip Yakov Pechersky (Jul 16 2020 at 17:47):

Thanks!

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jul 16 2020 at 18:13):

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

view this post on Zulip 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