# Documentation

Mathlib.Data.Nat.Fib

# 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
@[simp]
theorem Nat.fib_zero :
= 0
@[simp]
theorem Nat.fib_one :
= 1
@[simp]
theorem Nat.fib_two :
= 1
theorem Nat.fib_add_two {n : } :
Nat.fib (n + 2) = + Nat.fib (n + 1)

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

theorem Nat.fib_pos {n : } (n_pos : 0 < n) :
0 <
theorem Nat.fib_lt_fib_succ {n : } (hn : 2 n) :
< Nat.fib (n + 1)

fib (n + 2) is strictly monotone.

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

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 + 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) = * (2 * Nat.fib (n + 1) - )
theorem Nat.fib_two_mul_add_one (n : ) :
Nat.fib (2 * n + 1) = Nat.fib (n + 1) ^ 2 + ^ 2
theorem Nat.fib_bit0 (n : ) :
Nat.fib (bit0 n) = * (2 * Nat.fib (n + 1) - )
theorem Nat.fib_bit1 (n : ) :
Nat.fib (bit1 n) = Nat.fib (n + 1) ^ 2 + ^ 2
theorem Nat.fib_bit0_succ (n : ) :
Nat.fib (bit0 n + 1) = Nat.fib (n + 1) ^ 2 + ^ 2
theorem Nat.fib_bit1_succ (n : ) :
Nat.fib (bit1 n + 1) = Nat.fib (n + 1) * (2 * + Nat.fib (n + 1))

Computes (nat.fib n, nat.fib (n + 1)) using the binary representation of n. Supports nat.fast_fib.

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
• = ().fst
theorem Nat.fast_fib_aux_bit_ff (n : ) :
= let p := ; (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2)
theorem Nat.fast_fib_aux_bit_tt (n : ) :
= let p := ; (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
theorem Nat.fast_fib_aux_eq (n : ) :
= (, Nat.fib (n + 1))
theorem Nat.gcd_fib_add_self (m : ) (n : ) :
Nat.gcd () (Nat.fib (n + m)) = Nat.gcd () ()
theorem Nat.gcd_fib_add_mul_self (m : ) (n : ) (k : ) :
Nat.gcd () (Nat.fib (n + k * m)) = Nat.gcd () ()
theorem Nat.fib_gcd (m : ) (n : ) :
Nat.fib (Nat.gcd m n) = Nat.gcd () ()

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) :
theorem Nat.fib_succ_eq_sum_choose (n : ) :
Nat.fib (n + 1) = Finset.sum () fun p => Nat.choose p.fst p.snd
theorem Nat.fib_succ_eq_succ_sum (n : ) :
Nat.fib (n + 1) = (Finset.sum () fun k => ) + 1

### norm_num plugin for fib#

The norm_num plugin uses a strategy parallel to that of nat.fast_fib, but it instead produces proofs of what nat.fib evaluates to.

def NormNum.IsFibAux (n : ) (a : ) (b : ) :

Auxiliary definition for prove_fib plugin.

Equations
theorem NormNum.is_fib_aux_bit0 {n : } {a : } {b : } {c : } {a2 : } {b2 : } {a' : } {b' : } (H : ) (h1 : a + c = bit0 b) (h2 : a * c = a') (h3 : a * a = a2) (h4 : b * b = b2) (h5 : a2 + b2 = b') :
theorem NormNum.is_fib_aux_bit1 {n : } {a : } {b : } {c : } {a2 : } {b2 : } {a' : } {b' : } (H : ) (h1 : a * a = a2) (h2 : b * b = b2) (h3 : a2 + b2 = a') (h4 : bit0 a + b = c) (h5 : b * c = b') :
theorem NormNum.is_fib_aux_bit0_done {n : } {a : } {b : } {c : } {a' : } (H : ) (h1 : a + c = bit0 b) (h2 : a * c = a') :
Nat.fib (bit0 n) = a'
theorem NormNum.is_fib_aux_bit1_done {n : } {a : } {b : } {a2 : } {b2 : } {a' : } (H : ) (h1 : a * a = a2) (h2 : b * b = b2) (h3 : a2 + b2 = a') :
Nat.fib (bit1 n) = a'