The Fibonacci sequence

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

Created on 2022-01-26.
Last modified on 2023-09-11.

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

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

Recent changes

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).
2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).