Real Numbers game

Stream: Lean for teaching

[Riccardo Brasca]

In case anyone is interested, for a course I am teaching I've written some sort of a real numbers game, you can find it here. It is based (I mean shamelessly copied) on @Kevin Buzzard repo, where he defines the integers and the rationals. I also define the reals, up to the proof that they're a complete ordered archimedean field. Some comments:

• I have completely sorry free fies (not in the repo, but just ask me if you want.
• compared to Kevin's work, MyRat is Based on MyInt, and MyReal is based on MyRat.
• I didn't do MyNat, but I guess it's doable.
• I use heavy tactics, but mathlib's integers and rations don't appear explicitly.
• completeness is Cauchy completeness, with everything defined by hand (there is no topology/metric theory, just the absolute value that exists because R is a bla bla ordered field).

Overall it was pretty fun, and linarith, grw and grind really helped.

[Kenny Lau]

We might need a p-adic numbers game soon! :melt:

[Riccardo Brasca]

This is indeed the next subject of the course, but it's only on the blackboard

[Kevin Buzzard]

Wow, you made MyRat from MyInt and MyReal from MyRat? I've always been scared to do that -- I made MyNat, and then MyInt from Nat, and then MyRat from Int, so I always had access to things like omega. Maybe grind is better?

A heads-up: I have a student this summer who might work on a different kind of real number game -- start with the reals presented axiomatically and develop the theory from there. It was suggested a while ago on this Zulip that that might be an interesting game, and it's something I've not tried before.

[Riccardo Brasca]

Yes, grind immediately did the annoying things where you used nlinarith or polyrith or something. And grw for inequalities is really helpful

[Riccardo Brasca]

The students already played the NNG, so I didn't do MyNat, but I will surely try.

[Kevin Buzzard]

Fun fact: the way NNG was originally designed was this. I first searched for (Lean 3) classes that nat was an instance of, e.g. ordered_semiring or whatever, and then tried to prove all the axioms for all those classes.

[Riccardo Brasca]

Just to give an idea, here is the proof that the product of two rational Cauchy sequence is Cauchy (here Cauchy means rational ε, the reals don't exist yet). You should be able to guess the used results by their names. The proof is really close to the pen and paper proof.

lemma IsCauchy.mul {x y : ℕ → MyRat} (hx : IsCauchy x) (hy : IsCauchy y) : IsCauchy (x * y) := by
  rcases hx.bounded with ⟨A, hApos, hA⟩
  rcases hy.bounded with ⟨B, hBpos, hB⟩
  intro ε hε
  rcases hx (ε/(2*B)) (div_pos hε (by linarith)) with ⟨N, HN⟩
  rcases hy (ε/(2*A)) (div_pos hε (by linarith)) with ⟨M, HM⟩
  use max N M
  intro p q hp hq
  calc |(x * y) p - (x * y) q| = |x p * y p - x q * y q| := by simp
       _ = |x p * (y p - y q) + y q * (x p - x q)| := by ring_nf
       _ ≤ |x p * (y p - y q)| + |y q * (x p - x q)| := abs_add _ _
       _ = |x p| * |(y p - y q)| + |y q| * |(x p - x q)| := by simp only [abs_mul]
       _ ≤ A * (ε/(2*A)) + B * (ε/(2*B)) := by grw [hA, hB, HN p q (by grind) (by grind),
                                              HM p q (by grind) (by grind)]
       _ = ε := by field_simp; ring

[Riccardo Brasca]

Note that div_pos is docs#div_pos, I didn't prove it.

[Riccardo Brasca]

I have a versione with MyNat --> MyInt --> MyRat --> MyReal. It's really not such a pain, I am pleasantly surprised.

[Kevin Buzzard]

Wow! Nice!

[Kevin Buzzard]

Looking forward to MyPadic and MyComplex (and of course. MyPadicComplex, which just landed in mathlib!)

[David Michael Roberts]

Then MyAdeles, right?

[Miguel Marco]

Kevin Buzzard said:

A heads-up: I have a student this summer who might work on a different kind of real number game -- start with the reals presented axiomatically and develop the theory from there. It was suggested a while ago on this Zulip that that might be an interesting game, and it's something I've not tried before.

I have a student doing that for his Degree Thesis (not in the form of a game: the idea is to go from the definition of linearlyorderedfield with the axiom of supremum to prove that any two such fields are isomorphic).

[Kevin Buzzard]

That's a nice project! We have the result in mathlib but probably the proof is unreadable :-)

[Miguel Marco]

Kevin Buzzard said:

That's a nice project! We have the result in mathlib but probably the proof is unreadable :-)

Where exactly is it?

[Kevin Buzzard]

I'm not at a computer this week but if you look at the blog post about checking the scholze project then it's mentioned there

[Riccardo Brasca]

It is docs#LinearOrderedField.inducedOrderRingIso

[Niklas Halonen]

Hi @Riccardo Brasca! Thanks for making the (Real) Numbers game, I had a lot of fun and learned a lot! I have a couple of feedback points if you're intetested:

• In Real.lean working with the coercions (MyRat.i and k) was quite painful and I wondered if it could have been better to build some norm_num lemmas along the way.
• I found the following lemmas lemma k_div {a b : MyRat} : k (a / b) = (k a / k b) and lemma k_abs {a : MyRat} : k |a| = |k a| useful in section completeness.
• I ended up rewriting many thing in Filter.eventually style to use lemmas such as eventually.and to make things easier, but feel like my solutions are inelegant because of the constant back and forth rewriting eventually_atTop.

Despite these issues the game was the best Lean game I have played (at least after NNG)! Here are my current solutions for reference.

[Riccardo Brasca]

Thanks for the comments! I didn't want to introduce coercions, so I avoided them completely (I wanted the students to realize the these maps really exist), and similarly I didn't want to speak about filters, so I write by hand the notion of Cauchy sequence, but of course this would scale for a large library.