Notation for mul_vec and vec_mul

Stream: general

[Alexander Bentkamp]

What do you all think about introducing infix notations for matrix.mul_vec and matrix.vec_mul?

I am currently working on this lemma:

lemma schur_complement_eq' {A : matrix n n R} (hA : A.is_symm) [invertible A] :
(vec_mul (sum.elim x y) (from_blocks A B Bᵀ D)) ⬝ᵥ (sum.elim x y) =
  vec_mul (x + (mul_vec (A⁻¹ ⬝ B) y)) A ⬝ᵥ (x + mul_vec (A⁻¹ ⬝ B) y) + vec_mul y (D - Bᵀ ⬝ A⁻¹ ⬝ B) ⬝ᵥ y :=

It is really hard to read without infix notation. I would propose something like this:

localized "infix ` ⊕ᵥ `:65 := sum.elim" in matrix
localized "infix ` ᵛ⬝ `:73 := vec_mul" in matrix
localized "infix ` ⬝ᵛ `:74 := mul_vec" in matrix

lemma schur_complement_eq {A : matrix n n R} (hA : A.is_symm) [invertible A] :
(x ⊕ᵥ y) ᵛ⬝ from_blocks A B Bᵀ D ⬝ᵥ (x ⊕ᵥ y) =
  (x + A⁻¹ ⬝ B ⬝ᵛ y) ᵛ⬝ A ⬝ᵥ (x + A⁻¹ ⬝ B ⬝ᵛ y) + y ᵛ⬝ (D - Bᵀ ⬝ A⁻¹ ⬝ B) ⬝ᵥ y :=

[Eric Wieser]

I feel like if we go down that route we should change dot_product u v to u ᵛ⬝ᵛ v

[Eric Wieser]

The other option would be a has_mat_mul class and use ⬝ for all four operations

[Alexander Bentkamp]

⬝ for all of them would be amazing. What would be the best way to approach such a big refactoring?

[Eric Wieser]

I don't think the refactor will be all that big, although a danger with this change is that ![![1,2],![3,4]] ⬝ ![![1,2],![3,4]] = ![10, 20]

[Eric Wieser]

(because ![![...]] creates a vector of vectors not a matrix)

[Anne Baanen]

Eric Wieser said:

I don't think the refactor will be all that big, although a danger with this change is that ![![1,2],![3,4]] ⬝ ![![1,2],![3,4]] = ![10, 20]

I believe it would not be a problem since we can require that the entries of the vector are non_unital_non_assoc_semiring, and now we're applying has_mat_mul to the entries

[Eric Wieser]

I don't understand that suggestion. The problem is that

![![1,2],![3,4]] ⬝ ![![1,2],![3,4]]
  = dot_product ![![1,2],![3,4]] ![![1,2],![3,4]]
  = ![1,2] * ![1,2] + ![3,4] * ![3,4]
  = ![1,4] + ![9,16]
  = ![10, 20]

[Eric Wieser]

docs#pi.non_unital_non_assoc_semiring

[Eric Wieser]

Arguably the real problem here is that we don't have notation that actually produces a matrix

[Eric Wieser]

![![1,2],![3,4]] * ![![1,2],![3,4]] already fails to perform matrix multiplication

[Eric Wieser]

This has come up before, but I think the lean3 notation command isn't powerful enough to allow a special !![1, 2; 3, 4] notation

[Eric Wieser]

We could use a user_notation, but then it would print as something like to_matrix ![![1,2],![3,4]].

[Eric Wieser]

Maybe thats ok though

[Anne Baanen]

Indeed, we can't put the notation on matrix currently, or the instance isn't picked up.

import data.matrix.notation

class has_mat_mul (α β : Type*) (γ : out_param Type*) :=
(mat_mul : α → β → γ)

#print notation
infix `⬝`:75 := has_mat_mul.mat_mul

variables {m n o : Type*} {α β γ : Type*}

/-
-- Notation not found
instance matrix.has_mat_mul [non_unital_non_assoc_semiring α] [fintype n] :
  has_mat_mul (matrix m n α) (matrix n o α) (matrix m o α) :=
⟨matrix.mul⟩
-/

instance matrix.has_mat_mul [non_unital_non_assoc_semiring α] [fintype n] :
  has_mat_mul (m → n → α) (n → o → α) (m → o → α) :=
⟨matrix.mul⟩

@[priority 100]
instance matrix.has_dot_product [non_unital_non_assoc_semiring α] [fintype n] :
  has_mat_mul (n → α) (n → α) α :=
⟨matrix.dot_product⟩

