mathlib3 documentation

data.nat.fib

The Fibonacci Sequence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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  :
@[simp]
theorem nat.fib_one  :
@[simp]
theorem nat.fib_two  :
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_le_fib_succ {n : } :
theorem nat.fib_pos {n : } (n_pos : 0 < n) :
theorem nat.fib_lt_fib_succ {n : } (hn : 2 n) :
nat.fib n < nat.fib (n + 1)
theorem nat.fib_add_two_strict_mono  :
strict_mono (λ (n : ), nat.fib (n + 2))

fib (n + 2) is strictly monotone.

theorem nat.le_fib_self {n : } (five_le_n : 5 n) :
theorem nat.fib_coprime_fib_succ (n : ) :
(nat.fib n).coprime (nat.fib (n + 1))

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

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_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))

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

Equations
def nat.fast_fib (n : ) :

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

Equations
theorem nat.fast_fib_aux_bit_ff (n : ) :
(nat.bit bool.ff n).fast_fib_aux = let p : × := n.fast_fib_aux in (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2)
theorem nat.fast_fib_aux_bit_tt (n : ) :
(nat.bit bool.tt n).fast_fib_aux = let p : × := n.fast_fib_aux in (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
theorem nat.fast_fib_aux_eq (n : ) :
theorem nat.fast_fib_eq (n : ) :
theorem nat.gcd_fib_add_self (m n : ) :
(nat.fib m).gcd (nat.fib (n + m)) = (nat.fib m).gcd (nat.fib n)
theorem nat.gcd_fib_add_mul_self (m n k : ) :
(nat.fib m).gcd (nat.fib (n + k * m)) = (nat.fib m).gcd (nat.fib n)
theorem nat.fib_gcd (m n : ) :
nat.fib (m.gcd n) = (nat.fib m).gcd (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) :
theorem nat.fib_succ_eq_succ_sum (n : ) :
nat.fib (n + 1) = (finset.range n).sum (λ (k : ), nat.fib 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 norm_num.is_fib_aux (n a b : ) :
Prop

Auxiliary definition for prove_fib plugin.

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

prove_fib_aux ic n returns (ic', a, b, ⊢ is_fib_aux n a b), where n is a numeral.

A norm_num plugin for fib n when n is a numeral. Uses the binary representation of n like nat.fast_fib.

A norm_num plugin for fib n when n is a numeral. Uses the binary representation of n like nat.fast_fib.