Collatz.agda

module Collatz where

open import Coinduction
open import Data.Colist using (Colist; []; _∷_; take)
open import Data.Nat using (ℕ; zero; suc; _*_)
open import Data.Nat.Divisibility using (divides; _∣?_)
open import Data.Nat.Properties using (strictTotalOrder)
open import Function
open import Relation.Binary using (DecSetoid; StrictTotalOrder)
open import Relation.Nullary using (Dec; yes; no)

module Iterate {c ℓ} (A : DecSetoid c ℓ) where
  open DecSetoid A renaming (Carrier to C)

  iterate-trace : (C → C) → C → Colist C
  iterate-trace f x = iterate-trace-with f x x
    where
    iterate-trace-with : (C → C) → C → C → Colist C
    iterate-trace-with f z x with z ≟ f x
    ... | yes p = []
    ... | no ¬p = x ∷ ♯ iterate-trace-with f x (f x)

open StrictTotalOrder strictTotalOrder
open Iterate decSetoid

collatz : ℕ → ℕ
collatz zero = zero
collatz (suc zero) = suc zero
collatz (suc (suc x)) =
  let n = suc (suc x) in
  case 2 ∣? n of λ
  { (yes (divides q eq)) → q
  ; (no ¬p) → suc (3 * n)
  }

test : Colist ℕ
test = {!take 100 $ iterate-trace collatz 7!}