Fibonacci Numbers

This file defines the fibonacci series, proves results about it and introduces methods to compute it quickly.

The Fibonacci Sequence

Summary

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

Main Definitions

• Nat.fib returns the stream of Fibonacci numbers.

Main Statements

• Nat.fib_add_two: shows that fib indeed satisfies the Fibonacci recurrence Fₙ₊₂ = Fₙ + Fₙ₊₁..
• Nat.fib_gcd: fib n is a strong divisibility sequence.
• Nat.fib_succ_eq_sum_choose: fib is given by the sum of Nat.choose along an antidiagonal.
• Nat.fib_succ_eq_succ_sum: shows that F₀ + F₁ + ⋯ + Fₙ = Fₙ₊₂ - 1.
• Nat.fib_two_mul and Nat.fib_two_mul_add_one are the basis for an efficient algorithm to compute fib (see Nat.fastFib). There are bit0/bit1 variants of these can be used to simplify fib expressions: simp only [Nat.fib_bit0, Nat.fib_bit1, Nat.fib_bit0_succ, Nat.fib_bit1_succ, Nat.fib_one, Nat.fib_two].

Implementation Notes

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

Tags

fib, fibonacci

def Nat.fib (n : ℕ) : ℕ

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.

Equations

• Nat.fib n = ((fun (p : ℕ × ℕ) => (p.2, p.1 + p.2))^[n] (0, 1)).1

@[simp]

theorem Nat.fib_zero : Nat.fib 0 = 0

@[simp]

theorem Nat.fib_one : Nat.fib 1 = 1

@[simp]

theorem Nat.fib_two : Nat.fib 2 = 1

theorem Nat.fib_add_two {n : ℕ} : Nat.fib (n + 2) = Nat.fib n + Nat.fib (n + 1)

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

theorem Nat.fib_add_one {n : ℕ} : n ≠ 0 → Nat.fib (n + 1) = Nat.fib (n - 1) + Nat.fib n

theorem Nat.fib_le_fib_succ {n : ℕ} : Nat.fib n ≤ Nat.fib (n + 1)

theorem Nat.fib_mono : Monotone Nat.fib

@[simp]

theorem Nat.fib_eq_zero {n : ℕ} : Nat.fib n = 0 ↔ n = 0

@[simp]

theorem Nat.fib_pos {n : ℕ} : 0 < Nat.fib n ↔ 0 < n

theorem Nat.fib_add_two_sub_fib_add_one {n : ℕ} : Nat.fib (n + 2) - Nat.fib (n + 1) = Nat.fib n

theorem Nat.fib_lt_fib_succ {n : ℕ} (hn : 2 ≤ n) : Nat.fib n < Nat.fib (n + 1)

theorem Nat.fib_add_two_strictMono : StrictMono fun (n : ℕ) => Nat.fib (n + 2)

fib (n + 2) is strictly monotone.

theorem Nat.fib_strictMonoOn : StrictMonoOn Nat.fib (Set.Ici 2)

theorem Nat.fib_lt_fib {m : ℕ} (hm : 2 ≤ m) {n : ℕ} : Nat.fib m < Nat.fib n ↔ m < n

theorem Nat.le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) : n ≤ Nat.fib n

theorem Nat.le_fib_add_one (n : ℕ) : n ≤ Nat.fib n + 1

theorem Nat.fib_coprime_fib_succ (n : ℕ) : Nat.Coprime (Nat.fib n) (Nat.fib (n + 1))

Subsequent Fibonacci numbers are coprime, see https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime

theorem Nat.fib_add (m : ℕ) (n : ℕ) : Nat.fib (m + n + 1) = Nat.fib m * Nat.fib n + Nat.fib (m + 1) * Nat.fib (n + 1)

See https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers

theorem Nat.fib_two_mul (n : ℕ) : Nat.fib (2 * n) = Nat.fib n * (2 * Nat.fib (n + 1) - Nat.fib n)

theorem Nat.fib_two_mul_add_one (n : ℕ) : Nat.fib (2 * n + 1) = Nat.fib (n + 1) ^ 2 + Nat.fib n ^ 2

theorem Nat.fib_two_mul_add_two (n : ℕ) : Nat.fib (2 * n + 2) = Nat.fib (n + 1) * (2 * Nat.fib n + Nat.fib (n + 1))

theorem Nat.fib_bit0 (n : ℕ) : Nat.fib (bit0 n) = Nat.fib n * (2 * Nat.fib (n + 1) - Nat.fib n)

theorem Nat.fib_bit1 (n : ℕ) : Nat.fib (bit1 n) = Nat.fib (n + 1) ^ 2 + Nat.fib n ^ 2

theorem Nat.fib_bit0_succ (n : ℕ) : Nat.fib (bit0 n + 1) = Nat.fib (n + 1) ^ 2 + Nat.fib n ^ 2

theorem Nat.fib_bit1_succ (n : ℕ) : Nat.fib (bit1 n + 1) = Nat.fib (n + 1) * (2 * Nat.fib n + Nat.fib (n + 1))

def Nat.fastFibAux : ℕ → ℕ × ℕ

Computes (Nat.fib n, Nat.fib (n + 1)) using the binary representation of n. Supports Nat.fastFib.

Equations

• One or more equations did not get rendered due to their size.

def Nat.fastFib (n : ℕ) : ℕ

Computes Nat.fib n using the binary representation of n. Proved to be equal to Nat.fib in Nat.fast_fib_eq.

Equations

• Nat.fastFib n = (Nat.fastFibAux n).1

theorem Nat.fast_fib_aux_bit_ff (n : ℕ) : Nat.fastFibAux (Nat.bit false n) = let p := Nat.fastFibAux n; (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

theorem Nat.fast_fib_aux_bit_tt (n : ℕ) : Nat.fastFibAux (Nat.bit true n) = let p := Nat.fastFibAux n; (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))

theorem Nat.fast_fib_aux_eq (n : ℕ) : Nat.fastFibAux n = (Nat.fib n, Nat.fib (n + 1))

theorem Nat.fast_fib_eq (n : ℕ) : Nat.fastFib n = Nat.fib n

theorem Nat.gcd_fib_add_self (m : ℕ) (n : ℕ) : Nat.gcd (Nat.fib m) (Nat.fib (n + m)) = Nat.gcd (Nat.fib m) (Nat.fib n)

theorem Nat.gcd_fib_add_mul_self (m : ℕ) (n : ℕ) (k : ℕ) : Nat.gcd (Nat.fib m) (Nat.fib (n + k * m)) = Nat.gcd (Nat.fib m) (Nat.fib n)

theorem Nat.fib_gcd (m : ℕ) (n : ℕ) : Nat.fib (Nat.gcd m n) = Nat.gcd (Nat.fib m) (Nat.fib n)

fib n is a strong divisibility sequence, see https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers

theorem Nat.fib_dvd (m : ℕ) (n : ℕ) (h : m ∣ n) : Nat.fib m ∣ Nat.fib n

theorem Nat.fib_succ_eq_sum_choose (n : ℕ) : Nat.fib (n + 1) = Finset.sum (Finset.antidiagonal n) fun (p : ℕ × ℕ) => Nat.choose p.1 p.2

theorem Nat.fib_succ_eq_succ_sum (n : ℕ) : Nat.fib (n + 1) = (Finset.sum (Finset.range n) fun (k : ℕ) => Nat.fib k) + 1