concrete matrix multiplication

Stream: Is there code for X?

[Jeremy Avigad]

Can anyone tell me how to replace the sorry below by a proof?

import data.matrix.notation
import data.real.basic

theorem add_eq (a b c d e f g h : real) :
  ![![a, b], ![c, d]] + ![ ![e, f], ![g, h]] = ![![a + e, b + f], ![c + g, d + h]] :=
by simp only [matrix.cons_add_cons, matrix.empty_add_empty]

theorem mul_eq (a b c d e f g h : real) :
  ![![a, b], ![c, d]] * ![ ![e, f], ![g, h]] =
    ![![a * e + b * f, a * g + b * h], ![c * e + d * f, c * g + d * h]] :=
sorry

[Alex J. Best]

https://github.com/leanprover-community/mathlib/blob/master/test/matrix.lean#L53 is the most recent mathlib way to state and prove this, which version are you on?

[Jeremy Avigad]

I am probably working with an old version of mathlib, but I can update. Thanks!

[Eric Wieser]

docs#matrix.mul_fin_two is a direct statement of your second lemma

[Eric Wieser]

When I find the time, I'm planning to adapt the approach from this Zulip thread to generate these lemmas automaticaly for arbitrary m and n

[Jeremy Avigad]

Thanks again. I am trying to work this out for a friend who is thinking about using Lean in an undergraduate course on linear algebra. He says that even the 2x2 case will be helpful for students to work out definitions.

For the record, I also got this:

theorem transpose_eq {a b c d : real} : !![a, b; c, d]ᵀ = !![a, c; b, d] :=
begin
  ext i j,
  dsimp [matrix.of],
  fin_cases i; fin_cases j; simp
end

If there is a better way, I will be happy to hear it.

[Eric Wieser]

dsimp [matrix.of] is not something I was intending to be done

[Eric Wieser]

Because doing that makes your goal not quite type correct any more

[Eric Wieser]

theorem transpose_eq {a b c d : ℕ} : !![a, b; c, d]ᵀ = !![a, c; b, d] :=
begin
  ext i j,
  fin_cases i; fin_cases j; simp [matrix.transpose_apply],
end

is slightly better

[Eric Wieser]

It's a bit weird how simp gets in a dead end without the help

[Eric Wieser]

Again, probably we want a metaprogram like the one linked above here

[Heather Macbeth]

Jeremy Avigad said:

theorem mul_eq (a b c d e f g h : real) :
  ![![a, b], ![c, d]] * ![ ![e, f], ![g, h]] =
    ![![a * e + b * f, a * g + b * h], ![c * e + d * f, c * g + d * h]] :=
sorry

@Jeremy Avigad There's actually something terrible going on with this one when I try it locally. It's interpreting the multiplication as pi-type multiplication, i.e. pointwise multiplication of the entries. I've never seen this before, I wonder if something changed recently?

[Heather Macbeth]

I disabled that with (!)

local attribute [-instance] pi.has_mul pi.distrib pi.semiring pi.comm_semiring pi.ring pi.comm_ring
  pi.mul_zero_class pi.mul_zero_one_class pi.mul_one_class pi.monoid_with_zero pi.comm_monoid
  pi.semigroup_with_zero pi.monoid pi.div_inv_monoid pi.division_monoid pi.division_comm_monoid
  pi.non_unital_non_assoc_semiring pi.non_unital_non_assoc_ring pi.comm_monoid_with_zero
  pi.semigroup pi.comm_semigroup
  pi.non_unital_semiring pi.non_unital_comm_semiring pi.non_unital_ring pi.non_unital_comm_ring
  pi.non_assoc_semiring pi.non_assoc_ring

[Heather Macbeth]

And then Lean couldn't find the multiplication instance I wanted, although it did pick it up when I wrote @has_mul.mul _ matrix.has_mul rather than *.

[Yaël Dillies]

Yes, @Eric Wieser changed this recently. You now should use !![a, b; c, d] (or something of sort) instead of ![![a, b], ![c, d]].

[Yakov Pechersky]

