------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers, basic types and operations
------------------------------------------------------------------------

module Data.Nat.Base where

import Level using (zero)
open import Relation.Binary.Core
import Relation.Binary.PropositionalEquality.TrustMe as TrustMe
open import Relation.Nullary using (¬_)

infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_

------------------------------------------------------------------------
-- The types

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

data _≤_ : Rel  Level.zero where
  z≤n :  {n}                  zero   n
  s≤s :  {m n} (m≤n : m  n)  suc m  suc n

{-# BUILTIN NATURAL  #-}
{-# COMPILED_DATA_UHC  __NAT__ __ZERO__ __SUC__ #-}

infixl 6 _+_ _∸_
infixl 7 _*_

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

{-# BUILTIN NATPLUS _+_ #-}

_∸_ :     
m      zero  = m
zero   suc n = zero
suc m  suc n = m  n

{-# BUILTIN NATMINUS _∸_ #-}

_*_ :     
zero  * n = zero
suc m * n = n + m * n

{-# BUILTIN NATTIMES _*_ #-}

_<_ : Rel  Level.zero
m < n = suc m  n

_≥_ : Rel  Level.zero
m  n = n  m

_>_ : Rel  Level.zero
m > n = n < m

_≰_ : Rel  Level.zero
a  b = ¬ a  b

_≮_ : Rel  Level.zero
a  b = ¬ a < b

_≱_ : Rel  Level.zero
a  b = ¬ a  b

_≯_ : Rel  Level.zero
a  b = ¬ a > b

-- The following, alternative definition of _≤_ is more suitable for
-- well-founded induction (see Induction.Nat).

infix 4 _≤′_ _<′_ _≥′_ _>′_

data _≤′_ (m : ) :   Set where
  ≤′-refl :                         m ≤′ m
  ≤′-step :  {n} (m≤′n : m ≤′ n)  m ≤′ suc n

_<′_ : Rel  Level.zero
m <′ n = suc m ≤′ n

_≥′_ : Rel  Level.zero
m ≥′ n = n ≤′ m

_>′_ : Rel  Level.zero
m >′ n = n <′ m

-- Another alternative definition of _≤_.

record _≤″_ (m n : ) : Set where
  constructor less-than-or-equal
  field
    {k}   : 
    proof : m + k  n

infix 4 _≤″_ _<″_ _≥″_ _>″_

_<″_ : Rel  Level.zero
m <″ n = suc m ≤″ n

_≥″_ : Rel  Level.zero
m ≥″ n = n ≤″ m

_>″_ : Rel  Level.zero
m >″ n = n <″ m

erase :  {m n}  m ≤″ n  m ≤″ n
erase (less-than-or-equal eq) = less-than-or-equal (TrustMe.erase eq)

------------------------------------------------------------------------
-- A generalisation of the arithmetic operations

fold : {a : Set}  a  (a  a)    a
fold z s zero    = z
fold z s (suc n) = s (fold z s n)

module GeneralisedArithmetic {a : Set} (0# : a) (1+ : a  a) where

  add :   a  a
  add n z = fold z 1+ n

  mul : (+ : a  a  a)  (  a  a)
  mul _+_ n x = fold 0#  s  x + s) n

------------------------------------------------------------------------
-- Arithmetic

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

infixl 7 _⊓_
infixl 6 _+⋎_ _⊔_

-- Argument-swapping addition. Used by Data.Vec._⋎_.

_+⋎_ :     
zero  +⋎ n = n
suc m +⋎ n = suc (n +⋎ m)

-- Max.

_⊔_ :     
zero   n     = n
suc m  zero  = suc m
suc m  suc n = suc (m  n)

-- Min.

_⊓_ :     
zero   n     = zero
suc m  zero  = zero
suc m  suc n = suc (m  n)

-- Division by 2, rounded downwards.

⌊_/2⌋ :   
 0 /2⌋           = 0
 1 /2⌋           = 0
 suc (suc n) /2⌋ = suc  n /2⌋

-- Division by 2, rounded upwards.

⌈_/2⌉ :   
 n /2⌉ =  suc n /2⌋