Zulip Chat Archive

Stream: Codewars

Topic: 0.999... = 1? Prove it!

Patrick Lutz (Jun 08 2020 at 18:25):

I've been trying to complete the kata titled "0.999... = 1? Prove it!" and I've encountered something very confusing. The problem asks you to prove

theorem zero_point_nine_recurring_is_one :
lim_to_inf (λ n, 9 / 10 * geom_series (1 / 10) n) 1

where

def lim_to_inf (x : ℕ → ℝ) (l : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, abs (x n - l) < ε

However I noticed that

#reduce 9 / 10 * geom_series (1 / 10) 10

gives me 0 and likewise

#reduce geom_series (1 / 10) 10

gives me 1. It seems like what's going on is that Lean is interpreting9/10 and 1/10 as natural numbers (which means they are both 0). If so, doesn't this make the theorem impossible to prove?

On the other hand, apparently 6 people have solved this problem on codewars, so maybe I am just confused about something?

Johan Commelin (Jun 08 2020 at 18:26):

Your reduce is assuming you are talking about nats

Johan Commelin (Jun 08 2020 at 18:26):

Where as lim_to_inf is talking about sequences of reals

Johan Commelin (Jun 08 2020 at 18:26):

Try #reduce (blabla : real)

Johan Commelin (Jun 08 2020 at 18:27):

Of course you will then discover that reals are not computable...

Johan Commelin (Jun 08 2020 at 18:28):

So maybe try rat as a compromise

Johan Commelin (Jun 08 2020 at 18:28):

Also #reduce will probably timeout, but #eval will give you the answer in a blink of the eye

Patrick Lutz (Jun 08 2020 at 18:39):

So far when doing stuff in Lean I often have problems knowing when Lean will interpret numbers as natural numbers or real numbers and getting it to switch between them. Is there any general advice about this, or should I just find specific cases that are confusing me and ask about them on zulip?

Johan Commelin (Jun 08 2020 at 18:39):

lean defaults to nat.

Johan Commelin (Jun 08 2020 at 18:40):

If you want something else, either the context should force it, or you should force it (by using (bla : something_else))

Reid Barton (Jun 08 2020 at 18:40):

Generally Lean's type inference works outside-in, so here because lim_to_inf expects a function returning real all the operations and numeric literals are inferred to be reals.

Reid Barton (Jun 08 2020 at 18:42):

But in your #reduce examples there is no expected type.

Patrick Lutz (Jun 08 2020 at 18:48):

Is there some way to get Lean goal to show me what type it thinks everything is?

Johan Commelin (Jun 08 2020 at 18:50):

set_option pp.all true will give you more than you asked for.

Kevin Buzzard (Jun 08 2020 at 18:52):

Does hovering over a numeral give any information?

Patrick Lutz (Jun 08 2020 at 18:53):

Not for me

Patrick Lutz (Jun 08 2020 at 19:01):

I have another question related to this same kata which is not related to my first one (I think). The question is basically, what is the one line way to prove the following theorem?

example (a b : ℝ) : 1 - a*b = 1 + (-a)*b := by sorry

simp and norm_num both fail and library_search times out. Perhaps there is some theorem in mathlib I could apply to solve it in one line, but I don't find it very easy to search for things in mathlib. So what I'm really asking for is not just a one line solution, but a way to painlessly discover a one line solution to theorems of this difficulty level

Kevin Buzzard (Jun 08 2020 at 19:03):

ring

Johan Commelin (Jun 08 2020 at 19:04):

What does hint say?

Kevin Buzzard (Jun 08 2020 at 19:04):

ring solves things which follow from the axioms of a ring (i.e. +, - and * and their usual behavour). linarith solves inequalities. These are some of only a small number of high-powered tactics, so you should just painlessly learn of their existence :-)