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 #

• 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.fast_fib). 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_le_fib_succ {n : } :
nat.fib (n + 1)
theorem nat.fib_mono  :
theorem nat.fib_pos {n : } (n_pos : 0 < n) :
0 <
nat.fib (n + 2) - nat.fib (n + 1) =
theorem nat.fib_lt_fib_succ {n : } (hn : 2 n) :
< nat.fib (n + 1)
strict_mono (λ (n : ), nat.fib (n + 2))

fib (n + 2) is strictly monotone.

theorem nat.le_fib_self {n : } (five_le_n : 5 n) :
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_add (m n : ) :
nat.fib (m + n + 1) = * + nat.fib (m + 1) * nat.fib (n + 1)
theorem nat.fib_two_mul (n : ) :
nat.fib (2 * 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 + ^ 2
theorem nat.fib_bit0 (n : ) :
nat.fib (bit0 n) = * (2 * nat.fib (n + 1) - nat.fib n)
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
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 : ) :
= 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 : ) :
= 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_sum_choose (n : ) :
nat.fib (n + 1) = (λ (p : × ), p.fst.choose p.snd)
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 : b) (h1 : a + c = bit0 b) (h2 : a * c = a') (h3 : a * a = a2) (h4 : b * b = b2) (h5 : a2 + b2 = b') :
a' b'
theorem norm_num.is_fib_aux_bit1 {n a b c a2 b2 a' b' : } (H : b) (h1 : a * a = a2) (h2 : b * b = b2) (h3 : a2 + b2 = a') (h4 : bit0 a + b = c) (h5 : b * c = b') :
a' b'
theorem norm_num.is_fib_aux_bit0_done {n a b c a' : } (H : 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 : 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.

meta def norm_num.prove_fib (ic : tactic.instance_cache) (e : expr) :

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.