Conjecture.agda

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Bool
open import Data.Sum


record Stream (A : Set) : Set where
  coinductive
  field
    hd  : A
    tl  : Stream A
open Stream

even? : ℕ → Bool
even? zero           = true
even? (suc zero)     = false
even? (suc (suc n))  = even? n

step : ℕ → ℕ
step 1 = 1
step n with even? n
… | true  = ⌊ n /2⌋
… | false  = 3 * n + 1

collatz : ℕ → Stream ℕ
hd (collatz n)  = n
tl (collatz n)  = collatz (step n)

record Loops {A : Set} (xs : Stream A) : Set where
  coinductive
  field
    loop : hd xs ≡ hd (tl xs) ⊎ Loops (tl xs)
open Loops

conjecture : ∀ n → Loops (collatz n)
loop (conjecture zero) = inj₁ refl
loop (conjecture (suc n)) = inj₂ (conjecture (step (suc n)))