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

source
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
source
@[simp]
theorem nat.fib_zero  :
nat.fib 0 = 0
source
@[simp]
theorem nat.fib_one  :
nat.fib 1 = 1
source
@[simp]
theorem nat.fib_two  :
nat.fib 2 = 1
source
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ₙ₊₁.

source
theorem nat.fib_le_fib_succ {n : ℕ} :
nat.fib n ≤ nat.fib (n + 1)
source
theorem nat.fib_mono  :
monotone nat.fib
source
theorem nat.fib_pos {n : ℕ} (n_pos : 0 < n) :
0 < nat.fib n
source
theorem nat.fib_add_two_sub_fib_add_one {n : ℕ} :
nat.fib (n + 2) - nat.fib (n + 1) = nat.fib n
source
theorem nat.fib_lt_fib_succ {n : ℕ} (hn : 2 ≤ n) :
nat.fib n < nat.fib (n + 1)
source
theorem nat.fib_add_two_strict_mono  :
strict_mono (λ (n : ℕ), nat.fib (n + 2))

fib (n + 2) is strictly monotone.

source
theorem nat.le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) :
n ≤ nat.fib n
source
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

source
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

source
theorem nat.fib_two_mul (n : ℕ) :
nat.fib (2 * n) = nat.fib n * (2 * nat.fib (n + 1) - nat.fib n)
source
theorem nat.fib_two_mul_add_one (n : ℕ) :
nat.fib (2 * n + 1) = nat.fib (n + 1) ^ 2 + nat.fib n ^ 2
source
theorem nat.fib_bit0 (n : ℕ) :
nat.fib (bit0 n) = nat.fib n * (2 * nat.fib (n + 1) - nat.fib n)
source
theorem nat.fib_bit1 (n : ℕ) :
nat.fib (bit1 n) = nat.fib (n + 1) ^ 2 + nat.fib n ^ 2
source
theorem nat.fib_bit0_succ (n : ℕ) :
nat.fib (bit0 n + 1) = nat.fib (n + 1) ^ 2 + nat.fib n ^ 2
source
theorem nat.fib_bit1_succ (n : ℕ) :
nat.fib (bit1 n + 1) = nat.fib (n + 1) * (2 * nat.fib n + nat.fib (n + 1))
source
def nat.fast_fib_aux  :
ℕ → ℕ × ℕ

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

Equations
source
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
source
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)
source
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))
source
theorem nat.fast_fib_aux_eq (n : ℕ) :
n.fast_fib_aux = (nat.fib n, nat.fib (n + 1))
source
theorem nat.fast_fib_eq (n : ℕ) :
n.fast_fib = nat.fib n
source
theorem nat.gcd_fib_add_self (m n : ℕ) :
(nat.fib m).gcd (nat.fib (n + m)) = (nat.fib m).gcd (nat.fib n)
source
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)
source
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

source
theorem nat.fib_dvd (m n : ℕ) (h : m ∣ n) :
nat.fib m ∣ nat.fib n
source
theorem nat.fib_succ_eq_sum_choose (n : ℕ) :
nat.fib (n + 1) = (finset.nat.antidiagonal n).sum (λ (p : ℕ × ℕ), p.fst.choose p.snd)
source
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.

source
def norm_num.is_fib_aux (n a b : ℕ) :
Prop

Auxiliary definition for prove_fib plugin.

Equations
source
theorem norm_num.is_fib_aux_one  :
norm_num.is_fib_aux 1 1 1
source
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') :
norm_num.is_fib_aux (bit0 n) a' b'
source
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') :
norm_num.is_fib_aux (bit1 n) a' b'
source
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'
source
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'
source
meta def norm_num.prove_fib_aux (ic : tactic.instance_cache) :
expr → tactic (tactic.instance_cache × expr × expr × expr)

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

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

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

source
meta def norm_num.eval_fib  :
expr → tactic (expr × expr)

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