## Stream: general

### Topic: calculating fibonacci numbers

#### Johan Commelin (Apr 18 2020 at 12:05):

What is the correct way to calculate fibonacci numbers in Lean?

import data.nat.fib

open nat

example : fib 12 = 144 := by norm_num -- doesn't work


#### Johan Commelin (Apr 18 2020 at 12:11):

#eval fib 12


is instantaneous, but rfl doesn't work as proof of the above

#### Jason Rute (Apr 18 2020 at 12:18):

This is the archetypical example where the standard recursive definition is going to do a lot of extra computation (unless the lean compiler does something fancy). My guess is that if you need a fast version of fib, you can write your own (it’s pretty easy with some googling) and prove it is equal to fib. (But I’m not an expert.)

#### Kevin Buzzard (Apr 18 2020 at 12:24):

I clicked "try it online" and rfl failed to prove fib 12 = 144, but after staring at the definition I realised that -- oops -- it did prove fib 11 = 144 :-)

#### Kevin Buzzard (Apr 18 2020 at 12:24):

The canonical normalisation is the one Johan is using.

#### Johan Commelin (Apr 18 2020 at 12:26):

Wait, I get #eval fib 11 -- 89 in my Lean

#### Johan Commelin (Apr 18 2020 at 12:27):

But rfl is way too slow for these facts, it doesn't memoize

#### Kevin Buzzard (Apr 18 2020 at 12:28):

In TPIL they define their own Fibonacci numbers and I'm observing that rfl works for them

#### Kevin Buzzard (Apr 18 2020 at 12:28):

(or at least it did for me with "try it online")

#### Johan Commelin (Apr 18 2020 at 12:29):

Hmmm, weird... I think the definition in mathlib should actually memoize enough

#### Jason Rute (Apr 18 2020 at 12:37):

@Kevin Buzzard wrote

Generally speaking, from a computation standpoint, yes. From a math standpoint, that is the natural definition. I'll write some code showing the difference.

#### Kevin Buzzard (Apr 18 2020 at 12:39):

This is CS 101 coming up, isn't it :-) This is like the difference between foldl and foldr or something -- mathematically they are the same but computationally they couldn't be more different.

#### Kevin Buzzard (Apr 18 2020 at 12:41):

My problem is that even though I understand the basic principle that there are lots of mathematically equivalent ways to do something and they might have vastly different computational behaviour, when I see the definition like the one in TPIL I have so little understanding of what is happening under the hood that I am not capable of working out whether the definition is computationally good or not.

#### Kevin Buzzard (Apr 18 2020 at 12:42):

For all I know the equation compiler is cunningly storing all the auxiliary fib a computations on the way.

#### Jason Rute (Apr 18 2020 at 12:50):

I might be answering the wrong question. Johan isn't asking how does one compute with fib, but how does one prove fib 12 = 144. This works for me:

def fib: ℕ → ℕ
| 0 := 0
| 1 := 1
| (n + 2) := (fib n) + (fib (n + 1))

example : fib 12 = 144 := rfl


#### Johan Commelin (Apr 18 2020 at 12:51):

@Jason Rute But that one is slow, right?
Also, to be precise, I want to work with mathlib's fib...

#### Anne Baanen (Apr 18 2020 at 12:51):

According to TPiL "[The implementation of structural recursion] provides an efficient implementation of fib, avoiding the exponential blowup that would arise from evaluating each recursive call independently.", so it should not be slow.

#### Johan Commelin (Apr 18 2020 at 12:51):

What? Your fib is way faster than the one in mathlib... I'm really confused now

#### Shing Tak Lam (Apr 18 2020 at 12:52):

This works (I don't know why).

import data.nat.fib

open nat

example : fib 12 = 144 := by refl


#### Jason Rute (Apr 18 2020 at 12:53):

I'm more confused now too. I just looked at the mathlib implementation. It should be similar to this fast_fib which is much faster than the naive one:

def fast_fib_aux: ℕ → ℕ × ℕ
| 0 := (0, 1)
| 1 := (1, 1)
| (n + 2) := let (a, b) := fast_fib_aux (n + 1) in (b, a + b)

def fast_fib (n: ℕ): ℕ := (fast_fib_aux n).1

example : (fast_fib 12) = 144 := rfl


#### Johan Commelin (Apr 18 2020 at 12:54):

#eval fib 30 -- 832040 ... fast!

example : fib 30 = 832040 := by refl -- slow


#### Jason Rute (Apr 18 2020 at 12:55):

I thought I remember seeing that #eval takes shortcuts with interger computation that rfl can't take.

#### Johan Commelin (Apr 18 2020 at 12:57):

Sure, that might be the case. I also don't care whether the proof is by rfl. I just want some way to prove this, that doesn't involve manually apply fib_succ_succ and computing all the 30 fibonacci numbers before it.

#### Jason Rute (Apr 18 2020 at 12:58):

Does the by refl trick work for you? (Why does by refl work and not rfl?)

#### Johan Commelin (Apr 18 2020 at 12:59):

It works for fib 12, but not for fib 30

#### Jason Rute (Apr 18 2020 at 13:01):

You can use my fast_fib above (it works for 30) and prove it is equivalent to fib.) Maybe that needs to be the definition in mathlib.

