Linear Algebra Done Right, Complex mul_comm

Stream: general

[Martin C. Martin]

I'm translating the proofs in Linear Algebra Done Right into Lean. I'm looking for early feedback on example 1.4 that complex multiplication is commutative.
ComplexCommutative.jpg

import data.complex.basic

open complex

-- 1.4 Example "Show that αβ = βα for all α, β ∈ ℂ"
example {α β : ℂ} : α * β = β * α :=
  let ⟨a, b⟩ := α in
  let ⟨c, d⟩ := β in
  calc
    (complex.mk a b) * (complex.mk c d) = (a + b * I) * (c + d* I) : by rw [mk_eq_add_mul_I, mk_eq_add_mul_I]
        ... = (a * c - b * d) + (a * d + b * c) * I : by ext; simp
        ... = (c * a - d * b) + (c * b + d * a) * I : by ext; simp [mul_comm, add_comm]
        ... = (complex.mk c d) * (complex.mk a b) : by {ext; simp}

Is this the style that is expected? Any suggestions or improvements?

[Kyle Miller]

Here's a simpler proof :smile:

example {α β : ℂ} : α * β = β * α := mul_comm α β

Or

example {α β : ℂ} : α * β = β * α := by ring

What's the right sort of proof depends on what you're trying to do here. I guess one comment I'd give is that using let to destruct arguments like that isn't so common (and I'm not actually sure there's any guarantee there's any relationship between a, b, c, d and α, β in general.

[Kyle Miller]

If you want to compare to mathlib's proof, it's essentially

example {α β : ℂ} : α * β = β * α :=
begin
  ext,
  { simp,
    ring },
  { simp,
    ring }
end

or by ext; simp; ring for short. I extracted this from the commutative ring instance for the complex numbers https://github.com/leanprover-community/mathlib/blob/290a7ba01fbcab1b64757bdaa270d28f4dcede35/src/data/complex/basic.lean#L205

[Kyle Miller]

If you like your style with an explicit calculation, you can consider the following version, which handles destructuring in a way that should be more reliable

example {α β : ℂ} : α * β = β * α :=
begin
  obtain ⟨a, b⟩ := α,
  obtain ⟨c, d⟩ := β,
  calc
    (complex.mk a b) * (complex.mk c d) = (a + b * I) * (c + d* I) : by rw [mk_eq_add_mul_I, mk_eq_add_mul_I]
        ... = (a * c - b * d) + (a * d + b * c) * I : by ext; simp
        ... = (c * a - d * b) + (c * b + d * a) * I : by ext; simp [mul_comm, add_comm]
        ... = (complex.mk c d) * (complex.mk a b) : by {ext; simp}
end

[Martin C. Martin]

The goal is a good question. I'm trying to translate the proof in the book, which I put in the image, into Lean as directly as possible. The proof in the book is aimed at people who are rusty with manipulating complex numbers, and so explicitly writes out alpha as (a+bi), etc.

As I understand it, the goal of translating a textbook into Lean is to be a kind of Rosetta stone; for people who know the textbook but not Lean, it lets them see how something familiar can be translated into Lean.

If that's the goal, what's the write way to translate the snippet in the JPEG above?

[Kyle Miller]

I think the "right" translation, that shows how you'd normally prove this, is this proof:

example {α β : ℂ} : α * β = β * α :=
begin
  ext,
  { simp,
    ring },
  { simp,
    ring }
end

[Kyle Miller]

It's not exactly the same, but it has the same spirit. You have to step through it with an IDE to understand the proof though, but that's like most Lean proofs.

You could be more specific with which lemmas are being used by simp if you want (using squeeze_simp to obtain them).

[Kyle Miller]

The main difference is that the original proof says "to show two complex numbers are the same, we can represent everything in sight in rectangular coordinates and do some algebraic manipulations" and this one says "to show two complex numbers are the same, we can compare the real and imaginary parts separately"

[Kyle Miller]

Re rosetta's stone, it'd be nice to also have by ring or mul_comm α β, since that's pointing out how you'd make use of commutativity in practice.

[Kevin Buzzard]

For what it's worth, I define the complex numbers and prove that they are a ring in the first level of the complex number game here https://github.com/ImperialCollegeLondon/complex-number-game/blob/master/src/complex/Level_00_basic.lean

[Reid Barton]

If you want to use calc here then the right approach is to first prove an induction principle for complex saying that you can check things on complex numbers of the form a + b * I. Then use it twice to reduce to the middle part of your calculation.

[Martin C. Martin]

So it seems the preferred approach for a "Rosetta Stone" translation of a textbook, following Kevin's complex number game, as well as TPIL and MIL, is to define concepts we need, like complex number, vector, linear map, matrix, etc. The prove basic properties of them. Once that's done, we can retire our custom definitions and use the mathlib definitions. Sound good?

[Eric Wieser]

a "Rosetta Stone" translation of a textbook

I think there are two different interpretations of this; do you want a rosetta stone for proof strategies, or just for mathematical results?

[Eric Wieser]

The second approach would just be example {α β : ℂ} : α * β = β * α := mul_comm α β

[Martin C. Martin]

Eric Wieser said:

do you want a rosetta stone for proof strategies, or just for mathematical results?

This is really a question for this community. For context, I want to contribute something, and someday contribute to mathlib. As a first project, it was suggested that I translate Axler's book. So what would the community find most useful?

Personally, the second approach seems less useful. Just naming the existing result doesn't really show the reader how they might prove something that isn't already in mathlib. But I'll wait for others to chime in.

[Eric Wieser]

I've been using the second approach here as a means to spotting gaps in mathlib. But certainly that's not a real textbook, so a different approach for Axler is totally reasonable.

[Yakov Pechersky]

When faced with a choice between two valid approaches, why not choose both? You can show a calc style proof that doesn't rely on any instances on the complexes, and right below it, an example with an "idiomatic" proof relying on the comm_ring complex instance.

[Kevin Buzzard]

@Martin C. Martin "build then throw away" was my conclusion too. For example, I make the naturals in the natural number game, when making the integers from the naturals I switch to Lean's naturals because all the infrastructure is already there. You can see how long it takes to make infrastructure in lean: for example it takes ages to get a working theory of <= in the natural number game, and in the complex number game I have to spend a lot of time setting up extensionality lemmas, proving basic simp lemmas with refl etc. It takes a huge amount of time to make a robust object in lean and it's rather tedious, especially when many of the proofs are just refl and you have to make simp work. This is not really mathematics. So I definitely agree with you -- assume built in stuff, define new stuff yourself (groups are a great example, I make them in the group theory game) and then immediately throw them away in the next chapter and use Lean's inbuilt version.

[Kevin Buzzard]

I've made the naturals, integers, groups, filters, and the complexes all "from scratch" and in each case I mean "using lean's version of everything I need even if I've made it myself before"

[Kevin Buzzard]

You're welcome to use any of this stuff or be inspired by it and I don't need credit.

[Martin C. Martin]

Thanks @Kevin Buzzard . I'm trying something along those lines. I thought I'd give it a try without ext for a simple case, but I'm struggling with how to apply the definition of multiplication, or coercion, here:

structure complex : Type :=
(re : ℝ) (im : ℝ)

notation `ℂ` := complex

namespace complex

/-- The imaginary unit. -/
def I : ℂ := ⟨0, 1⟩

-- if a ∈ ℝ, we identify a + 0I with the real number a.
instance : has_coe ℝ ℂ := ⟨λ a, ⟨a, 0⟩⟩

-- instance : has_add ℂ := ⟨λ z w, ⟨z.re + w.re, z.im + w.im⟩⟩

def mul (z w : ℂ) : ℂ := ⟨z.re * w.re - z.im * w.im, z.re * w.im + z.im * w.re⟩
-- Notation '*' for multiplication.
instance : has_mul ℂ := ⟨mul⟩

@[simp] lemma I_mul_I : I * I = (-1 : ℝ) :=
begin
  cases I,
  cases I,
  sorry
end

I tried rw mul, simp and refl in place of sorry, but nothing works. How can I get it to rewrite using mul, and expand the coercion on the RHS?

[Ruben Van de Velde]

You can first add a lemma

lemma mul_def (z w : ℂ) : z * w = ⟨z.re * w.re - z.im * w.im, z.re * w.im + z.im * w.re⟩ := rfl

and then rw [mul_def] in I_mul_I

[Martin C. Martin]

Thanks! Although looking closer, cases I, isn't doing what I thought. I is replaced with {re := re, im := im}, I don't know where the 0 and 1 went.

[Eric Wieser]

You want rw I not cases I

[Eric Wieser]

cases h : I prevents lean forgetting the details too, but that's not very useful to you here

[Kevin Buzzard]

You saw that I have an entire sheet on I right? The reason simp isn't doing anything for you is because you have made a new structure now you have to train the simplifier on how to work with it. Hence the gazillion simp lemmas in the first sheet, all of which are imported in the second sheet where we deal with I

[Kevin Buzzard]

This is exactly why it's a PITA to make new mathematical objects from first principles -- simp won't work until you've made all the simp lemmas, ring won't work until you've proved all the ring axioms etc etc

[Kevin Buzzard]

You're working with I but I proved a gazillion boring things before I even started on I

[Martin C. Martin]

Thanks again @Kevin Buzzard . I was more wondering how to invoke the definition of a has_mul, I thought there might be some way to do it without having to have a parallel theorem like mul_def. I was hoping refl or dsimp would expand it, or maybe rw (*). I noticed in your complex numbers game, you define the function mul, although now that I look, you only ever use it in the definition of has_mul.

mathlib doesn't have a separate mul_def that it gives to the simplifier, but I think it just breaks everything into real and imaginary parts and goes from there. Which makes sense, it's a great way to leverage existing abilities on N, Z, and R.

[Eric Wieser]

dsimp [(*)] usually works

[Eric Wieser]

But that's rarely useful, since it unfolds all the multiplications, not just the one you wanted

[Kevin Buzzard]

I define mul and then I define has_mul and then I prove lots of API about *, which is the "canonical form" or "simp normal form" for mul.

[Martin C. Martin]

It's interesting that mathlib doesn't have mul_def, but instead separate theorems for the real and imaginary parts:

@[simp] lemma mul_re (z w : ℂ) : (z * w).re = z.re * w.re - z.im * w.im := rfl
@[simp] lemma mul_im (z w : ℂ) : (z * w).im = z.re * w.im + z.im * w.re := rfl

[Eric Wieser]

Mathlib has decreed that complex.mk is unmathematical, and therefore that basically no lemmas should exist about it

[Arien Malec]

Martin C. Martin said:

I'm translating the proofs in Linear Algebra Done Right into Lean. I'm looking for early feedback on example 1.4 that complex multiplication is commutative.
ComplexCommutative.jpg

import data.complex.basic

open complex

-- 1.4 Example "Show that αβ = βα for all α, β ∈ ℂ"
example {α β : ℂ} : α * β = β * α :=
  let ⟨a, b⟩ := α in
  let ⟨c, d⟩ := β in
  calc
    (complex.mk a b) * (complex.mk c d) = (a + b * I) * (c + d* I) : by rw [mk_eq_add_mul_I, mk_eq_add_mul_I]
        ... = (a * c - b * d) + (a * d + b * c) * I : by ext; simp
        ... = (c * a - d * b) + (c * b + d * a) * I : by ext; simp [mul_comm, add_comm]
        ... = (complex.mk c d) * (complex.mk a b) : by {ext; simp}

Is this the style that is expected? Any suggestions or improvements?

The proof that's wanted is that scalar multiplication on a vector space is commutative, right?

[Arien Malec]

I don't have the same edition, but in the edition I have the field axioms are taken for granted, and our interest is in proofs of the properties of vector spaces.

[Pedro Sánchez Terraf]

Arien Malec said:

The proof that's wanted is that scalar multiplication on a vector space is commutative, right?

It's actually the commutativity of complex multiplication

[Arien Malec]

I think 3rd ed goes a bit slower than 2nd ed :-) It's confusing, because it's also given as an axiom...

