## 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?

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

#### Patrick Lutz (Jun 08 2020 at 19:05):

Johan Commelin said:

What does hint say?

It says to try ring or finish

#### Patrick Lutz (Jun 08 2020 at 19:05):

I think I forgot that ring existed for some reason

#### Patrick Lutz (Jun 08 2020 at 19:05):

I've gotten too used to using norm_num simp and linarith

#### Johan Commelin (Jun 08 2020 at 19:06):

@Patrick Lutz Well, you can forget about ring if you remember hint :rofl:

#### Patrick Lutz (Jun 08 2020 at 19:06):

I'd never heard of hint or finish before

#### Patrick Lutz (Jun 08 2020 at 19:06):

they both seem very useful potentially

#### Kenny Lau (Jun 08 2020 at 19:16):

we're on our way to building the slowest tactic ever

#### Johan Commelin (Jun 08 2020 at 19:20):

I don't think that hint suggests hint...

#### Patrick Lutz (Jun 08 2020 at 19:24):

Does it suggest library_search?

#### Patrick Lutz (Jun 08 2020 at 20:17):

Well, I've now solved the kata although I can't say my solution is especially nice looking

#### Patrick Lutz (Jun 08 2020 at 20:17):

Thanks everybody for answering my dumb questions

Last updated: May 08 2021 at 22:13 UTC