# Zulip Chat Archive

## Stream: new members

### Topic: rw not working with nat.fib

#### ROCKY KAMEN-RUBIO (Apr 19 2020 at 02:07):

(from the coderwars fibonacci problem). I think I'm misunderstanding something about the interface between `nat`

and `real`

here, and the way `nat.fib`

is defined. I'm getting errors on the last two lines even though the rewrites look like they're trying to rewrite things that are there. Any comments or links to resources would be appreciated; I've had a hard time finding useful info on working with reals in tactic mode.

lemma f_succ_succ' (n : ℕ) : fib (succ (succ n)) = (fib (succ n)) + (fib n) := begin sorry, end theorem binet' (n : ℕ) : (nat.fib n : ℝ) = (phi^n - psi^n) / real.sqrt 5 := begin induction n with k hk, simp, induction k with l hl, sorry, rw f_succ_succ, rw hl, end

#### Reid Barton (Apr 19 2020 at 02:37):

Is there a reason that your lemma has a `'`

but you rewrite with a lemma without the `'`

?

Can you provide working code?

#### ROCKY KAMEN-RUBIO (Apr 19 2020 at 03:45):

Reid Barton said:

Is there a reason that your lemma has a

`'`

but you rewrite with a lemma without the`'`

?

Can you provide working code?

Sorry! This error got introduce when I simplified my code to show the error more concisely. The error is still happening though.

#### Reid Barton (Apr 19 2020 at 03:54):

Can you provide working code then?

#### ROCKY KAMEN-RUBIO (Apr 19 2020 at 05:46):

lemma f_succ_succ' (n : ℕ) : fib (succ (succ n)) = (fib (succ n)) + (fib n) :=

begin

sorry,

end

theorem binet' (n : ℕ) : (nat.fib n : ℝ) = (phi^n - psi^n) / real.sqrt 5 :=

begin

induction n with k hk,

simp,

induction k with l hl,

sorry,

rw f_succ_succ',

rw hl,

rw hk,

end

#### Johan Commelin (Apr 19 2020 at 06:13):

If you put the code between

``` your code here ```

then you get syntax highlighting

#### Shing Tak Lam (Apr 19 2020 at 06:49):

@ROCKY KAMEN-RUBIO

For a Minimum Working Example, you want to include imports and all definitions required here. so it should look like this:

For something from Codewars, include the preloaded file, so people can just copy what you post here and run it.

import data.nat.fib data.real.basic open nat noncomputable theory def phi : ℝ := (1 + real.sqrt 5) / 2 def psi : ℝ := (1 - real.sqrt 5) / 2 lemma f_succ_succ' (n : ℕ) : fib (succ (succ n)) = (fib (succ n)) + (fib n) := begin sorry, end theorem binet' (n : ℕ) : (nat.fib n : ℝ) = (phi^n - psi^n) / real.sqrt 5 := begin induction n with k hk, simp, induction k with l hl, sorry, rw f_succ_succ', rw hl, rw hk, end

#### Shing Tak Lam (Apr 19 2020 at 06:50):

The reasons why your rewrites weren't working was because in your goal, you have `↑(fib (succ l) + fib l)`

, but in`hk`

you have `↑(fib (succ l))`

. If you use `norm_num`

, your goal becomes `↑(fib (succ l)) + ↑(fib l)`

and your rewrite works.

#### Shing Tak Lam (Apr 19 2020 at 06:52):

(Removed, Kata spoiler?)

#### Shing Tak Lam (Apr 19 2020 at 07:20):

(Kata spoiler?)

Last updated: May 11 2021 at 00:31 UTC