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

{-# OPTIONS --without-K --guardedness --sized-types #-}

module Codata.Musical.Conat where

open import Codata.Musical.Notation
open import Data.Nat.Base using (; zero; suc)
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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

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

module Coℕ-injective where

 suc-injective :  {m n}  (Coℕ  suc m)  suc n  m  n
 suc-injective P.refl = P.refl

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

pred : Coℕ  Coℕ
pred zero    = zero
pred (suc n) =  n

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

fromℕ-injective :  {m n}  fromℕ m  fromℕ n  m  n
fromℕ-injective {zero}  {zero}  eq = P.refl
fromℕ-injective {suc m} {suc n} eq = P.cong suc (fromℕ-injective (P.cong pred eq))

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

infixl 6 _+_

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

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

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

module ≈-injective where

 suc-injective :  {m n p q}  (suc m  suc n  suc p)  suc q  p  q
 suc-injective P.refl = P.refl

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

------------------------------------------------------------------------
-- Legacy

import Codata.Conat as C
open import Codata.Thunk
import Size

fromMusical :  {i}  Coℕ  C.Conat i
fromMusical zero    = C.zero
fromMusical (suc n) = C.suc λ where .force  fromMusical ( n)

toMusical : C.Conat Size.∞  Coℕ
toMusical C.zero    = zero
toMusical (C.suc n) = suc ( toMusical (n .force))