# 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 interpreting`9/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 `nat`

s

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

Where as `lim_to_inf`

is talking about sequences of `real`

s

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

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