The Fibonacci sequence

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-01-26.
Last modified on 2024-10-16.

module elementary-number-theory.fibonacci-sequence where

Imports

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.greatest-common-divisor-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.relatively-prime-natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.transport-along-identifications

Idea

The Fibonacci sequence^¶ is a recursively defined sequence of natural numbers given by the equations

  Fₙ₊₂ = Fₙ₊₁ + Fₙ,   where F₀ = 0 and F₁ = 1

A number in this sequence is called a Fibonacci number^¶. The first few Fibonacci numbers are

  n    0   1   2   3   4   5   6   7   8   9
  Fₙ   0   1   1   2   3   5   8  13  21  34

Definitions

The standard definition using pattern matching

Fibonacci-ℕ : ℕ → ℕ
Fibonacci-ℕ 0 = 0
Fibonacci-ℕ (succ-ℕ 0) = 1
Fibonacci-ℕ (succ-ℕ (succ-ℕ n)) = (Fibonacci-ℕ (succ-ℕ n)) +ℕ (Fibonacci-ℕ n)

A definition using the induction principle of `ℕ`

The above definition of the Fibonacci sequence uses Agda’s powerful pattern matching definitions. Below, we will give a definition of the Fibonacci sequence in terms of ind-ℕ.

The problem with defining the Fibonacci sequence using ind-ℕ, is that ind-ℕ doesn’t give us a way to refer to both (F n) and (F (succ-ℕ n)). So, we have to give a workaround, where we store two values in the Fibonacci sequence at once.

The basic idea is that we define a sequence of pairs of integers, which will be consecutive Fibonacci numbers. This would be a function of type $N \to N^{2}$ .

Such a function is easy to give with induction, using the map $N^{2} \to N^{2}$ that takes a pair (m,n) to the pair (n,n+m). Starting the iteration with (0,1) we obtain the Fibonacci sequence by taking the first projection.

However, we haven’t defined cartesian products or booleans yet. Therefore we mimic the above idea, using $N \to N$ instead of $N^{2}$ .

shift-one : ℕ → (ℕ → ℕ) → (ℕ → ℕ)
shift-one n f = ind-ℕ n (λ x y → f x)

shift-two : ℕ → ℕ → (ℕ → ℕ) → (ℕ → ℕ)
shift-two m n f = shift-one m (shift-one n f)

Fibo-zero-ℕ : ℕ → ℕ
Fibo-zero-ℕ = shift-two 0 1 (λ x → 0)

Fibo-succ-ℕ : (ℕ → ℕ) → (ℕ → ℕ)
Fibo-succ-ℕ f = shift-two (f 1) ((f 1) +ℕ (f 0)) (λ x → 0)

Fibo-function : ℕ → ℕ → ℕ
Fibo-function =
  ind-ℕ
    ( Fibo-zero-ℕ)
    ( λ n → Fibo-succ-ℕ)

Fibo : ℕ → ℕ
Fibo k = Fibo-function k 0

Properties

`F(m+n+1) ＝ F(m+1)F(n+1) + F(m)F(n)`

Fibonacci-add-ℕ :
  (m n : ℕ) →
  Fibonacci-ℕ (m +ℕ (succ-ℕ n)) ＝
  ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n))) +ℕ
  ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ n))
Fibonacci-add-ℕ m zero-ℕ =
  ap-add-ℕ
    ( inv (right-unit-law-mul-ℕ (Fibonacci-ℕ (succ-ℕ m))))
    ( inv (right-zero-law-mul-ℕ (Fibonacci-ℕ m)))
Fibonacci-add-ℕ m (succ-ℕ n) =
  ( ap Fibonacci-ℕ (inv (left-successor-law-add-ℕ m (succ-ℕ n)))) ∙
  ( Fibonacci-add-ℕ (succ-ℕ m) n) ∙
  ( ap
    ( _+ℕ ((Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n)))
    ( right-distributive-mul-add-ℕ
      ( Fibonacci-ℕ (succ-ℕ m))
      ( Fibonacci-ℕ m)
      ( Fibonacci-ℕ (succ-ℕ n)))) ∙
  ( associative-add-ℕ
    ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
    ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
    ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n))) ∙
  ( ap
    ( ((Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n))) +ℕ_)
    ( commutative-add-ℕ
      ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
      ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n)))) ∙
  ( inv
    ( associative-add-ℕ
      ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
      ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n))
      ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n))))) ∙
  ( ap
    ( _+ℕ ((Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n))))
    ( inv
      ( left-distributive-mul-add-ℕ
        ( Fibonacci-ℕ (succ-ℕ m))
        ( Fibonacci-ℕ (succ-ℕ n))
        ( Fibonacci-ℕ n))))

Consecutive Fibonacci numbers are relatively prime

