Notation for matrices and vectors

Stream: general

[Anne Baanen]

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]

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]

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]

What do you all think?

[Johan Commelin]

Something like this is certainly a good idea.

[Johan Commelin]

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

[Johan Commelin]

I'll try to find the posts on zulip

[Johan Commelin]

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]

@Anne Baanen Isn't your vector_insert the same as fin.cons?

[Anne Baanen]

It is indeed exactly the same!

[Kevin Buzzard]

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]

The elaborator always struggles with explicit sets. Look at:

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

[Patrick Massot]

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

[Anne Baanen]

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]

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

[Kevin Buzzard]

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]

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.