Zulip Chat Archive

Stream: Codewars

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


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 08 2020 at 18:26):

Your reduce is assuming you are talking about nats

view this post on Zulip Johan Commelin (Jun 08 2020 at 18:26):

Where as lim_to_inf is talking about sequences of reals

view this post on Zulip Johan Commelin (Jun 08 2020 at 18:26):

Try #reduce (blabla : real)

view this post on Zulip Johan Commelin (Jun 08 2020 at 18:27):

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

view this post on Zulip Johan Commelin (Jun 08 2020 at 18:28):

So maybe try rat as a compromise

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 08 2020 at 18:39):

lean defaults to nat.

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 08 2020 at 18:42):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 08 2020 at 18:50):

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

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 18:52):

Does hovering over a numeral give any information?

view this post on Zulip Patrick Lutz (Jun 08 2020 at 18:53):

Not for me

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 08 2020 at 19:03):

ring

view this post on Zulip Johan Commelin (Jun 08 2020 at 19:04):

What does hint say?

view this post on Zulip 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 :-)

view this post on Zulip Patrick Lutz (Jun 08 2020 at 19:05):

Johan Commelin said:

What does hint say?

It says to try ring or finish

view this post on Zulip Patrick Lutz (Jun 08 2020 at 19:05):

I think I forgot that ring existed for some reason

view this post on Zulip Patrick Lutz (Jun 08 2020 at 19:05):

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

view this post on Zulip Johan Commelin (Jun 08 2020 at 19:06):

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

view this post on Zulip Patrick Lutz (Jun 08 2020 at 19:06):

I'd never heard of hint or finish before

view this post on Zulip Patrick Lutz (Jun 08 2020 at 19:06):

they both seem very useful potentially

view this post on Zulip Kenny Lau (Jun 08 2020 at 19:16):

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

view this post on Zulip Johan Commelin (Jun 08 2020 at 19:20):

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

view this post on Zulip Patrick Lutz (Jun 08 2020 at 19:24):

Does it suggest library_search?

view this post on Zulip 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

view this post on Zulip Patrick Lutz (Jun 08 2020 at 20:17):

Thanks everybody for answering my dumb questions


Last updated: May 08 2021 at 22:13 UTC