pi has_one as default instance

Stream: general

[Yakov Pechersky]

Is it expected that matrix notation is inferred to be the function, so that a notated matrix to the 0th power is _not_ equal to the identity matrix?

import data.matrix.notation

example (n : ℕ) (hn : n = 0) :
  (![![1, 1, 1], ![0, 1, 1], ![0, 0, 1]] : matrix _ _ ℕ) ^ n ≠ (1 : matrix _ _ ℕ) :=
begin
  rw [hn, pow_zero],
  intro H,
  have := congr_fun (congr_fun H 0) 1, -- 1 0 1 = 1 0 1
  simpa [matrix.one_apply] using this
end

[Alex J. Best]

I guess using docs#id is a workaround

import data.matrix.notation

example (n : ℕ) (hn : n = 0) :
  (id ![![1, 1, 1], ![0, 1, 1], ![0, 0, 1]] : matrix _ _ ℕ) ^ n = (1 : matrix _ _ ℕ) :=
begin
  rw [hn, pow_zero],
end

[Yakov Pechersky]

Thanks! Any thoughts on why this is happening?

[Alex J. Best]

Only that the vector notation is really defining a term of type fin 0.succ.succ → fin 0.succ.succ → nat and that the type ascription is only checking that this type is equal to matrix _ _ nat rather than forcing it to be treated like that for typeclass resolution.

[Yakov Pechersky]

I see. And since matrix is only really a type synonym over functions, it's not using the separate instance for matrix.

[Alex J. Best]

Yeah and you can't change vec_cons to return matrix blah blah because the same notation is used for rows and full matrices, an alternate design would be to have a separate notation for matrix_cons that only constructs matrices from rows, but this seems less elegant in the long run?

import data.matrix.notation
variable {α : Type*}

def mat_empty {n : ℕ} : fin 0 → fin n → α :=
fin_zero_elim

def mat_cons {n m : ℕ} (h : fin m → α) (t : matrix (fin n) (fin m) α) : matrix (fin n.succ) (fin m) α :=
fin.cons h t
notation `![[` l:(foldr `, ` (h t, mat_cons h t) mat_empty `]]`) := l

example (n : ℕ) (hn : n = 0) :
  (![[![1, 1, 1], ![0, 1, 1], ![0, 0, 1] ]] : matrix _ _ ℕ) ^ n = (1 : matrix _ _ ℕ) :=
begin
  rw [hn, pow_zero],
end

[Heather Macbeth]

I've encountered this unfortunate feature of matrices before, too. Another solution: tell it at the time it takes a power what type it should be.

example (n : ℕ) (hn : n = 0) :
  @has_pow.pow (matrix (fin 3) (fin 3) ℕ) _ _ (![![1, 1, 1], ![0, 1, 1], ![0, 0, 1]]) n = 1 :=
begin
  rw [hn, pow_zero]
end

[Eric Wieser]

Does putting the power inside the (_ : matrix n n R) help at all?

[Yakov Pechersky]

Yes, it does. Thanks!