Zulip Chat Archive

Stream: new members

Topic: rw not working with nat.fib


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

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

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

view this post on Zulip Reid Barton (Apr 19 2020 at 03:54):

Can you provide working code then?

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

view this post on Zulip Johan Commelin (Apr 19 2020 at 06:13):

If you put the code between

```
your code here
```

then you get syntax highlighting

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

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

view this post on Zulip Shing Tak Lam (Apr 19 2020 at 06:52):

(Removed, Kata spoiler?)

view this post on Zulip Shing Tak Lam (Apr 19 2020 at 07:20):

(Kata spoiler?)


Last updated: May 11 2021 at 00:31 UTC