The Fibonacci Sequence

Summary

Definition of the Fibonacci sequence F₀ = 0, F₁ = 1, Fₙ₊₂ = Fₙ + Fₙ₊₁.

Main Definitions

Main Statements

Implementation Notes

For efficiency purposes, the sequence is defined using stream.iterate.

Tags

fib, fibonacci


_private.1927372039.fib_aux_stream

Auxiliary stream creating Fibonacci pairs ⟨Fₙ, Fₙ₊₁⟩.

nat.fib

Implementation of the fibonacci sequence satisfying fib 0 = 0, fib 1 = 1, fib (n + 2) = fib n + fib (n + 1).

Note: We use a stream iterator for better performance when compared to the naive recursive implementation.

nat.fib_succ_succ

Shows that fib indeed satisfies the Fibonacci recurrence Fₙ₊₂ = Fₙ + Fₙ₊₁.