the complex number game

Stream: new members

[Kevin Buzzard]

Have you done the natural number game? Can you prove complex conjugation is a ring homomorphism?

Link to Lean web editor (takes a long time to load, honestly I'd leave it on "lean is busy" for at least 1 minute before concluding something is wrong):

https://tinyurl.com/thecomplexnumbergame

Source (cut and paste this into any Lean project which uses mathlib and you won't have to wait 1 minute)

Solutions

This is part of a book I'm writing with Jeremy, Rob and Patrick. All comments from mathematicians welcome!

[Aniruddh Agarwal]

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

Is the code above roughly equivalent to the Haskell:

 data Complex = C Real Real

[Patrick Stevens]

Aniruddh Agarwal said:

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

Is the code above roughly equivalent to the Haskell:

 data Complex = C Real Real

Basically, but the fields are named in Lean whereas you haven't named them in the Haskell.

[Kevin Buzzard]

I'm trying to work out a path to building a basic mathematical API for the complexes in a way that a mathematician can understand easily. I've got something which I think works ok and I'll be live streaming a walkthrough of a basic complex number game on twitch tomorrow Thursday 21st 5pm UK time.

[Jalex Stark]

(If you "follow" kevin at https://www.twitch.tv/kbuzzard, you'll get an email when he goes live)

[Johan Commelin]

walkthrough or speedrun?

[Kevin Buzzard]

Walkthrough

[Kevin Buzzard]

Basically I have got what I think is a really nice proof that C is a ring which hopefully will convince people that lean is easy

[Kevin Buzzard]

And by the time they're using it and realise that it's hard, it's too late they're hooked

[Kenny Lau]

what, by ring?

[Kevin Buzzard]

It's my_complex

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/complex-number-game

[Patrick Massot]

Do you want this to be added to https://leanprover-community.github.io/learn.html or is this a transient thing waiting to be integrated to MIL?

[Patrick Massot]

Yes you'd like this to be added, then you simply need to click the edit button at https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/learn.md to open a PR

[Kevin Buzzard]

This was just a gimmick. I am happy to use it any way you think is best.

[Filippo A. E. Nuccio]

I can't understand the lines

def Conj : ℂ →+* ℂ := { to_fun := conj, map_one' := begin ext; simp, end, map_mul' := begin intros, ext; simp end, map_zero' := begin ext; simp end, map_add' := begin intros, ext; simp end}

in the Complex Numbers Game,

[Kevin Buzzard]

Did you understand the question? That looks like the solution

[Filippo A. E. Nuccio]

No, indeed (as you said yesterday), I guess I don't know what an equivalence relation is.

[Filippo A. E. Nuccio]

I understand that conj could take (x,y) and send it to (x,-y)

[Kevin Buzzard]

The question is probably the same as the solution except that between each begin end block there is a sorry

[Filippo A. E. Nuccio]

and solved all the exercises related to conj.

[Kevin Buzzard]

and if you click on the sorry you will see the goal which Lean wants you to prove.

[Filippo A. E. Nuccio]

I suspect I don't know what it means to " define a function" (more than specifying where it should send every element of the domain)

[Kevin Buzzard]

I don't know what you are talking about. What function?

[Kevin Buzzard]

This is the question:

/-- the ring homomorphism complex conjugation -/
def Conj : ℂ →+* ℂ :=
{ to_fun := conj,
  map_zero' := begin sorry end,
  map_one' := begin sorry end,
  map_add' := begin sorry end,
  map_mul' := begin sorry end
}

[Kevin Buzzard]

I have done the hard work (the computer science stuff).

[Filippo A. E. Nuccio]

you begin with
def Conj : C->+* C :=

[Kevin Buzzard]

Yes but you don't need to worry about all that part

[Kevin Buzzard]

Sorry, what is your question?

[Kevin Buzzard]

Did you manage to fill in the sorrys yourself?

[Filippo A. E. Nuccio]

Indeed, I haven't realised I could click on the sorry to understand what Lean wanted from me

[Filippo A. E. Nuccio]

I agree that now everything looks trivial (or at the same level of previous exercices), so no problem. An thanks.

[Filippo A. E. Nuccio]

But still one small point eludes me:

[Kevin Buzzard]

OK so the question for mathematicians is supposed to be the following: "replace each sorry with a tactic proof. You can see what the goal is in each case by clicking on the sorry"

[Filippo A. E. Nuccio]

What is the point of these lines? I gather that it is to state the lemma "the set-theoretic map conj is actually a ring homomoprhism", is that right?

[Kevin Buzzard]

I only released the game yesterday and I didn't try it out on some select group of people or anything -- I am sure that there will be plenty of things that need to be clarified.

[Kevin Buzzard]

Yes, so that's the other question we have here.

[Kevin Buzzard]

You might know that to define a complex number z in Lean we could do something like { re := 3, im := 4}

[Filippo A. E. Nuccio]

Yes

[Kevin Buzzard]

Well, to define a ring homomorphism from $\mathbb{C}$ to $\mathbb{C}$ it's the same kind of story

[Kevin Buzzard]

We need to give Lean a map, and four proofs

[Filippo A. E. Nuccio]

I believe that my problem is that those lines begin with def rather than lemma

[Kevin Buzzard]

def z := { re := 3, im := 4} also has a def

[Kevin Buzzard]

as does def conj (z : ℂ) : ℂ := sorry

[Kevin Buzzard]

If you are defining things, you use def or definition. If you are proving theorems you use theorem or lemma

[Filippo A. E. Nuccio]

This line (435 in the code) is OK with me: it defines a function taking a complex number to another complex number.

[Kevin Buzzard]

We are defining the ring homomorphism, and part of the definition is the underlying function. We are not proving that a function is a ring homomorphism, we are defining a ring homomorphism to be a collection of data, most of which is proofs, but not all of it, so we use def

[Filippo A. E. Nuccio]

What puzzles me are the line where you check it is a ring hom: they begin with
def Conj : ℂ →+* ℂ :=

[Kevin Buzzard]

I am defining a second thing

[Kevin Buzzard]

conj is the function, Conj is the ring homomorphism

[Filippo A. E. Nuccio]

(the invisible map again is in the background, I suspect)

[Kevin Buzzard]

There's an invisible map from ring homs to functions, and it will send Conj to conj.

[Kevin Buzzard]

Conj is a variable that contains a lot of data, including conj

[Filippo A. E. Nuccio]

Ahah! Clear: so, I am correct in saying that
1) the to_fun line says that the underlying function to Conj is conj
2) the ->+* is telling Lean that we are going to define a ring hom
3) the map_one' until map_add' are the axioms a ring hom must satisfy (because we told him already that a ring hom is by definition something which satisfies them)

