The Kolakoski sequence

module elementary-number-theory.kolakoski-sequence where
Imports
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strong-induction-natural-numbers

open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types

Idea

The Kolakoski sequence

1,2,2,1,1,2,1,2,2,1,2,2,1,1,...

is a self-referential sequence of 1s and 2s which is the flattening of a sequence

(1),(2,2),(1,1),(2),(1),(2,2),(1,1)

of sequences of repeated 1s and 2s such that the n-th element in the Kolakoski sequence describes the length of the n-th element of the above sequence of sequences.

Definition

The following definition of the Kolakoski sequence is due to Léo Elouan.

kolakoski-helper-inductive :
  (n : ) 
  ((i : )  i ≤-ℕ n  bool × (bool × (Σ   j  j ≤-ℕ i)))) 
  bool × (bool × (Σ   j  j ≤-ℕ (succ-ℕ n))))
kolakoski-helper-inductive n f with f n (refl-leq-ℕ n)
... | b , false , i , H = b , true , i , preserves-leq-succ-ℕ i n H
... | b , true , i , H with f i H
... | true , true , j , K = neg-bool b , true , succ-ℕ i , H
... | true , false , j , K = neg-bool b , false , succ-ℕ i , H
... | false , true , j , K = neg-bool b , false , succ-ℕ i , H
... | false , false , j , K = neg-bool b , true , succ-ℕ i , H

kolakoski-helper : (n : )  bool × (bool × Σ   i  i ≤-ℕ n))
kolakoski-helper =
  strong-ind-ℕ
    ( λ n  bool × (bool × Σ   j  j ≤-ℕ n)))
    ( false , true , 0 , refl-leq-ℕ 0)
    ( λ n f  kolakoski-helper-inductive n f)

kolakoski :   
kolakoski n with pr1 (kolakoski-helper n)
... | true = 2
... | false = 1