------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive "natural" numbers
------------------------------------------------------------------------

module Data.Conat where

open import Coinduction
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary

------------------------------------------------------------------------
-- The type

data Coℕ : Set where
  zero : Coℕ
  suc  : (n : ∞ Coℕ) → Coℕ

------------------------------------------------------------------------
-- Some operations

fromℕ : ℕ → Coℕ
fromℕ zero    = zero
fromℕ (suc n) = suc (♯ fromℕ n)

∞ℕ : Coℕ
∞ℕ = suc (♯ ∞ℕ)

infixl  _+_
infixl  _*_

_+_ : Coℕ → Coℕ → Coℕ
zero  + n = n
suc m + n = suc (♯ (♭ m + n))

_*_ : Coℕ → Coℕ → Coℕ
zero  * n = zero
suc m * n = go n module Star where
  go  : Coℕ → Coℕ
  go' : Coℕ → Coℕ

  go zero    = zero
  go (suc m) = go' (♭ m)

  go' zero    = suc (♯ (♭ m * n))
  go' (suc m) = suc (♯ go' (♭ m))

-- fromℕ 1 * zero ≡ zero
-- ∞ℕ * zero ↝ loop
-- (1 + m)*(1 + n) = 2 + m + n + m*n

toℕ : ℕ → Coℕ → ℕ
toℕ zero m = zero
toℕ (suc n) zero = zero
toℕ (suc n) (suc m) = suc (toℕ n (♭ m))

------------------------------------------------------------------------
-- Equality

infix  _≈_

data _≈_ : Coℕ → Coℕ → Set where
  zero :                                 zero  ≈ zero
  suc  : ∀ {m n} (m≈n : ∞ (♭ m ≈ ♭ n)) → suc m ≈ suc n

setoid : Setoid _ _
setoid = record
  { Carrier       = Coℕ
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≈_
  refl {zero}  = zero
  refl {suc n} = suc (♯ refl)

  sym : Symmetric _≈_
  sym zero      = zero
  sym (suc m≈n) = suc (♯ sym (♭ m≈n))

  trans : Transitive _≈_
  trans zero      zero      = zero
  trans (suc m≈n) (suc n≈k) = suc (♯ trans (♭ m≈n) (♭ n≈k))