[Arien Malec]

I take that back -- in 2nd ed Axler has us use the definition of complex numbers of the reals to re-prove field axioms, so yeah, all of @Kevin Buzzard CNG.

Again, the basic pedagogical issue with recapitulating proofs in Mathlib is that it's hard to get just the axioms you want, without all the machinery that you need to prove. In addition, in Linear Algebra, rather than vector spaces over fields (which Axler uses to simplify) we need to build machinery for Modules & Submodules if we want to actually use Mathlib later on...

[Arien Malec]

Which I suspect is confusing for the intended audience....

[Arien Malec]

I suspect that building the machinery for even the first chapter ad hoc before replacing it with Mathlib is going to be a major chore, since we want modules & submodules & the fields they are defined over and sums and direct sums, each of which have a bunch of Mathlib machinery behind it....

[Kyle Miller]

A vision I have for a mathlib-formalized textbook is that you avoid all these issues by not defining anything from scratch. When something new is defined in the textbook, you explain how to write down that concept in Lean (potentially with some auxiliary definitions if the concept doesn't match up perfectly), and then for proofs you use pre-existing mathlib proofs as much as possible. The purpose of this exercise would be to show someone who already knows the math what the mathlib equivalent is.

[Scott Morrison]

cf #13911 (and perhaps someone could hit merge?)

[Arien Malec]

Every time I think about this, I'm impressed by how much work went into Mathlib in the first place, as well as how well done NNG and CNG are (thanks @Kevin Buzzard )...

[Arien Malec]

What's the basic Mathlib machinery for something like:

"Is the set of all vectors ${(x_1, x_2, x_3, x_4)} \in F^4 | x_1 + 2x_2 + 3x_4 = 0}$ a subspace of F^4"

[Kyle Miller]

I'd translate that into "is it true that there exists a subspace W of F^4 such that W = ... that set ...", where there's a coercion to Set here for W.

[Arien Malec]

Which I'd show by constructing a submodule and showing in the construction the three required proofs?

[Kyle Miller]

For this problem, I'd use the fact it's a kernel of a linear map, so no need for the three proofs.

[Kyle Miller]

But, yeah, you could also give a construction using the submodule constructor too.

[Arien Malec]

We haven't gotten to null spaces yet though :-)

[Yakov Pechersky]

Could you also skip to talking about span and ask whether coe (span S) = S?

[Arien Malec]

Span, linear independence, basis and dimension are all chapter 2.

[Martin C. Martin]

Kyle Miller said:

When something new is defined in the textbook, you explain how to write down that concept in Lean ..., and then for proofs you use pre-existing mathlib proofs as much as possible. The purpose of this exercise would be to show someone who already knows the math what the mathlib equivalent is.

By "use pre-existing mathlib proofs", do you mean just invoking the existing mathlib theorem, e.g. := mul_comm z w, or do you mean copying the mathlib proof into the formalized textbook, so they can see how these things are proven?

I can see it either way. The first way is a kind of index into mathlib theorems. The second way shows how to do proofs in this area.

[Martin C. Martin]

With has_coe ℝ ℂ and an @[simp] lemma, example : ( (5 : ℝ) : ℂ).re = 5 := by simp works just fine. But to get example : ( 5 : ℂ).re = 5 := by simp working, I need @[simp] lemma bit0_re (z : ℂ) : (bit0 z).re = bit0 z.re and similarly for bit1. What are these, and what do they have to do with coercing ℕ to ℂ? Also, presumably there's already a coercion from ℕ to ℝ, I guess Lean/mathlib doesn't automatically compose that with my shiny new has_coe ℝ ℂ to make my example work, without the bit0/1 stuff?

[Ruben Van de Velde]

The bit things are how numerals are represented in lean 3: 5 is bit1 bit0 bit0 (if I counted right)

[Martin C. Martin]

And those are not enough to get, example {n : ℕ} : (n : ℂ).re = n := sorry working.

[Kevin Buzzard]

Kyle Miller said:

A vision I have for a mathlib-formalized textbook is that you avoid all these issues by not defining anything from scratch.

That's another route I've experimented with. In my Lean UG course last year I defined e.g. groups and subgroups by rolling my own. But this year I decided to just use Lean's definitions for most things. The course material became a lot more "overviewy" as a result, for example the last three lectures here here and here just ended up being overviews of algebraic number theory, representation theory and Galois theory in mathlib with essentially no proofs at all.