## 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