#### Jason Rute (Apr 18 2020 at 13:02):

Sorry, I thought it was working for 30, but it doesn't. My bad.

#### Reid Barton (Apr 18 2020 at 13:18):

The equation compiler uses a version of memoization automatically.

fib 30

Even adding two numbers of around this size by rfl is too slow, so this can't work.

#### Kevin Buzzard (Apr 18 2020 at 13:18):

Johan Commelin said:

Sure, that might be the case. I also don't care whether the proof is by rfl. I just want some way to prove this, that doesn't involve manually apply fib_succ_succ and computing all the 30 fibonacci numbers before it.

I thought the problem was that with some naive implementations you compute all the 30 fibonacci numbers before it many many times.

#### Kevin Buzzard (Apr 18 2020 at 13:19):

There's a way of computing fib n involving induction on binary expansion of n, because $F_{2n}$ and $F_{2n+1}$ are closely related to $F_n$ by Binet.

#### Kevin Buzzard (Apr 18 2020 at 13:19):

That would be super-efficient, but I'm assuming that this isn't the question. Or is it?

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

So we turn that into simp-lemmas?

#### Kenny Lau (Apr 18 2020 at 13:26):

Kevin Buzzard said:

That would be super-efficient, but I'm assuming that this isn't the question. Or is it?

until you realize that dividing by 2 isn't O(1), but rather O(n)

#### Jason Rute (Apr 18 2020 at 13:29):

To be clear, I was originally mistaken on the definition used in mathlib. It is (what should be on paper) a fast definition. My first comment led us down the wrong track. As @Reid Barton said, apparently rfl isn't even good at adding large numbers (which is what exactly what any computation of fibonacci does). So I think this is still an open question how to prover stuff like this if rfl (and refl) are unusable.

#### Johan Commelin (Apr 18 2020 at 13:30):

$F_{2n} = \sum_{i < n} F_{2i+1}, \qquad F_{2n+1} = \left(\sum_{i < n} F_{2(i+1)} \right) + 1$

Am I stupid, or is there no division by two there?

#### Kevin Buzzard (Apr 18 2020 at 13:34):

I'm talking about $F_{2n}=$ something like $F_n^2$, the same trick that one uses when computing $a^b$ if $b$ is large, by repeated squaring.

#### Johan Commelin (Apr 18 2020 at 13:36):

@Kevin Buzzard That one :up: ?

Right.

#### Kevin Buzzard (Apr 18 2020 at 13:39):

If $n>>0$ and one can do the arithmetic efficiently then this is a far quicker way of computing Fibonacci numbers.

#### Kevin Buzzard (Apr 18 2020 at 13:40):

But I suspect that this has nothing to do with your original question.

#### Johan Commelin (Apr 18 2020 at 13:40):

Well, I want to show e.g. that fib 34 is > 4 million

#### Kevin Buzzard (Apr 18 2020 at 13:43):

Reid Barton said:

Even adding two numbers of around this size by rfl is too slow, so this can't work.

@Reid Barton
I once found a counterexample to this in front of a room full of schoolchildren and it took me a while to realise what the heck was going on:

example : 1000000000000 + 1000000000000 = 2000000000000 := rfl -- works fine


#### Kevin Buzzard (Apr 18 2020 at 13:43):

I had just coherently argued that this would fail miserably.

#### Jason Rute (Apr 18 2020 at 14:17):

So I think the prerequisite question is how does one prove this in Lean?

example : 317811 + 514229 = 832040


#### Kevin Buzzard (Apr 18 2020 at 14:20):

by norm_num

#### Reid Barton (Apr 18 2020 at 14:21):

This one is by norm_num. The question is really how to make norm_num aware of fib, or fib aware of norm_num, or something which can do both definitional unfolding and norm_num where appropriate.

#### Kenny Lau (Apr 18 2020 at 14:29):