instance matrix.has_mat_mul_right [non_unital_non_assoc_semiring α] [fintype n] :
  has_mat_mul (matrix m n α) (n → α) (m → α) :=
⟨matrix.mul_vec⟩

instance matrix.has_mat_mul_left [non_unital_non_assoc_semiring α] [fintype m] :
  has_mat_mul (m → α) (matrix m n α) (n → α) :=
⟨matrix.vec_mul⟩

#eval ((![![1,2],![3,4]]) ⬝ (![![1,2],![3,4]]))
#eval ((![![1,2],![3,4]] : matrix (fin 2) (fin 2) ℕ) ⬝ (![![1,2],![3,4]] : matrix (fin 2) (fin 2) ℕ))

[Eric Wieser]

(x : A) * (x : A) where x : X is not enough to tell lean to use the multiplication on A

[Alexander Bentkamp]

Ok, but what's the problem with the instance on m → n → α as in Anne's code above?

[Eric Wieser]

I think it's a bad idea to ever spell matrix m n a in that way

[Eric Wieser]

It feels as bad as spelling opposite a as a or multiplicative a as a

[Eric Wieser]

This does the right thing:

#eval (show matrix (fin 2) (fin 2) ℕ, from ![![1,2],![3,4]])
    ⬝ (show matrix (fin 2) (fin 2) ℕ, from ![![1,2],![3,4]])

[Eric Wieser]

foo (x : A) where x : X and def A := X means "parse x as an A, but then call foo with x as an X"

[Eric Wieser]

Here's a nicer spelling:

def to_matrix : (m → n → α) ≃ matrix m n α := equiv.refl _
@[simp] lemma to_matrix_apply (f : m → n → α) (i j) : to_matrix f i j = f i j := rfl
@[simp] lemma to_matrix_symm_apply (f : matrix m n α) (i j) : to_matrix.symm f i j = f i j := rfl

notation `!ₘ[` l:(foldr `, ` (h t, matrix.vec_cons h t) matrix.vec_empty `]`) := to_matrix l

#eval !ₘ[![1,2],![3,4]] ⬝ !ₘ[![1,2],![3,4]]  -- does the right thing

[Eric Wieser]

I implemented the user_notation in #14665

[Eric Wieser]

Now that !![1, 2; 3, 4] notation is merged, we could consider revisiting class has_mat_mul

[Wrenna Robson]

What are the operations it would apply to (and what is that symbol - is it different from the smul symbol?)

[Alexander Bentkamp]

The symbol is \cdot. It's different from the smul symbol. The dot is a bit smaller.

[Alexander Bentkamp]

We could use it for matrix.mul, where it is used already, for matrix.mul_vec, matrix.vec_mul, and matrix.dot_product.

[Wrenna Robson]

And possibly matrix.vec_mul_vec?

[Wrenna Robson]

Though that may not work with matrix.dot_product.

[Eric Wieser]

We don't need notation for that, you can spell it col v ⬝ row w

[Eric Wieser]

You don't have that option for the others, because the result type ends up a matrix not a vector

[Wrenna Robson]

Ah, so you can.

[Eric Wieser]

I tried this in #15585, but it doesn't work as well as I'd hoped because lean's overloaded notations:

• Doesn't seem to work with local or open_locale
• Unfolds type synonyms

[Alexander Bentkamp]

I thought you planned to create a type class has_mat_mul . Why do you use overloaded notations now?

[Eric Wieser]

The typeclass had its own problems:

• The out_param stuff doesn't always help, you still can't write things like v ⬝ 0
• You now have to change everything to be stated about has_mat_mul.mul instead of dot_product etc. This is a lot more unwieldy if the notation is not enabled;

[Alexander Bentkamp]

I see. But I feel that the type class approach works quite well for +, *, •, etc. The fact that we can't write v ⋅ 0 doesn't shock me. Somehow we need to tell Lean what 0 we mean. You probably can't write a • 0 either, right?

[Eric Wieser]

a • 0 isn't quite as bad because lean knows the result type is the same type as the 0

[Alexander Bentkamp]

Ah, ok, right. ⋅ would be extremely ambiguous about what comes in and what comes out...

[Alexander Bentkamp]

How about this: we add a typeclass has_mat_mul using ⋅ and in addition localized notations ᵥ⋅ₘ, ᵥ⋅ₘ, ₘ⋅ₘ, ᵥ⋅ᵥ that abbreviate has_mat_mul with the appropriate type class instance specified. So in most cases, you'll be able to use ⋅. Whenever Lean doesn't understand what's going on because it's not clear what types the arguments have, you can use the more specific notation.

It would be nice if the output window would show ⋅ whenever possible, though.