[Kevin Buzzard]

Mathematicians think that Conj and conj are equal, because to a mathematician the "object" is just the function, and the proofs of the axioms are not things you can make with sets -- the proofs live in some other part of the story.

In Lean, proofs are objects, just like functions are, so you can make objects which package together functions and proofs. conj has no packaging -- it's just the function. Conj is the package: the function, and the proofs, all in one object. In type theory, proofs are no different to numbers -- they are just terms, which can be packaged together.

[Filippo A. E. Nuccio]

Wonderful, it does make sense. In particular, I guess that before a mathematician (or myself, at least) can do something cool with Lean, this part of the story needs to be fully digested.

[Filippo A. E. Nuccio]

But it seems very edible.

[Kevin Buzzard]

Do you have leanproject installed @Filippo A. E. Nuccio ? If you do then there is now a much easier way to play the complex number game: you can just download and compile the repository with leanproject get ImperialCollegeLondon/complex-number-game

[Filippo A. E. Nuccio]

Yes, I have already done so.

[Kevin Buzzard]

and then you can solve the levels individually in VS Code

[Filippo A. E. Nuccio]

I am playing on my pc, actually

[Kevin Buzzard]

I asked because you mentioned line 435

[Kevin Buzzard]

but I have pulled everything off into individual chapters now, in their own files, e.g. https://github.com/ImperialCollegeLondon/complex-number-game/blob/master/src/complex/conj.lean

