Zulip Chat Archive

Stream: new members

Topic: Matrix equality by extensionality


view this post on Zulip Yakov Pechersky (Jun 08 2020 at 04:52):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:03):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:03):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:03):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:06):

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.

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:07):

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.

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:08):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:11):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:12):

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

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:15):

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?

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:22):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:22):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:23):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:23):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:24):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:24):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:24):

It seems no one did this for matrices, perhaps.

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:24):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:24):

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

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:26):

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.

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:26):

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

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:27):

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

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:28):

Ah, the i = j in the ite statement.

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:32):

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?

view this post on Zulip Scott Morrison (Jun 08 2020 at 05:32):

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

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 05:35):

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.

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:10):

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.

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 06:18):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:26):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:27):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:27):

We can walk you through the rest of it.

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:28):

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.

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:28):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:28):

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.)

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 06:36):

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.

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:43):

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

view this post on Zulip Scott Morrison (Jun 08 2020 at 06:44):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 08 2020 at 06:45):

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.

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 07:15):

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.

view this post on Zulip Johan Commelin (Jun 08 2020 at 07:20):

@Yakov Pechersky you can try #where

view this post on Zulip Yakov Pechersky (Jun 08 2020 at 15:32):

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

view this post on Zulip Johan Commelin (Jun 08 2020 at 16:40):

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


Last updated: May 14 2021 at 22:15 UTC