module Data.Nat.Base where
import Level using (zero)
open import Relation.Binary.Core
open import Relation.Nullary using (¬_)
infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_
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 ℕ #-}
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
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
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
pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n
infixl 7 _⊓_
infixl 6 _+⋎_ _⊔_
_+⋎_ : ℕ → ℕ → ℕ
zero +⋎ n = n
suc m +⋎ n = suc (n +⋎ m)
_⊔_ : ℕ → ℕ → ℕ
zero ⊔ n = n
suc m ⊔ zero = suc m
suc m ⊔ suc n = suc (m ⊔ n)
_⊓_ : ℕ → ℕ → ℕ
zero ⊓ n = zero
suc m ⊓ zero = zero
suc m ⊓ suc n = suc (m ⊓ n)
⌊_/2⌋ : ℕ → ℕ
⌊ 0 /2⌋ = 0
⌊ 1 /2⌋ = 0
⌊ suc (suc n) /2⌋ = suc ⌊ n /2⌋
⌈_/2⌉ : ℕ → ℕ
⌈ n /2⌉ = ⌊ suc n /2⌋