rw not working with nat.fib

Stream: new members

[ROCKY KAMEN-RUBIO]

(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]

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]

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]

Can you provide working code then?

[ROCKY KAMEN-RUBIO]

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]

If you put the code between

```
your code here
```

then you get syntax highlighting

[Shing Tak Lam]

@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]

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]

(Removed, Kata spoiler?)

[Shing Tak Lam]

(Kata spoiler?)