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.

[Eric Wieser]

It is probably worth revisiting this thread now that ⬝ is no longer used for matrix multiplication (we use * instead)

[Martin Dvořák]

I really wish we had infix operators for all those multiplications!

[Martin Dvořák]

Hear me out!
Matrix times vector: A ₘ⋅ v
Vector times matrix: v ⋅ₘ A
Matrix times matrix: A * B
Dot product: u ⋅ᵥ v
Cross product: u ×₃ v
The first two symbols are new (my suggestion).
What do you think?

[Adam Topaz]

Why can't HMul work for all of these?

[Adam Topaz]

(except maybe the cross product and dot product)

[Johan Commelin]

I would think the first two are good examples of left and right actions. So they could use SMul.

[Martin Dvořák]

Both would use \smul then?

[Johan Commelin]

Well, there are variant notations of SMul that distinguish left and right actions.

[Johan Commelin]

A right action is a left action, but acting via the multiplicative opposite.

[Martin Dvořák]

Ah, so in both cases, it would be a matrix having an action on vector?

[Eric Wieser]

Johan Commelin said:

I would think the first two are good examples of left and right actions. So they could use SMul.

They're not heterogenous homogenous, so they'd have to use HSMul

[Eric Wieser]

But this would then probably be fighting the elaborator changes that Kyle made which fixed ^.

[Jireh Loreaux]

They are heterogeneous, so they need to use HSMul.

[Jireh Loreaux]

(deleted)

[Eric Wieser]

I just got my words muddled, edited above

[Kyle Miller]

Long term, there's still the possibility of tweaking the "expression tree elaborator" that all the basic operators use, including \smul. It would be good to collect elaboration issues.

This elaborator basically turns itself off if the expressions involved can't be coerced to one another. \smul has the wrinkle that (1) it works best for left actions and (2) the RHS can't hint to the LHS what type it should have.

I'm not sure how well known this is, but in mathlib we have a similar elaborator that tries to find a common "functor" to coerce everything to. I think it's just used for Set.prod at the moment.

[Eric Wieser]

It's perhaps also worth noting that we should be very careful with typeclass inheritance of heterogenous operators, as discussed in S1.1.8 of the attachment in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Cardinality.20of.20permutation/near/411183622

[Martin Dvořák]

Why not just add notation for mul_vec and vec_mul without typeclasses?

[Kyle Miller]

It would be nice if these matrix-vector products could be in the language of HSMul somehow, because they're actions (well, multi-sort actions, though definitely actions when the matrices are square).

Using HSMul directly probably has some bad elaboration issues, since it won't be able to link up the dimensions. Though perhaps that's fixable with default instances?

If that doesn't work, maybe we could make a A ₘ• v notation that elaborates to A • v while somehow unifying the dimensions. Maybe there could be a pretty printer that prints this as A ₘ• v so that there's any hope of round tripping (i.e., successfully pasting in and using something from the infoview).

[Kyle Miller]

That is getting into redesign though. I don't see any reason not to add in notation for A ₘ• v and v •ₘ A for the pre-existing mul_vec and vec_mul.

[Eric Wieser]

Or perhaps ₘ•> and <•ₘ for consistency with left and right actions

[Martin Dvořák]

Can we draw a conclusion please? I would like to add it to Mathlib today.

[Yaël Dillies]

Unclear to me

[Martin Dvořák]

Eric Wieser said:

Or perhaps ₘ•> and <•ₘ for consistency with left and right actions

I'd rather not.
I find using the symbols < and > confusing when not in a syntax for binary relations.
As far as GitHub show me, the operators•> and <• are used only in two files anyway.
I'd rather add ₘ• and •ₘ but anything will be better than the status quo.

[Jireh Loreaux]

It's unclear to me what the ₘ is supposed to mean in this notation. And I agree with Eric about consistency, so something involving <• or •> would be preferable. (Martin, I could turn the tables and complain that it's unclear whether ₘ• should be A * v or v * A, so I don't see your reasoning as a good argument.)

[Jireh Loreaux]

If we used •ᵥ and ᵥ•, for mulVec and vecMul, respectively, then at least the notation order would match the word order. Although I take it that •ᵥ is already taken for docs#dotProduct.

[Eric Wieser]

Thinking again, I think I'd prefer to avoid • in the notation, since I am wary of ending up with a future generalization of vecMul that performs SMul between the coefficients instead of * (due to a much higher risk of diamonds)

[Eric Wieser]

@Jireh Loreaux, note that docs#Matrix.dotProduct uses a different dot symbol, ⬝ᵥ

[Jireh Loreaux]

Lol, • and ⬝ are nearly visually indistinguishable for me with my font and size.

[Martin Dvořák]

So A ₘ* v and v *ₘ A or rather A *ᵥ v and v ᵥ* A will we declare?

[Eric Wieser]

Should we use the same notation for both?

[Kyle Miller]

I'd say let's go with A *ᵥ v and v ᵥ* A, unless you have a tested design for how to get them to use the same notation, without any elaboration gotchas.

[Kyle Miller]

If we change this design later, we can easily search/replace when the notations are different.

[Jireh Loreaux]

I actually like having the different notations, because then I don't have to mentally juggle types, but this is not a major issue I suppose since I can hover.

[Yaël Dillies]

Martin Dvořák said:

As far as GitHub show me, the operators•> and <• are used only in two files anyway.

This is because the notation is really new and I haven't had time to refactor its potential use cases to use it.

[Kyle Miller]

I might suggest *> and <* for this for parallelism, but these are already taken by applicative monads. Thanks Haskell!

[Martin Dvořák]

Eric Wieser said:

Should we use the same notation for both?

Are you worried that A *ᵥ v and v ᵥ* A would make v ⋅ᵥ w look inadequate?

[Martin Dvořák]

Kyle Miller said:

I'd say let's go with A *ᵥ v and v ᵥ* A,

Imma implement this right now.

[Martin Dvořák]

#10297

[Eric Wieser]

Martin Dvořák said:

Eric Wieser said:

Should we use the same notation for both?

Are you worried that A *ᵥ v and v ᵥ* A would make v ⋅ᵥ w look inadequate?

Yes, the lack of symmetry bugs me slightly, but I don't think it's worse than the status quo so I'm happy enough with this proposal

[Martin Dvořák]

Martin Dvořák said:

#10297

Alright, ready for review!

[Martin Dvořák]

Another potential refactoring is to write ⋅ᵥ in place of dotProduct everywhere.