[Filippo A. E. Nuccio]

That was from the github page, because I feared I could not make myself clear.

[Kevin Buzzard]

I don't think any file in the github repo I'm talking about has as many as 435 lines.

[Filippo A. E. Nuccio]

https://github.com/kbuzzard/xena/blob/master/Mathematics_In_Lean_ideas/complex_solns.lean

[Kevin Buzzard]

Right. What I'm trying to say is that I have made a more sophisticated version of this game now

[Filippo A. E. Nuccio]

Now I got it, thanks; sorry for not grasping it more quickly.

[Kevin Buzzard]

https://www.twitch.tv/videos/627659597 if you want to see me playing through the tutorial level

[Filippo A. E. Nuccio]

I attended it live, actually .

[Kevin Buzzard]

and on Thursday 21st I'll be solving I and conj live

[Filippo A. E. Nuccio]

You mean that yesterday you'll be solving them?

[Kevin Buzzard]

oops Thursday 28th :-)

[Patrick Massot]

Kevin, that's what you get for encouraging people to be rigorous

[Filippo A. E. Nuccio]

I hope to be done with the full proof that C is a field by next week, as I would like to move towards factorizing ideals as products of primes in Dedekind domains.

[Filippo A. E. Nuccio]

Thank you for your help, in the meantime.

[Kevin Buzzard]

I don't give any hints for this, and it's slightly tricky to get started. You should be warned that Lean's axioms for a field are not what we usually teach!

[Kevin Buzzard]

Check this out: a field is a nonzero commutative ring equipped with a map inv : K -> K satisfying inv(0)=0, and x*inv(x)=1 if x isn't 0

[Kevin Buzzard]

I'm sure you can see that this is trivially equivalent to what we think a field is

[Filippo A. E. Nuccio]

Sure

[Kevin Buzzard]

But they like their functions to be defined everywhere for technical reasons to do with implementation issues

[Kevin Buzzard]

Note that a/b is defined to be a*inv(b), so in particular 1/0=0

[Filippo A. E. Nuccio]

(are "they" computer scientists?)

[Kevin Buzzard]

This means that you can define inv(z) to be {re := re(z)/norm_sq(z), im := -im(z)/norm_sq(z)}

[Filippo A. E. Nuccio]

Sure, this makes sense.

[Kevin Buzzard]

and if z=0 this will give you 0, which is what the CS people want

[Filippo A. E. Nuccio]

Great. It all makes sense, and also explains why norms come before it being a field.

[Patrick Massot]

Filippo A. E. Nuccio said:

I hope to be done with the full proof that C is a field by next week, as I would like to move towards factorizing ideals as products of primes in Dedekind domains.

I love that sentence.

[Patrick Massot]

I wish our students could be that ambitious.

[Kevin Buzzard]

I intentionally put the proof it was a ring before the definition of $i$, because as a mathematician I feel like $i$ is the first thing you want to define, and I thought it really interesting that you can prove $\mathbb{C}$ is a ring without ever mentioning it explicitly.

[Patrick Massot]

And I also wish people could stop teaching set theory bullshit to our students. I'm marking exams and I just saw. Let's fix $(f, g) \in \left(\mathbb R^{\mathbb R}\right)^2$ instead of $f, g : \mathbb R \to \mathbb R$...

[Kevin Buzzard]

It's defeq Patrick so you can't take a mark off

[Filippo A. E. Nuccio]

That's terrifying, though...

[Kevin Buzzard]

That's the French for you

[Patrick Massot]

And those are my students who used Lean for 12 weeks...

[Filippo A. E. Nuccio]

Patrick Massot said:

And those are my students who used Lean for 12 weeks...