maybe if norm_num accepts tags then we can tag fib_bit0 and fib_bit1 as norm_num

#### Kenny Lau (Apr 18 2020 at 14:29):

this still wouldn't make it memoize though

#### Kenny Lau (Apr 18 2020 at 14:30):

Johan Commelin said:

there must be a formula without minus

#### Johan Commelin (Apr 18 2020 at 14:31):

Well, F n * L n doesn't contain a minus... maybe there are fast formulas for L n as well??

#### Kenny Lau (Apr 18 2020 at 14:48):

$\begin{bmatrix} F_{2n+1} & F_{2n} \\ F_{2n} & F_{2n-1} \end{bmatrix} = \begin{bmatrix} F_{n+1} & F_{n} \\ F_{n} & F_{n-1} \end{bmatrix}^2$

20 = 2 * 10 = 2 * (2 * 5) = 2 * (2 * (2 * 2 + 1))
(F(0), F(1)) = (0, 1)
(F(1), F(2)) = (0*0+1*1, 1*(2*0+1)) = (1, 1)
(F(3), F(4)) = (1*1+1*1, 1*(2*1+1)) = (2, 3)
(F(4), F(5)) = (3, 2+3) = (3, 5)
(F(9), F(10)) = (3*3+5*5, 5*(2*3+5)) = (34, 55)
(F(19), F(20)) = (34*34+55*55, 55*(2*34+55)) = (4181, 6765)


proposed algorithm:

fib 20
= fib (bit0 10)
= fib (bit0 $bit0 5) = fib (bit0$ bit0 $bit1 2) = fib (bit0$ bit0 $bit1$ bit0 1)
→ (fib_aux $bit0$ bit0 $bit1$ bit0 1).2
→ (f0 $fib_aux$ bit0 $bit1$ bit0 1).2
→ (f0 $f0$ fib_aux $bit1$ bit0 1).2
→ (f0 $f0$ fs $f0$ fib_aux $bit0 1).2 → (f0$ f0 $fs$ f0 $f0$ fib_aux 1).2
→ (f0 $f0$ fs $f0$ f0 (0, 1)).2
→ (f0 $f0$ fs $f0 (0*0+1*1, 1*(2*0+1))).2 → (f0$ f0 $fs$ f0 (1, 1)).2
→ (f0 $f0$ fs (1*1+1*1, 1*(2*1+1))).2
→ (f0 $f0$ fs (2, 3)).2
→ (f0 $f0 (3, 2+3)).2 → (f0$ f0 (3, 5)).2
→ (f0 (3*3+5*5, 5*(2*3+5))).2
→ (f0 (34, 55)).2
→ (34*34+55*55, 55*(2*34+55)).2
→ (4181, 6765).2
→ 6765


#### Kevin Buzzard (Apr 18 2020 at 14:51):

That is much better than the foldl/foldr issue

foldl/foldr?

#### Kenny Lau (Apr 18 2020 at 14:52):

def f0(s):
return ("({0}*{0}+{1}*{1})".format(*s), "{1}*(2*{0}+{1})".format(*s))
def fs(s):
return (s,"({0}+{1})".format(*s))

f20 = f0(f0(fs(f0(f0((0,1))))))
print(f20)
print(eval(f20))


output:

(((0*0+1*1)*(0*0+1*1)+1*(2*0+1)*1*(2*0+1))+1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1)))*(2*1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1))+(((0*0+1*1)*(0*0+1*1)+1*(2*0+1)*1*(2*0+1))+1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1))))*(2*(1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1))*1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1))+(((0*0+1*1)*(0*0+1*1)+1*(2*0+1)*1*(2*0+1))+1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1)))*(((0*0+1*1)*(0*0+1*1)+1*(2*0+1)*1*(2*0+1))+1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1))))+(((0*0+1*1)*(0*0+1*1)+1*(2*0+1)*1*(2*0+1))+1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1)))*(2*1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1))+(((0*0+1*1)*(0*0+1*1)+1*(2*0+1)*1*(2*0+1))+1*(2*0+1)*(2*(0*0+1*1)+1*(2*0+1)))))

6765


#### Kevin Buzzard (Apr 18 2020 at 14:52):

I just mean asking a functional language to compute Fibonacci numbers might naively involve computing $F_{n-d}$ about $d$ times. It's not foldl/foldr but it's the same sort of thing.

#### Kenny Lau (Apr 18 2020 at 14:53):

I don't know whether it will cause problem if the intermediate expressions are not immediately evaluated

#### Kenny Lau (Apr 18 2020 at 14:53):

it might undo our optimization by having exponential complexity (on top of logarithmic complexity)

