# Zulip Chat Archive

## Stream: general

### Topic: Notation for matrices and vectors

#### Anne Baanen (Feb 14 2020 at 11:13):

This morning, I was playing around with defining notation for vectors and matrices, which would allow us to write:

def v2 : fin 2 → ℕ := {1, 2} def m22 : matrix (fin 2) (fin 2) ℤ := {{1, 2}, {3, 4}} def m32 : matrix (fin 3) (fin 2) ℤ := {{1, 2}, {3, 4}, {4, 5}} @[simp] lemma det_2x2 {α} [comm_ring α] (a b c d : α) : matrix.det ({{a, b}, {c, d}} : matrix (fin 2) (fin 2) α) = a * d - b * c := calc matrix.det ({{a, b}, {c, d}} : matrix (fin 2) (fin 2) α) = ((0 + 1) * (a * (d * 1))) + (((- (0 + 1)) * (c * (b * 1))) + 0) : rfl ... = a * d - b * c : by ring

#### Anne Baanen (Feb 14 2020 at 11:13):

My first implementation generalizes the notation in core Lean for `has_insert.insert : h → t → t`

to `has_dependent_insert.insert : h → t → ht`

:

import data.matrix.basic import linear_algebra.determinant import tactic.ring universes u v variables {α : Type} class has_dependent_insert (h : out_param (Type u)) (t : out_param (Type v)) (ht : Type v) := (insert {} : h → t → ht) notation `{` l:(foldr `, ` (h t, has_dependent_insert.insert h t) (has_emptyc.emptyc _) `}`) := l /- -- Optionally: @[priority 100] instance insert_to_dependent_insert {γ} [has_insert α γ] : has_dependent_insert α γ γ := ⟨insert⟩ -/ instance insert_vector {n : ℕ} : has_dependent_insert α (fin n → α) (fin n.succ → α) := ⟨@fin.cases _ (λ _, α)⟩ instance empty_vector : has_emptyc (fin 0 → α) := ⟨λ x, by exfalso; rcases x with ⟨_, ⟨⟩⟩⟩ -- Either: -- local attribute [reducible] matrix -- Or: instance insert_matrix {n : Type} {m : ℕ} [fintype n] : has_dependent_insert (n → α) (matrix (fin m) n α) (matrix (fin m.succ) n α) := ⟨@fin.cases _ (λ _, n → α)⟩ instance empty_matrix {n : Type} [fintype n] : has_emptyc (matrix (fin 0) n α) := ⟨λ x, by {exfalso, rcases x with ⟨_, ⟨⟩⟩}⟩ @[simp] lemma det_2x2 [comm_ring α] (a b c d : α) : matrix.det ({{a, b}, {c, d}} : matrix (fin 2) (fin 2) α) = a * d - b * c := calc matrix.det ({{a, b}, {c, d}} : matrix (fin 2) (fin 2) α) = ((0 + 1) * (a * (d * 1))) + (((- (0 + 1)) * (c * (b * 1))) + 0) : rfl ... = a * d - b * c : by ring example : fin 2 → ℕ := {1, 2} def m22 : matrix (fin 2) (fin 2) ℤ := {{1, 2}, {3, 4}} def m32 : matrix (fin 3) (fin 2) ℤ := {{1, 2}, {3, 4}, {4, 5}} def wrong_m22 : matrix (fin 2) (fin 2) ℤ := {{1, 2}, {3, 4}, {4, 5}} def wrong_m32 : matrix (fin 3) (fin 2) ℤ := {{1, 2}, {3, 4}} example : matrix.det m22 = 1 * 4 - 2 * 3 := by simp [m22]

#### Anne Baanen (Feb 14 2020 at 11:14):

Although I prefer the braces, this will probably give overload issues because the notation for `has_insert.insert`

is still around. The elaborator also gets stuck quite easily, for example if you remove the type hint in `({{a, b}, {c, d}} : matrix (fin 2) (fin 2) α)`

. We could also make the notation specific to `fin n → α`

, solving the second issue somewhat:

import data.matrix.basic import linear_algebra.determinant import tactic.ring variables {α : Type} def vector_insert {n : ℕ} : α → (fin n → α) → (fin n.succ → α) := @fin.cases _ (λ _, α) def vector_empty : fin 0 → α := λ x, by exfalso; rcases x with ⟨_, ⟨⟩⟩ notation `{` l:(foldr `, ` (h t, vector_insert h t) vector_empty `}`) := l @[simp] lemma det_2x2 [comm_ring α] (a b c d : α) : matrix.det {{a, b}, {c, d}} = a * d - b * c := calc matrix.det {{a, b}, {c, d}} = ((0 + 1) * (a * (d * 1))) + (((- (0 + 1)) * (c * (b * 1))) + 0) : rfl ... = a * d - b * c : by ring example : fin 2 → ℕ := {1, 2} def m22 : matrix (fin 2) (fin 2) ℤ := {{1, 2}, {3, 4}} def m32 : matrix (fin 3) (fin 2) ℤ := {{1, 2}, {3, 4}, {4, 5}} def wrong_m22 : matrix (fin 2) (fin 2) ℤ := {{1, 2}, {3, 4}, {4, 5}} -- Type mismatch: `{{4, 5}}` has type `fin 1 → fin 2 → ℤ` -- but was expected to have type `fin 0 → fin 2 → ℤ` def wrong_m32 : matrix (fin 3) (fin 2) ℤ := {{1, 2}, {3, 4}} -- Type mismatch: `vector_empty` has type `fin 0 → ?m_1 → ℤ` -- but was expected to have type `fin 1 → fin 2 → ℤ` example : matrix.det m22 = 1 * 4 - 2 * 3 := by simp [m22]

#### Anne Baanen (Feb 14 2020 at 11:14):

What do you all think?

#### Johan Commelin (Feb 14 2020 at 11:27):

Something like this is certainly a good idea.

#### Johan Commelin (Feb 14 2020 at 11:27):

I think that a very long time ago, Johannes Hölzl also showed how to do something like this

#### Johan Commelin (Feb 14 2020 at 11:27):

I'll try to find the posts on zulip

#### Johan Commelin (Feb 14 2020 at 11:30):

Aha, it was in a private chat (we were writing code for @Kevin Buzzard's birthday):

import data.vector def {u} fast_matrix (m n : ℕ) (α : Type u) : Type u := vector (vector α n) m def vec {α : Type*} (l : list α) : vector α l.length := ⟨l, rfl⟩ local notation `![` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) := vec l example : fast_matrix 2 2 ℤ := ![ ![1,1], ![0,1] ]

#### Johan Commelin (Feb 14 2020 at 11:32):

@Anne Baanen Isn't your `vector_insert`

the same as `fin.cons`

?

#### Anne Baanen (Feb 14 2020 at 11:55):

It is indeed exactly the same!

#### Kevin Buzzard (Feb 14 2020 at 12:06):

I was moaning about notation in my talk in Bonn two weeks ago (in front of Sebastian Ullrich!) in the context of algebraic geometry, and afterwards @Floris van Doorn sent me a file with some ideas in, which I still have not looked at but have certainly not forgotten about. I'm hoping to have a weekend of Lean where I can catch up -- I've had to deal with real life this week...

#### Patrick Massot (Feb 14 2020 at 12:35):

The elaborator always struggles with explicit sets. Look at:

#check {1} #check {(1 : ℕ)} #check ({1} : set ℕ)

#### Patrick Massot (Feb 14 2020 at 12:35):

So I wouldn't expect the situation for matrices to be better. We can only hope :four_leaf_clover:

#### Anne Baanen (Feb 24 2020 at 10:20):

I'm ready to revisit this topic and do some bikeshedding today. It turns out that notation with `{...}`

is special-cased in the C++ parser, so defining our own `{...}`

-based notation will definitely result in unfixable notation conflicts (the first one I saw was with `simp {contextual := tt}`

of all things), meaning that option is out.

#### Anne Baanen (Feb 24 2020 at 10:21):

@Kevin Buzzard Do you have some time to send that file?

#### Kevin Buzzard (Feb 24 2020 at 13:26):

Your message prompted me to finally take a look at what @Floris van Doorn sent me -- but I can't get it to work right now. Perhaps he should be the one talking to you about this?

#### Floris van Doorn (Feb 24 2020 at 18:44):

Since braces already have many different meanings and are handled in a special way in the parser, I think it would be better to use a different symbol for matrices.

The file I sent to Kevin was about pretty printing the tactic state by defining a new interactive tactic environment.

Last updated: May 10 2021 at 19:16 UTC