{-# OPTIONS --without-K --safe #-}
module Data.Nat.Base where
open import Data.Bool.Base using (Bool; true; false; T; not)
open import Level using (0ℓ)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; _≢_; refl)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation.Core using (contradiction)
open import Relation.Unary using (Pred)
open import Agda.Builtin.Nat public
using (zero; suc) renaming (Nat to ℕ)
open import Agda.Builtin.Nat public
using () renaming (_==_ to _≡ᵇ_)
open import Agda.Builtin.Nat public
using () renaming (_<_ to _<ᵇ_)
infix 4 _≤ᵇ_
_≤ᵇ_ : (m n : ℕ) → Bool
zero ≤ᵇ n = true
suc m ≤ᵇ n = m <ᵇ n
infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_
data _≤_ : Rel ℕ 0ℓ where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
_<_ : Rel ℕ 0ℓ
m < n = suc m ≤ n
_≥_ : Rel ℕ 0ℓ
m ≥ n = n ≤ m
_>_ : Rel ℕ 0ℓ
m > n = n < m
_≰_ : Rel ℕ 0ℓ
a ≰ b = ¬ a ≤ b
_≮_ : Rel ℕ 0ℓ
a ≮ b = ¬ a < b
_≱_ : Rel ℕ 0ℓ
a ≱ b = ¬ a ≥ b
_≯_ : Rel ℕ 0ℓ
a ≯ b = ¬ a > b
record NonZero (n : ℕ) : Set where
field
nonZero : T (not (n ≡ᵇ 0))
instance
nonZero : ∀ {n} → NonZero (suc n)
nonZero = _
≢-nonZero : ∀ {n} → n ≢ 0 → NonZero n
≢-nonZero {zero} 0≢0 = contradiction refl 0≢0
≢-nonZero {suc n} n≢0 = _
>-nonZero : ∀ {n} → n > 0 → NonZero n
>-nonZero (s≤s 0<n) = _
≢-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n ≢ 0
≢-nonZero⁻¹ (suc n) ()
>-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0
>-nonZero⁻¹ (suc n) = s≤s z≤n
open import Agda.Builtin.Nat public
using (_+_; _*_) renaming (_-_ to _∸_)
pred : ℕ → ℕ
pred n = n ∸ 1
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⌋
_^_ : ℕ → ℕ → ℕ
x ^ zero = 1
x ^ suc n = x * x ^ n
∣_-_∣ : ℕ → ℕ → ℕ
∣ zero - y ∣ = y
∣ x - zero ∣ = x
∣ suc x - suc y ∣ = ∣ x - y ∣
infix 4 _≤′_ _<′_ _≥′_ _>′_
data _≤′_ (m : ℕ) : ℕ → Set where
≤′-refl : m ≤′ m
≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
_<′_ : Rel ℕ 0ℓ
m <′ n = suc m ≤′ n
_≥′_ : Rel ℕ 0ℓ
m ≥′ n = n ≤′ m
_>′_ : Rel ℕ 0ℓ
m >′ n = n <′ m
record _≤″_ (m n : ℕ) : Set where
constructor less-than-or-equal
field
{k} : ℕ
proof : m + k ≡ n
infix 4 _≤″_ _<″_ _≥″_ _>″_
_<″_ : Rel ℕ 0ℓ
m <″ n = suc m ≤″ n
_≥″_ : Rel ℕ 0ℓ
m ≥″ n = n ≤″ m
_>″_ : Rel ℕ 0ℓ
m >″ n = n <″ m
data _≤‴_ : ℕ → ℕ → Set where
≤‴-refl : ∀{m} → m ≤‴ m
≤‴-step : ∀{m n} → suc m ≤‴ n → m ≤‴ n
infix 4 _≤‴_ _<‴_ _≥‴_ _>‴_
_<‴_ : Rel ℕ 0ℓ
m <‴ n = suc m ≤‴ n
_≥‴_ : Rel ℕ 0ℓ
m ≥‴ n = n ≤‴ m
_>‴_ : Rel ℕ 0ℓ
m >‴ n = n <‴ m
data Ordering : Rel ℕ 0ℓ where
less : ∀ m k → Ordering m (suc (m + k))
equal : ∀ m → Ordering m m
greater : ∀ m k → Ordering (suc (m + k)) m
compare : ∀ m n → Ordering m n
compare zero zero = equal zero
compare (suc m) zero = greater zero m
compare zero (suc n) = less zero n
compare (suc m) (suc n) with compare m n
... | less m k = less (suc m) k
... | equal m = equal (suc m)
... | greater n k = greater (suc n) k