Matrix equality by extensionality

Stream: new members

[Yakov Pechersky]

I am learning the mathlib syntax for matrices. The long-term goal is to show that the dimension of matrix n n \R is n^2. On the way, I am playing around with different matrix definitions. Currently, I can't show that two matrices are identical. What's the right way to do it? Errors are included:

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

universe u

-- we specialize matrix for n × n matrices
-- with a reducible definition because it's just a shell defn
@[reducible] def Mn (α : Type u) (n : ℕ) := matrix (fin n) (fin n) α
-- we infer the has_one instance to be able to use numerals instead
instance Mn_has_one (α : Type u) [has_zero α] [has_one α] (n : ℕ) :
    has_one (Mn α n) := infer_instance

-- and a shortcut for Mn(ℝ)
@[reducible] def MnR (n : ℕ) := Mn ℝ n
-- with a has_one instance to use numerals
instance MnR_has_one (n : ℕ) : has_one (MnR n) := infer_instance

example : (2 : MnR 2) = ![![2,0],![0,2]] :=
begin
    ext i j,
    cases i,
    cases j,
    cases i_val with i,
    cases j_val with j,
        refl, -- 0,0 case
        simp, -- 0,1 case, now have to show that it is actually 0,1
        have : j = 0,
            apply le_antisymm,
            have : j.succ <= 1,
                by linarith,
            rwa nat.succ_le_succ_iff at this,
            exact nat.zero_le j,
        have : j.succ = 1, by simp [this],
        -- goal is now: 2 ⟨0, _⟩ ⟨j.succ, j_is_lt⟩ = 0
        rw this,
        -- error is rewrite tactic failed, motive is not type correct
        -- λ (_a : ℕ), 2 ⟨0, _⟩ ⟨j.succ, j_is_lt⟩ = 0 = (2 ⟨0, _⟩ ⟨_a, j_is_lt⟩ = 0)
end

[Scott Morrison]

First note that neither of your instances do anything. Since you made the definitions reducible, Lean can find the instances directly.

[Scott Morrison]

(anytime you create an instance just by infer_instance or apply_instance, without any dsimp first, you know that it wasn't necessary)

[Scott Morrison]

(similarly if you're proving a @[simp] lemma merely with by simp, it likely isn't necessary)

[Scott Morrison]

I would suggest that a canonical start to this proof should be

begin
  ext x y,
  fin_cases x; fin_cases y; dsimp,
end

and if you're not done by then (you're not!) then there are some missing @[simp] lemmas that should be written.

[Yakov Pechersky]

Awesome, good to know. So I will remove those instances. Originally, I did not have reducible, and couldn't get the infer_instance to work. Reading some of the source code suggested to try reducible, so that made it work. Didn't realize that the instances came with reducible.

[Yakov Pechersky]

Ah, fin_cases! Did not know about that, none of the tutorials worked with it. Still learning all the tactic tricks.

[Scott Morrison]

The alternative to @[reducible] would be to construct those instances using by { dsimp [Mn], apply_instance }.

[Scott Morrison]

Or you can write @[derive has_one] before the def Mn ..., which just uses this trick under the hood.

[Yakov Pechersky]

Your hint, if I understand correctly, is to show that for 2 : MnR 2, the off-diagonal entries are 0, by calling on an underlying matrix lemma about the definition of one for a matrix. Correct?

[Scott Morrison]

You might like these lemmas:

universes v

@[simp] lemma matrix.bit0_apply_apply
   (n : Type u) [fintype n] (α : Type v) [has_add α] (M : matrix n n α) (i : n) (j : n) :
  (bit0 M) i j = bit0 (M i j) := rfl

@[simp] lemma matrix.bit1_apply_apply
   (n : Type u) [fintype n] [decidable_eq n] (α : Type v) [semiring α] (M : matrix n n α) (i : n) (j : n) :
  (bit1 M) i j = if i = j then bit1 (M i j) else bit0 (M i j) :=
begin
  dsimp [bit1, matrix.one_val],
  split_ifs; simp,
end

[Scott Morrison]

