Why does `Matrix.row` use `Unit` instead of `Fin 1`?

Stream: mathlib4

[Sina Hazratpour 𓃵]

In the following MWE, Matrix.row ![1, 1] yields the error "expected Unit found Fin 1". Why did we choose Unit in this definition and can this be made working somehow?

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.RowCol
import Mathlib.Data.Real.Basic

open Matrix
example : Fin 1 ≃ Unit := by exact finOneEquiv


/-
type mismatch
  of ![![1, 1]]
has type
  Matrix (Fin 1) (Fin 2) ?m.224 : Type ?u.54
but is expected to have type
  Matrix Unit (Fin (Nat.succ (Nat.succ 0))) ?m.55 : Type ?u.54
-/
example : Matrix.row ![1, 1] = !![1, 1] := sorry

[Jon Eugster]

@Sina following our conversation earlier, here is a PR that uses Fin 1 instead of Unit in the definition of Matrix.row and Matrix.col:

#11522

It does look like a very reasonable change to me. Obviously some () need to be replaced with 0, but essentially there are no notable implications for Mathlib - except of course that now matrix-notation and row/col are more compatible.

[Jon Eugster]

@Eric Wieser, @Yaël Dillies you two commented about preferrably using a generic Unique ι instead of Fin 1, by which I assumed you meant the following:

def col {ι : Type} [Unique ι] (w : m → α) : Matrix m ι α :=
  of fun x _ => w x

but then an expression like

@[simp]
theorem col_apply (w : m → α) (i j) : col w i j = w i :=
  rfl

gets stuck because it can't find which ι to use, i.e. it fails to synthesize "Unique ?m.227". This means one would need to write col (ι := Fin 1) w i j each time.

Did I misunderstand what you proposed?

[Yaël Dillies]

That's only a problem for generic lemmas. For specific lemmas, ι will be inferred through unification

[Yaël Dillies]

Also surely you mean

@[simp]
theorem col_apply (w : m → α) (i) (j : ι) : col w i j = w i :=
  rfl

[Jon Eugster]

Oh I see, we then need to extend basically all (generic) theorems involving col or row by this ι type.

I'm not fully convinced that this is desirable and not just making the API harder to use. For sure it's going to be a larger diff on the PR, but I can look into it a bit more.

[Eric Wieser]

Yaël Dillies said:

That's only a problem for generic lemmas. For specific lemmas, ι will be inferred through unification

I think the question is whether this actually happens effectively

[Eric Wieser]

One thing we could do to make this less painful is add notation for the type Matrix (Fin m) (Fin n) R

[Jon Eugster]

Eric Wieser said:

One thing we could do to make this less painful is add notation for the type Matrix (Fin m) (Fin n) R

I don't think I understand yet what you're suggesting. How would that differ from !![a,b;c,d]?

And I mean we do have concrete examples where we'd prefer Fin 1 as the one-point-type. Are there cases anywhere where we would prefer anything else to be our "canonical" one-point-type?

[Jon Eugster]

(I started doing the change at #11536, but so far I don't see how the user will not be confronted with random Unique types ι appearing here and there which cannot be guessed by lean)

[Eric Wieser]

I mean something like (col v : R^m×1)

[Yaël Dillies]

I was thinking something like M_[m, n][R]

[Eric Wieser]

What's the motivation for wanting to use row and col for Fin? Can't we use !![a; b] and !![a, b] instead of col ![a, b] and row ![a, b]? It would be nice to see a slightly more realistic motivating example than Matrix.row ![1, 1] = !![1, 1].

[Eric Wieser]

I guess the change runs into a recurring point of tension; do you define functions as generally as possible, or do you define them to operate on some universal object for which there are canonical maps to / from the general types?

[Eric Wieser]

(see also: Yael's Finset.dens(ity), FooHom vs FooHomClass, ...)

[Eric Wieser]

In the context of this thread, Unique is the general version, and Unit / Fin 1 are fighting to be that universal object

[Notification Bot]

4 messages were moved from this topic to #mathlib4 > Notation for Matrix (Fin m) (Fin n) R by Eric Wieser.

[Martin Dvořák]

Breaking changes like this one make me unhappy (not asking for anything; I'm just complaining).

[Kim Morrison]

Martin Dvořák said:

Breaking changes like this one make me unhappy (not asking for anything; I'm just complaining).

What is the breaking change your referring to here?

[Yaël Dillies]

#11522

[Jon Eugster]

I think you mean #11536

[Kim Morrison]

Oh, I see, that is interesting that you need to specify the [Unique] type that you want to index the row/column by. I'm sympathetic to Martin here. :-)

[Jon Eugster]

I still think #11522 would have been way less intrusive and nobody would have noticed that "fix", but it was decided by several reviewers that it's better to generalise the notion of a column/row matrix instead.

[Riccardo Brasca]

I have maybe underestimated the pain of having to write (ι := ...) a lot. On the other hand it is nice to have this degree of generality.