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





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