BTW: I might ask you hints on how to teach Lean to my students as well, also in France (Saint-Étienne), but this will come later. I might need to first lea(r)n it myself.

[Patrick Massot]

Did you do the tutorials based on my course?

[Filippo A. E. Nuccio]

Some of them, yes. Almost all of them, actually.

[Patrick Massot]

You can also get the French version on my web page (together with the lecture notes and tactic cheat sheet).

[Kevin Buzzard]

@Filippo A. E. Nuccio I just pushed solutions to field.lean in the complex number game repo

[Filippo A. E. Nuccio]

Thanks to both of you!

[Patrick Massot]

Actually if you are interested in the French version then I'll do some cleanup. Because I wrote files each week there are some inefficiencies in the libraries. There are also things that are now fixed in Lean and mathlib (I used a version of mathlib frozen in early January so that Lean and mathlib could be installed in our computer labs and on student's computers).

[Mario Carneiro]

Patrick Massot said:

And I also wish people could stop teaching set theory bullshit to our students. I'm marking exams and I just saw. Let's fix $(f, g) \in \left(\mathbb R^{\mathbb R}\right)^2$ instead of $f, g : \mathbb R \to \mathbb R$...

Yes, the type theory minded students can write the much clearer "Let's fix $(f,g):(\mathbb{R}\to\mathbb{R})\times(\mathbb{R}\to\mathbb{R})$"...

[Mario Carneiro]

or $(f,g):2\to\mathbb{R}\to\mathbb{R}$ in some conventions

[Patrick Massot]

I think you first suggestion is much clearer than what I wrote. The second one however...

[Sam Lichtenstein]

I have a basic question about basic.lean in the CNG (sorry to coopt someone else's thread) -- when proving something is an instance, like in the example:

instance : comm_ring ℂ :=
begin
  -- first the data
  refine_struct {
      zero := (0 : ℂ), add := (+), neg := has_neg.neg, one := 1, mul := (*),
  ..};
 sorry,

I am curious how to get Lean to "autocomplete" the set of data that needs to be provided in refine_struct { ... } . (By autocomplete, I don't mean that it will fill the data itself, just the list of fields that need to be defined, i.e. zero, add, neg, one, mul in this example.) I have a vague recollection reading somewhere on Zulip that there is some magic thing one can type that causes a little light bulb to show up. Is that the case, and what is the magic?

[Alex J. Best]

It's {! !}, which you can ask to fill in the skeleton for the structure under construction.

[Sam Lichtenstein]

ah great, I knew there was a ! involved, but didn't remember that you need two of them
thanks!

[Alex J. Best]

I'm not sure it works in tactic mode though.
So you'd need to do instance : comm_ring ℂ :={! !} to generate the structure first, then move into refine_struct if you prefer.

[Sam Lichtenstein]

are there keybindings, or does one need to use the mouse to hover over the bulb and select from the dropdown? (I am using VSCode not emacs)

[Gabriel Ebner]

ctrl+.

[Sam Lichtenstein]

Gabriel, if I am between the {! and the !} and I type CTRL + "." (which I think is what you meant?), nothing seems to happen

[Sam Lichtenstein]

is it supposed to?

[Patrick Massot]

Yes

[Patrick Massot]

And I think it should work wherever Lean wants a term, so inside refine_struct should be ok

[Sam Lichtenstein]

ah, duh it's CMD+. on a mac

[Sam Lichtenstein]

but does not work in refine_struct{}

[Mario Carneiro]

I think you have to write refine_struct {! !}

[Alex J. Best]

Didn't seem to work after refine struct for me

[Sam Lichtenstein]

"no code actions available"

[Bryan Gin-ge Chen]

Hah, this seems to work:

import data.complex.basic

instance a : comm_ring ℂ :=
begin
  -- first the data
  refine_struct by exact {! !};
 sorry,
end

[Jalex Stark]

I didn't know about {!!} until now. suggest is pretty good at filling the same purpose (and if there are lemmas around letting you construct with fewer arguments, suggest can find some of those too)

[Patrick Lutz]

I noticed that in the official solutions to the complex number game (which @Kevin Buzzard said were basically taken directly from mathlib) sometimes simp is used on a nonterminal line of a proof. For instance:

@[simp] lemma conj_add (z w : ℂ) : conj (z + w) = conj z + conj w :=
by ext; -- check on real and imag parts
   simp; -- question becomes to check that a+b=b+a for certain real numbers a and b
   ring -- true because this is obvious in a ring

Is this considered bad style, or is there a reason it's okay to do here?

[Mario Carneiro]

simp, ring is a whitelisted combination

[Mario Carneiro]

because it is mostly insensitive to additional simp rules

[Patrick Lutz]

wouldn't there still be a problem if simp became good enough to finish the proof on its own? You're not allowed to have additional lines after the goals have been accomplished right?

[Mario Carneiro]

Indeed, simp; ring is better than simp, ring for this reason

[Patrick Lutz]

what's the difference between , and ; exactly?

[Mario Carneiro]

tac1;tac2 calls tac1 and then calls tac2 on all goals produced by tac1

[Alex J. Best]

, will do one tactic after the other, ; will run the second tactic on all the goals produced by the first (so if there are none it gracefully does nothing)

[Patrick Lutz]

Okay, I think I had missed that aspect of it

[Patrick Lutz]

Thanks

[Alex J. Best]

If you have an iff statement you might use split; intro for example.

[Reid Barton]

If a proof breaks because it tries to invoke ring when there are no goals, it's usually pretty obvious how to fix it.

[Kevin Buzzard]

I used simp; linarith today and felt like I could get away with it for the same sort of reason

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Filippo A. E. Nuccio I just pushed solutions to field.lean in the complex number game repo

I have finished playing with everything you proposed before proving that $\mathbb{C}$ is a field, and I am now trying to attack this. I realise I am stuck with inv, already, because I can't tell Lean how to distinguish between 0 and non-zero complex numbers. I have tried to copy from the proof that $\mathbb{Q}$ is a field, unfortunately with no success. In the link I had, I cannot really see your solutions, have you uploaded them or are you still beneath your pile of copies to be marked?

[Alex J. Best]

They are at https://github.com/ImperialCollegeLondon/complex-number-game/tree/master/kb_solutions

[Filippo A. E. Nuccio]

Ahah! Thanks, I had the wrong adress.

[Kevin Buzzard]

Sorry, my solutions are currently in flux because last Thursday I embarked upon a major refactor. What is going on here is that in src there are incomplete solutions to the current (re-ordered) state of the game, and Alex' link is to far more complete solutions to the older version of the game, which is basically exactly the same theorems but in a different order. Hope you can untangle things from these hints! To give an example of the difference: I moved the "coercion from R to C" level from level 4 to level 1, because it was quite boring and the sooner you do it the less you have to do; as a result any theorems about e.g. coercions and conjugation used to be in the coersions level and are now in the conjugation level (you need to have both the coercion and conjugation to formalise the statement, and because the order of the levels swapped, the level which the lemma appears in changes).

[Kevin Buzzard]

@Filippo A. E. Nuccio

[Filippo A. E. Nuccio]

Yes, thanks, I realised this. But it is OK, I could make my way through the solutions. I am now trying to digest your def's of inv and on how to prove that $\mathbb{C}$ is a field.

[Kevin Buzzard]

So what is going on here is that if z isn't 0 then my definition is mathematically correct, and if z=0 then the inverse is 0 because I am dividing by 0 and x/0=0. The key thing which is not obvious is that in Lean the axioms for a field contain this "inverse" map which is a map from K to K, defined by inv(0)=0 and then for non-zero z there's an axiom z*inv(z)=1. So it's just the same as a usual field but they totalised the inverse function, because total functions are easier to work with.

[Jalex Stark]

Filippo, do you know about tactic#by_cases? Maybe by_cases z = 0 is useful for the things you're working on

[Filippo A. E. Nuccio]

Well, but in the definition
noncomputable def inv (z : ℂ) : ℂ := ⟨re(z)/norm_sq(z), -im(z)/norm_sq(z)⟩
where is it hidden that $z \ne 0$? Because although I can understand that you can insist $\mathrm{inv}(0)=0$ and set $z^{-1}=\mathrm{inv}(z)$, so that $0^{-1}=0$, the above definition involves dividing $0=\mathrm{re}(0)$ by $\mathrm{norm}\_\mathrm{sq}(0)$ as real numbers, no?

[Kenny Lau]

it isn't?

[Filippo A. E. Nuccio]

?

[Kenny Lau]

if z=0 then inv 0 = \< re 0 / norm_sq 0, -im 0 / norm_sq 0 \> = \< 0 / 0, 0 / 0 \> = \< 0, 0 \> = 0

[Kenny Lau]

where 0 / 0 = 0 * 0\-1 = 0 * 0 = 0

[Filippo A. E. Nuccio]

Ah, so you are saying that it has already been declared that also in $\mathbb{R}$ we have $a/0=0$ for all $a\in\mathbb{R}$ and therefore the definition makes sense for all $z\in\mathbb{C}$?

[Kenny Lau]

yep

[Filippo A. E. Nuccio]

Great! Thanks.

[Johan Commelin]

It's a field "axiom"

[Filippo A. E. Nuccio]

Ah, perfect. And we're applying it to the reals to deduce it for the complexes

[Kevin Buzzard]

Filippo A. E. Nuccio said:

Ah, so you are saying that it has already been declared that also in $\mathbb{R}$ we have $a/0=0$ for all $a\in\mathbb{R}$ and therefore the definition makes sense for all $z\in\mathbb{C}$?

"In Lean the axioms for a field contain this "inverse" map which is a map from K to K, defined by inv(0)=0 and then ...", and the reals are already a field because I imported data.real.basic which shows this.

[Filippo A. E. Nuccio]

Great, I was stupidly thinking that the "field" in the sentence was $\mathbb{C}$, whereas it was both $\mathbb{R}$ and $\mathbb{C}$...

[Jalex Stark]

0\inv = 0 is true not just in R or C, it's true in any field, where a field is the sort of thing talked about on this page: https://en.wikipedia.org/wiki/Field_(mathematics)

[Yury G. Kudryashov]

More precisely: mathlib formalizes fields and division rings so that 0⁻¹=0. In math it is usually undefined.

[ROCKY KAMEN-RUBIO]

From the most recent version, it looks like local attribute [simp] ext_iff is on line 58 of Kevin's solution to level 01, but not in either of the user solution files. It's not obvious to me that I would need to add this, and makes some of his solutions break if you keep the given files structure. Was there thing I missed that mentioned having to add this yourself?

[Kevin Buzzard]

I am in two minds about whether this is a good idea

[Kevin Buzzard]

If you make it a simp lemma then some low level proofs are easier but people seemed to think that it was not a good global simp lemma

[Kevin Buzzard]

Someone suggested that it was obfuscating the proofs

[Kevin Buzzard]

It was also making trivial proofs shorter

[Kevin Buzzard]

So either add it, or do ext; simp instead of simp

[ROCKY KAMEN-RUBIO]

oh ok, the earlier comments about this make more sense now.

[Kevin Buzzard]

Extensionality is the principle that two things are equal if they're made from the same parts. The extensionality tactic can be used to replace a goal that two things are equal by goals saying the parts are equal. complex.ext is tagged with @[ext] to make the extensionality tactic use this lemma. But it only goes one way. If you have a hypothesis that two complex numbers are equal and you want to deduce that their real and imaginary parts are equal I don't think you can use the ext tactic, so that's why ext_iff is useful. I realised I was using it a lot though so I wanted to teach it to simp.

[Mario Carneiro]

If you have that two complex numbers are equal and want to know their real parts are equal, use congr