Section 2 : An introduction to the real numbers =============================================== The real real numbers --------------------- Lean's maths library ``mathlib`` has the real numbers. This isn't surprising, a lot of programming languages like Python etc have the real numbers. But actually there is a difference between Python's real numbers and Lean's real numbers. Python's real numbers are actually what a computer scientist would call ``float`` s, i.e. floating point numbers. Are floating point numbers different to real numbers? Yes, definitely! There are only finitely many floating point numbers, for example. Floats are "real numbers stored up to a finite precision". Addition on floats is not associative; if ``N`` is a really large floating point number and ``ε`` is a really small floating point number, then ``N+ε=N`` because of rounding errors, so ``(-N)+(N+ε)=0`` but ``((-N)+N)+ε=ε``. Lean's real numbers are the *real* real numbers. Lean's real numbers are defined under the hood as equivalence classes of Cauchy sequences (although you will never need to know this). You can prove that Lean's real numbers are uncountable. Remember that in Lean, we use types not sets. So the real numbers are a *type*. They have an official name of ``real``, but we never use this; we always use the notation, which is ``ℝ``. Type this in VS Code with ``\R``. Lean's maths library ``mathlib`` doesn't just have the real numbers -- it also has what is known to computer scientists as an "Application Programming Interface" for the real numbers, otherwise known as an "API" or "interface". This sounds extremely intimidating, until you discover what this actually means in practice: it means that Lean knows a whole bunch of theorems about the real numbers (for example, a nonempty bounded set of reals has a least upper bound), and Lean also has a whole bunch of definitions of standard functions on the real numbers like the cosine function ``real.cos : ℝ → ℝ`` and the square root function ``real.sqrt : ℝ → ℝ`` and so on, and it knows a bunch of theorems about these functions too. Garbage in, garbage out ----------------------- Did you spot what looked like a mistake in what I just said? I just claimed that the ``mathlib`` function ``real.sqrt`` took in a real number and outputted a real number. So what happens if you feed in ``-1`` or some other negative number? Lean doesn't give you an error! It just spits out some arbitrary answer -- for all I know, ``real.sqrt(-1) = 37``. I have no idea what ``real.sqrt(-1)`` actually is, and it doesn't even matter, because I am a mathematician, so I only run ``real.sqrt`` on non-negative real numbers. If I want to take the square root of a negative number, I use ``complex.sqrt``. Perhaps you are worried that such a cavalier attitude towards square roots of negative numbers leads to contradictions in the system -- but it does not. The simplest way to explain why is the following. Let me define a function ``f`` on the real numbers, by ``f(x)=sqrt(x)`` for ``x>=0``, and ``f(x)=37`` if ``x<0``. Does *defining such a function* lead to a contradiction in mathematics? Of course it does not! That's what ``real.sqrt`` looks like (although they might have chosen ``0`` or ``sqrt(-x)`` for the output when ``x`` was negative -- who knows, and who cares). The trick is that it is in the *theorems* about ``real.sqrt`` where the hypotheses of nonnegativity appear. For example, it is probably not true that ``real.sqrt(a*b)=real.sqrt(a)*real.sqrt(b)`` in general, because ``a`` or ``b`` might be negative. However it *is* true that ``real.sqrt(a*b)=real.sqrt(a)*real.sqrt(b)`` if ``a ≥ 0`` and ``b ≥ 0``, and this is the theorem in the library. So you *do* have to check that you're not taking the square roots of negative numbers -- just not where you might expect. Lean is not a computer ---------------------- The last thing I would like to say about the real numbers in this introduction is that Lean 3 is *not designed to compute*. This might all change in Lean 4, but right now you cannot try and "evaluate" ``real.sqrt 2`` and expect the answer to be equal to ``1.41421356...``. That ``...`` has no meaning in Lean, because real numbers have infinite precision. You could prove that ``1.41421356 < real.sqrt 2 < 1.41421357`` and right now you would have to do this manually by squaring up and multiplying out. I think it would be an interesting and possibly tricky challenge to prove something like ``0.54 < real.cos 1 ∧ real.cos 1 < 0.55`` (Lean's cosines are of course in radians; one might want to try and prove this using the power series expansion of cosine but it might well be painful). Working with reals ------------------ How do we state that ``2+2=4``? We can do it like this: .. code-block:: example : (2 : ℝ) + 2 = 4 := begin sorry end What's going on here? If I hadn't put that ``ℝ`` in there, Lean would have assumed that I meant the natural number ``2`` -- Lean's "default" ``2``. The naturals, integers, rationals, reals and complexes (and p-adic numbers for all primes p, if you know what they are) are all different types, so they all have different ``2`` s. Writing ``(2 : ℝ)`` tells Lean exactly which ``2`` we mean. So how come we didn't have to write ``(2 : ℝ) + (2 : ℝ) = (4 : ℝ)``? The reason for this is that addition in Lean takes two terms of a type ``X`` and outputs a term of the same type ``X``, so once Lean knows that the first term has type ``ℝ`` it figures out that all the other terms must have type ``ℝ`` as well for things to make sense. How do we *prove* that ``2+2=4``? The answer is the :ref:`norm_num ` tactic, which "normalises numerical expressions" -- in other words it proves equalities and inequalities *as long as only numbers, and no variables, are involved*. To solve the ``sorry`` s in section 2 you'll need to know about the :ref:`norm_num ` and :ref:`ring ` tactics, as well as the specialize tactic. Read about them in the tactic documentation in Part C, and, if you like, in the `mathlib community tactic documentation `_ .