Zulip Chat Archive

Stream: general

Topic: Notation for matrices and vectors


view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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]

view this post on Zulip Anne Baanen (Feb 14 2020 at 11:14):

What do you all think?

view this post on Zulip Johan Commelin (Feb 14 2020 at 11:27):

Something like this is certainly a good idea.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 14 2020 at 11:27):

I'll try to find the posts on zulip

view this post 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]
]

view this post on Zulip Johan Commelin (Feb 14 2020 at 11:32):

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

view this post on Zulip Anne Baanen (Feb 14 2020 at 11:55):

It is indeed exactly the same!

view this post on Zulip 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...

view this post on Zulip Patrick Massot (Feb 14 2020 at 12:35):

The elaborator always struggles with explicit sets. Look at:

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Anne Baanen (Feb 24 2020 at 10:21):

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

view this post on Zulip 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?

view this post on Zulip 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