(It's arguable whether they should actually be simp lemmas, but I think probably yes.)

[Scott Morrison]

With them you can use:

example : (2 : MnR 2) = ![![2,0],![0,2]] :=
begin
  ext x y,
  fin_cases x; fin_cases y; simp [matrix.one_val],
end

[Scott Morrison]

Perhaps matrix.one_val should be a simp lemma, too.

[Scott Morrison]

Ask if you've got no idea what bit0 and bit1 are about! They are how to encode numerals.

[Scott Morrison]

Typically whenever you decide you want to use numerals for some new type, you need to set up some lemmas describing "their inner workings".

[Scott Morrison]

It seems no one did this for matrices, perhaps.

[Yakov Pechersky]

I've seen bit0 and bit1 only in the tutorials, but only briefly.

[Scott Morrison]

If you like you can PR these lemmas to mathlib. :-)

[Yakov Pechersky]

I was going to say "Your lemmas are probably generalizable to arbitrary m x n matrices, not necessarily square...." but then I realized that (bit0 M) would not make sense for a rectangular matrix.

[Yakov Pechersky]

I mean, there are identity-like matrices for rectangular ones, but those are probably not what people want.

[Yakov Pechersky]

Why do you not need [decidable_eq n] for the bit0 lemma?

[Yakov Pechersky]

Ah, the i = j in the ite statement.

[Yakov Pechersky]

If those lemmas were not defined, would the scalar-multiplication lemma to show 2 : MnR n is diagonal also work, for the off-diagonal elements?

[Scott Morrison]

I'm not sure what you mean by the last comment.

[Yakov Pechersky]

I was stuck at the step that had to show (2 : MnR) 0 1 = ![![2,0],![0,2]] 0 1. simp is able to get the rhs down to 0. The lhs was not simplifying at all. I thought your earlier hint was to show that 2 = 2 * 1 and have a lemma that forall s, s * (diagonal d) = (diagonal (\la i, s * d i)). Then, we have that 2 : MnR 2 is also diagonal, so the off-diagonal entries are 0.

[Scott Morrison]

That would be another approach, but I think it's easier to just write simp lemmas for the matrix entries of numerals. Otherwise people are going to have to do this scalar-multiplication-times-one trick themselves every time.

[Yakov Pechersky]

OK, makes sense to me. Any tips on PRs for mathlib?

[Scott Morrison]

There's some basic advice at https://leanprover-community.github.io/contribute/index.html about making a PR.

[Scott Morrison]

The essential points are:

1. make a fork of mathlib on github
2. make a branch locally that contains just your changes
3. push this to your fork on github
4. click the "pull request" button

[Scott Morrison]

We can walk you through the rest of it.

[Scott Morrison]

It's nice if you try to put a title on the PR that matches our conventions, and similarly if you try to read the "naming" page accessible from that link, to try to get the names of declarations in mathlib style.

[Scott Morrison]

But those can all be fixed in the PR comments. We try to be nice to people on their first PR. :-)

[Scott Morrison]

It also helps if you run #lint at the bottom of any file you're going to include, and try to fix any problems it reports. (Or ask here if you don't know what it wants.)

[Yakov Pechersky]

Cool, I'll try that out. When cloning mathlib locally, is it worth it to do leanproject build? The times I've done it after doing leanproject get tutorials, for example, it's ruined my folder for live coding in VS code, I just get lots of errors.

[Scott Morrison]

Definitely don't run leanproject build. That will compile everything, and you'd really prefer someone else does that work.

[Scott Morrison]

leanproject up will simultaneously get the latest version of mathlib, and download precompiled olean files for you.

[Bryan Gin-ge Chen]

If you're cloning mathlib, you can use leanproject get-cache to fetch the oleans for any branch that's in the mathlib repo. You can run leanproject build if you want to check locally that your changes don't break other parts of the library, but most of us rely on the Github Actions scripts which build mathlib "in the cloud". As recommended in the "how to contribute" page that Scott linked, you should make sure that Github Actions is enabled for your fork of mathlib as well.

[Yakov Pechersky]

In files like data.matrix.basic, where it seems the lemmas should go, set variables local to a namespace. In addition, in that namespace, instances for those variables are assumed. At a given line in the file, is there a way to see what instances are associated with a variable, with something like a #check? That way the lemma definitions can be placed in the most appropriate namespace. For example, namespace one is not appropriate because it assumes too much about \a, but namespace diagonal seems appropriate because of [decidable_eq n].

I didn't notice the instances for the variables at first, and after pasting the lemmas into the namespace one section, was surprised to see errors.

[Johan Commelin]

@Yakov Pechersky you can try #where

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib/pull/2987

[Johan Commelin]

@Yakov Pechersky Thanks, I've kicked it on the merge queue