#### Kenny Lau (Apr 18 2020 at 14:53):

then the overall complexity would just be O(n)

#### Reid Barton (Apr 18 2020 at 14:54):

None of this is really relevant if you can't compute these additions in subexponential time

#### Kevin Buzzard (Apr 18 2020 at 14:54):

Yes, you are evaluating 0*0+1*1 a lot of times there

#### Kenny Lau (Apr 18 2020 at 14:54):

Reid Barton said:

None of this is really relevant if you can't compute these additions in subexponential time

norm_num can

#### Reid Barton (Apr 18 2020 at 14:54):

But you can't solve the original problem using norm_num

#### Reid Barton (Apr 18 2020 at 14:55):

You are solving the second problem before solving the first problem.

#### Kenny Lau (Apr 18 2020 at 14:55):

if you're referring to writing a tactic that will calculate fib 20, then my algorithm can call norm_num in each intermediate step

#### Kenny Lau (Apr 18 2020 at 14:55):

what's the first problem?

#### Reid Barton (Apr 18 2020 at 14:56):

I don't want to write a new tactic to compute every function I write.

#### Kenny Lau (Apr 18 2020 at 14:56):

so I also proposed having a norm_num tag that you can tag my lemmas with, which include fib n = (fib_aux n).2 and fib_aux (bit0 n) = f0 (fib_aux n) and fib_aux(bit1 n) = fs (f0 (fib_aux n)), and my algorithm demonstrated how you can use these three lemmas to calculate fib 20 in logarithmic time

#### Kevin Buzzard (Apr 18 2020 at 14:57):

One could imagine a general "multiply these two matrices together using norm_num and also other tricks" function.

(removed)

#### Kevin Buzzard (Apr 18 2020 at 14:57):

Such a function will I think be hard coded into any decent computer algebra system

(removed)

#### Alex J. Best (Apr 18 2020 at 17:05):

@Mario Carneiro has mentioned that we need Coq's cbv tactic a few times now for similar questions I believe, but I don't know enough about coq to know what needs doing here (can we get a formal roadmap for a tactic)!

#### Mario Carneiro (Apr 18 2020 at 20:13):

As Reid suggests, the "right" answer here is to extend norm_num, and I've been meaning to use def_replacer for this purpose so that norm_num doesn't have to import every number theoretic function it will ever use

#### Mario Carneiro (Apr 18 2020 at 20:15):

There is nothing wrong with using - inside norm_num, because norm_num doesn't prove a - b = c, it proves b + c = a where a and b are the inputs and c is the output

#### Mario Carneiro (Apr 18 2020 at 20:20):

Extending norm_num is a bit more complicated than just marking fib_bit0 and fib_bit1, because it's not a simp set, it requires some carefully stated custom theorems and goes by recursion, which is much faster than simp

#### Mario Carneiro (Apr 18 2020 at 20:22):

But it also means that it is not difficult to get it to evaluate subterms as required to get the O(n log n) algorithm

#### Mario Carneiro (Apr 18 2020 at 20:24):

Johan Commelin said:

Well, I want to show e.g. that fib 34 is > 4 million

If that's all you want, you don't need to evaluate fib at all, unless that bound is particularly close. A quick estimation method would say that fib n is close to phi^n / sqrt 5 or something like that, and you can easily get proven bounds on phi using continued fractions

#### Kevin Buzzard (Apr 18 2020 at 20:36):

import data.nat.fib

open nat

example : fib 12 = 144 := begin
rw fib_succ_succ,
rw @fib_succ_succ 9,
rw @fib_succ_succ 8,
rw @fib_succ_succ 7,
rw @fib_succ_succ 6,
rw @fib_succ_succ 5,
rw @fib_succ_succ 4,
rw @fib_succ_succ 3,
rw @fib_succ_succ 2,
rw @fib_succ_succ 1,
rw @fib_succ_succ 0,
refl,
end


#### Kevin Buzzard (Apr 18 2020 at 20:37):

example : fib 12 = 144 := begin
-- start the countdown
rw @fib_succ_succ 10,
rw @fib_succ_succ 9,
rw @fib_succ_succ 8,
rw @fib_succ_succ 7,
rw @fib_succ_succ 6,
rw @fib_succ_succ 5,
rw @fib_succ_succ 4,
rw @fib_succ_succ 3,
rw @fib_succ_succ 2,
rw @fib_succ_succ 1,
rw @fib_succ_succ 0,
rw @fib_one,
rw @fib_zero,
end


Last updated: May 11 2021 at 13:22 UTC