And also why we have the cdot for matrix.mul

[Eric Wieser]

To be clear, I didn't change the behavior, that's always been broken: what I changed was adding new syntax that is no longer broken in that way

[Heather Macbeth]

Anyway, this works for me:

theorem mul_eq (a b c d e f g h : real) :
  !![a, b; c, d] * !![e, f; g, h] =
    !![a * e + b * g, a * f + b * h; c * e + d * g, c * f + d * h] :=
by ext i j; fin_cases i; fin_cases j; simp [matrix.mul_apply]

Note that there was a typo (f and g swapped) in the first version. ext i j; fin_cases i; fin_cases j; is my algorithm for all matrix problems.

[Eric Wieser]

Maybe next week I'll make a matrix.of_mul_of lemma that uses tactics to generate the goal types for us

[Eric Wieser]

This was much more interesting than whatever I was supposed to be doing today: #15738. Using mul_fin from that PR:

example {α} [add_comm_monoid α] [has_mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
  !![a₁₁, a₁₂;
     a₂₁, a₂₂] ⬝ !![b₁₁, b₁₂;
                    b₂₁, b₂₂] = !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂;
                                   a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] :=
begin
  rw mul_fin,
end

example {α} [add_comm_monoid α] [has_mul α] (a₁₁ a₁₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
  !![a₁₁, a₁₂] ⬝ !![b₁₁, b₁₂;
                    b₂₁, b₂₂] = !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂;] :=
begin
  rw mul_fin,
end

[Kevin Buzzard]

Nice!

[Kevin Buzzard]

I guess there's not much we can do about the fact that the equation is diagonal :-)

[Eric Wieser]

I don't think the world is ready for the level of whitespace-sensitivity that would require

[Alex J. Best]

Should this really be a tactic though?

[Eric Wieser]

Alex J. Best said:

Should this really be a tactic though?

It's pretty useful to be able to use it in a rewrite chain

[Eric Wieser]

The design is based off docs#category_theory.reassoc_of

[Alex J. Best]

Eric Wieser said:

Alex J. Best said:

Should this really be a tactic though?

It's pretty useful to be able to use it in a rewrite chain

You could say the same about many tactics though

[Eric Wieser]

Kevin Buzzard said:

I guess there's not much we can do about the fact that the equation is diagonal :-)

You could invest in a rotatable screen:
image.png

[Alex J. Best]

And we could massage a lot of them into rewrite lemmas with this sort of technique right? Or is there some special form such auto params have to take?

[Alex J. Best]

Like can you make a rw norm_num in this way?

[Eric Wieser]

Ah, one downside of trying to be clever here is that mul_fin isn't allowed in simp or simp_rw

[Alex J. Best]

And what happens when library_search and such try to apply this lemma?

[Eric Wieser]

Library_search gives

Try this: refine mul_fin
  (id
     ((λ (_inst_1_1 : has_mul α) (_inst_2_1 : add_comm_monoid α)
       (b₀₀ b₀₁ b₁₀ b₁₁_1 a₀₀ a₀₁ a₁₀ a₁₁_1 : α),
         ((⇑of ![![a₀₀, a₀₁], ![a₁₀, a₁₁_1]]).mulᵣ_eq
            (⇑of ![![b₀₀, b₀₁], ![b₁₀, b₁₁_1]])).symm)
        _inst_2
        _inst_1
        b₁₁
        b₁₂
        b₂₁
        b₂₂
        a₁₁
        a₁₂
        a₂₁
        a₂₂))

[Eric Wieser]

I guess I should have been consistent about 0 or 1-based numbering of matrices

[Eric Wieser]

I think having some standard mechanism for generating lemmas templated by some arguments would be nice

[Alex J. Best]

Yeah the thing that bothers me is that these are generated each time they are used, which maybe isn't a huge problem (tactics are run each time too).

[Eric Wieser]

Maybe there's some way to cache the lemma for each value of (l, m, n)

[Eric Wieser]

I've updated the PR so that library_search now suggests

Try this: refine mul_fin
  (id (mul_fin_aux 2 2 2 a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂))