Zulip Chat Archive

Stream: new members

Topic: the complex number game


view this post on Zulip Kevin Buzzard (May 10 2020 at 12:08):

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!

view this post on Zulip Aniruddh Agarwal (May 10 2020 at 12:23):

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

Is the code above roughly equivalent to the Haskell:

 data Complex = C Real Real

view this post on Zulip Patrick Stevens (May 10 2020 at 12:34):

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.

view this post on Zulip Kevin Buzzard (May 20 2020 at 21:32):

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.

view this post on Zulip Jalex Stark (May 21 2020 at 00:10):

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

view this post on Zulip Johan Commelin (May 21 2020 at 03:53):

walkthrough or speedrun?

view this post on Zulip Kevin Buzzard (May 21 2020 at 07:18):

Walkthrough

view this post on Zulip Kevin Buzzard (May 21 2020 at 07:18):

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

view this post on Zulip Kevin Buzzard (May 21 2020 at 07:19):

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

view this post on Zulip Kenny Lau (May 21 2020 at 07:20):

what, by ring?

view this post on Zulip Kevin Buzzard (May 21 2020 at 07:21):

It's my_complex

view this post on Zulip Kevin Buzzard (May 21 2020 at 15:50):

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

view this post on Zulip Patrick Massot (May 21 2020 at 15:53):

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?

view this post on Zulip Patrick Massot (May 21 2020 at 15:54):

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

view this post on Zulip Kevin Buzzard (May 21 2020 at 17:14):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:11):

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,

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:12):

Did you understand the question? That looks like the solution

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:12):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:12):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:13):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:13):

and solved all the exercises related to conj.

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:13):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:14):

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)

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:14):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:14):

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
}

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:15):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:15):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:15):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:15):

Sorry, what is your question?

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:15):

Did you manage to fill in the sorrys yourself?

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:16):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:16):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:16):

But still one small point eludes me:

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:17):

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"

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:17):

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?

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:17):

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.

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:17):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:18):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:18):

Yes

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:18):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:18):

We need to give Lean a map, and four proofs

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:18):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:19):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:19):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:20):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:20):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:21):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:21):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:21):

I am defining a second thing

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:21):

conj is the function, Conj is the ring homomorphism

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:21):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:22):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:22):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:23):

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)

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:25):

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.

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:26):

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.

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:27):

But it seems very edible.

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:27):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:27):

Yes, I have already done so.

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:27):

and then you can solve the levels individually in VS Code

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:27):

I am playing on my pc, actually

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:27):

I asked because you mentioned line 435

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:28):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:28):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:29):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:29):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:30):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:31):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:31):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:31):

I attended it live, actually .

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:31):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:32):

You mean that yesterday you'll be solving them?

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:32):

oops Thursday 28th :-)

view this post on Zulip Patrick Massot (May 22 2020 at 18:32):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:33):

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.

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:34):

Thank you for your help, in the meantime.

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:34):

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!

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:35):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:36):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:36):

Sure

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:36):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:37):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:37):

(are "they" computer scientists?)

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:37):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:38):

Sure, this makes sense.

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:38):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:38):

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

view this post on Zulip Patrick Massot (May 22 2020 at 18:39):

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.

view this post on Zulip Patrick Massot (May 22 2020 at 18:39):

I wish our students could be that ambitious.

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:40):

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

view this post on Zulip Patrick Massot (May 22 2020 at 18:42):

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)(RR)2(f, g) \in \left(\mathbb R^{\mathbb R}\right)^2 instead of f,g:RRf, g : \mathbb R \to \mathbb R...

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:42):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:42):

That's terrifying, though...

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:43):

That's the French for you

view this post on Zulip Patrick Massot (May 22 2020 at 18:44):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:46):

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.

view this post on Zulip Patrick Massot (May 22 2020 at 18:47):

Did you do the tutorials based on my course?

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 18:51):

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

view this post on Zulip Patrick Massot (May 22 2020 at 18:55):

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

view this post on Zulip Kevin Buzzard (May 22 2020 at 19:18):

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

view this post on Zulip Filippo A. E. Nuccio (May 22 2020 at 19:34):

Thanks to both of you!

view this post on Zulip Patrick Massot (May 22 2020 at 19:42):

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

view this post on Zulip Mario Carneiro (May 22 2020 at 19:53):

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)(RR)2(f, g) \in \left(\mathbb R^{\mathbb R}\right)^2 instead of f,g:RRf, g : \mathbb R \to \mathbb R...

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

view this post on Zulip Mario Carneiro (May 22 2020 at 19:54):

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

view this post on Zulip Patrick Massot (May 22 2020 at 20:01):

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

view this post on Zulip Sam Lichtenstein (May 22 2020 at 20:06):

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?

view this post on Zulip Alex J. Best (May 22 2020 at 20:08):

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

view this post on Zulip Sam Lichtenstein (May 22 2020 at 20:08):

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

view this post on Zulip Alex J. Best (May 22 2020 at 20:08):

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.

view this post on Zulip Sam Lichtenstein (May 22 2020 at 20:10):

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)

view this post on Zulip Gabriel Ebner (May 22 2020 at 20:11):

ctrl+.

view this post on Zulip Sam Lichtenstein (May 22 2020 at 20:12):

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

view this post on Zulip Sam Lichtenstein (May 22 2020 at 20:13):

is it supposed to?

view this post on Zulip Patrick Massot (May 22 2020 at 20:14):

Yes

view this post on Zulip Patrick Massot (May 22 2020 at 20:15):

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

view this post on Zulip Sam Lichtenstein (May 22 2020 at 20:17):

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

view this post on Zulip Sam Lichtenstein (May 22 2020 at 20:18):

but does not work in refine_struct{}

view this post on Zulip Mario Carneiro (May 22 2020 at 20:21):

I think you have to write refine_struct {! !}

view this post on Zulip Alex J. Best (May 22 2020 at 20:25):

Didn't seem to work after refine struct for me

view this post on Zulip Sam Lichtenstein (May 22 2020 at 20:25):

"no code actions available"

view this post on Zulip Bryan Gin-ge Chen (May 22 2020 at 20:40):

Hah, this seems to work:

import data.complex.basic

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

view this post on Zulip Jalex Stark (May 22 2020 at 21:04):

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)

view this post on Zulip Patrick Lutz (May 28 2020 at 21:15):

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?

view this post on Zulip Mario Carneiro (May 28 2020 at 21:17):

simp, ring is a whitelisted combination

view this post on Zulip Mario Carneiro (May 28 2020 at 21:17):

because it is mostly insensitive to additional simp rules

view this post on Zulip Patrick Lutz (May 28 2020 at 21:18):

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?

view this post on Zulip Mario Carneiro (May 28 2020 at 21:19):

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

view this post on Zulip Patrick Lutz (May 28 2020 at 21:20):

what's the difference between , and ; exactly?

view this post on Zulip Mario Carneiro (May 28 2020 at 21:22):

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

view this post on Zulip Alex J. Best (May 28 2020 at 21:22):

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

view this post on Zulip Patrick Lutz (May 28 2020 at 21:23):

Okay, I think I had missed that aspect of it

view this post on Zulip Patrick Lutz (May 28 2020 at 21:23):

Thanks

view this post on Zulip Alex J. Best (May 28 2020 at 21:23):

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

view this post on Zulip Reid Barton (May 28 2020 at 21:30):

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

view this post on Zulip Kevin Buzzard (May 28 2020 at 22:36):

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

view this post on Zulip Filippo A. E. Nuccio (May 30 2020 at 13:27):

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 C\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 Q\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?

view this post on Zulip Alex J. Best (May 30 2020 at 13:32):

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

view this post on Zulip Filippo A. E. Nuccio (May 30 2020 at 13:33):

Ahah! Thanks, I had the wrong adress.

view this post on Zulip Kevin Buzzard (May 30 2020 at 13:41):

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

view this post on Zulip Kevin Buzzard (May 30 2020 at 13:41):

@Filippo A. E. Nuccio

view this post on Zulip Filippo A. E. Nuccio (May 30 2020 at 13:45):

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 C\mathbb{C} is a field.

view this post on Zulip Kevin Buzzard (May 30 2020 at 14:46):

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.

view this post on Zulip Jalex Stark (May 31 2020 at 01:07):

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

view this post on Zulip Filippo A. E. Nuccio (May 31 2020 at 09:57):

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

view this post on Zulip Kenny Lau (May 31 2020 at 09:58):

it isn't?

view this post on Zulip Filippo A. E. Nuccio (May 31 2020 at 09:58):

?

view this post on Zulip Kenny Lau (May 31 2020 at 09:59):

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

view this post on Zulip Kenny Lau (May 31 2020 at 09:59):

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

view this post on Zulip Filippo A. E. Nuccio (May 31 2020 at 10:00):

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

view this post on Zulip Kenny Lau (May 31 2020 at 10:00):

yep

view this post on Zulip Filippo A. E. Nuccio (May 31 2020 at 10:00):

Great! Thanks.

view this post on Zulip Johan Commelin (May 31 2020 at 10:00):

It's a field "axiom"

view this post on Zulip Filippo A. E. Nuccio (May 31 2020 at 10:00):

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

view this post on Zulip Kevin Buzzard (May 31 2020 at 10:08):

Filippo A. E. Nuccio said:

Ah, so you are saying that it has already been declared that also in R\mathbb{R} we have a/0=0a/0=0 for all aRa\in\mathbb{R} and therefore the definition makes sense for all zCz\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.

view this post on Zulip Filippo A. E. Nuccio (May 31 2020 at 10:12):

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

view this post on Zulip Jalex Stark (Jun 01 2020 at 01:56):

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)

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 02:09):

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

view this post on Zulip ROCKY KAMEN-RUBIO (Jun 02 2020 at 19:17):

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?

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 19:23):

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

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 19:23):

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

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 19:24):

Someone suggested that it was obfuscating the proofs

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 19:24):

It was also making trivial proofs shorter

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 19:25):

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

view this post on Zulip ROCKY KAMEN-RUBIO (Jun 02 2020 at 20:30):

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

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 07:28):

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.

view this post on Zulip Mario Carneiro (Jun 03 2020 at 07:34):

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


Last updated: May 12 2021 at 04:19 UTC