is-one-div-fibonacci-succ-div-fibonacci-ℕ :
  (d n : ℕ) → div-ℕ d (Fibonacci-ℕ n) → div-ℕ d (Fibonacci-ℕ (succ-ℕ n)) →
  is-one-ℕ d
is-one-div-fibonacci-succ-div-fibonacci-ℕ d zero-ℕ H K = is-one-div-one-ℕ d K
is-one-div-fibonacci-succ-div-fibonacci-ℕ d (succ-ℕ n) H K =
  is-one-div-fibonacci-succ-div-fibonacci-ℕ d n
    ( div-right-summand-ℕ d (Fibonacci-ℕ (succ-ℕ n)) (Fibonacci-ℕ n) H K)
    ( H)

relatively-prime-fibonacci-fibonacci-succ-ℕ :
  (n : ℕ) → is-relatively-prime-ℕ (Fibonacci-ℕ n) (Fibonacci-ℕ (succ-ℕ n))
relatively-prime-fibonacci-fibonacci-succ-ℕ n =
  is-one-div-fibonacci-succ-div-fibonacci-ℕ
    ( gcd-ℕ (Fibonacci-ℕ n) (Fibonacci-ℕ (succ-ℕ n)))
    ( n)
    ( div-left-factor-gcd-ℕ (Fibonacci-ℕ n) (Fibonacci-ℕ (succ-ℕ n)))
    ( div-right-factor-gcd-ℕ (Fibonacci-ℕ n) (Fibonacci-ℕ (succ-ℕ n)))

A 3-for-2 property of divisibility of Fibonacci numbers

We prove that if an two of the following three properties hold, then so does the third:

d | Fibonacci-ℕ m
d | Fibonacci-ℕ n
d | Fibonacci-ℕ (m +ℕ n).

div-Fibonacci-add-ℕ :
  (d m n : ℕ) → div-ℕ d (Fibonacci-ℕ m) → div-ℕ d (Fibonacci-ℕ n) →
  div-ℕ d (Fibonacci-ℕ (m +ℕ n))
div-Fibonacci-add-ℕ d m zero-ℕ H1 H2 = H1
div-Fibonacci-add-ℕ d m (succ-ℕ n) H1 H2 =
  tr
    ( div-ℕ d)
    ( inv (Fibonacci-add-ℕ m n))
    ( div-add-ℕ d
      ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
      ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ n))
      ( div-mul-ℕ (Fibonacci-ℕ (succ-ℕ m)) d (Fibonacci-ℕ (succ-ℕ n)) H2)
      ( tr
        ( div-ℕ d)
        ( commutative-mul-ℕ (Fibonacci-ℕ n) (Fibonacci-ℕ m))
        ( div-mul-ℕ (Fibonacci-ℕ n) d (Fibonacci-ℕ m) H1)))

If `m | n`, then `d | F(m)` implies `d | F(n)`

div-Fibonacci-div-ℕ :
  (d m n : ℕ) → div-ℕ m n → div-ℕ d (Fibonacci-ℕ m) → div-ℕ d (Fibonacci-ℕ n)
div-Fibonacci-div-ℕ d m .zero-ℕ (zero-ℕ , refl) H = div-zero-ℕ d
div-Fibonacci-div-ℕ d zero-ℕ .(k *ℕ zero-ℕ) (succ-ℕ k , refl) H =
  tr
    ( div-ℕ d)
    ( ap Fibonacci-ℕ (inv (right-zero-law-mul-ℕ (succ-ℕ k))))
    ( div-zero-ℕ d)
div-Fibonacci-div-ℕ d (succ-ℕ m) ._ (succ-ℕ k , refl) H =
  div-Fibonacci-add-ℕ d
    ( k *ℕ (succ-ℕ m))
    ( succ-ℕ m)
    ( div-Fibonacci-div-ℕ d
      ( succ-ℕ m)
      ( k *ℕ (succ-ℕ m))
      ( pair k refl)
      ( H))
    ( H)

Fibonacci-ℕ is an order preserving map on ℕ ordered by divisibility

preserves-div-Fibonacci-ℕ :
  (m n : ℕ) → div-ℕ m n → div-ℕ (Fibonacci-ℕ m) (Fibonacci-ℕ n)
preserves-div-Fibonacci-ℕ m n H =
  div-Fibonacci-div-ℕ (Fibonacci-ℕ m) m n H (refl-div-ℕ (Fibonacci-ℕ m))

External links

Fibonacci sequence at Mathswitch
Fibonacci number at Mathswitch
Fibonacci sequence at Wikipedia
A000045 in the OEIS

Recent changes

2024-10-16. Fredrik Bakke. Some links in elementary number theory (#1199).
2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
2023-05-22. Fredrik Bakke, Victor Blanchi, Egbert Rijke and Jonathan Prieto-Cubides. Pre-commit stuff (#627).
2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).