module ordering where

{-
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
-}

open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥)
open import Relation.Nullary using (¬_)
open import Data.Sum using (_⊎_; inj₁; inj₂)

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

2≤4 : 2 ≤ 4
2≤4 = s≤s (s≤s z≤n)

¬4≤2 : ¬ (4 ≤ 2)
¬4≤2 (s≤s (s≤s ()))

≤-refl : ∀ {n : ℕ} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s (≤-refl {n})

≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans z≤n _ = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

≤-trans′ : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans′ {.0} {n} {p} z≤n _ = z≤n
≤-trans′ {.(suc _)} {.(suc _)} {.(suc _)} (s≤s m≤n) (s≤s n≤p)
 = s≤s (≤-trans m≤n n≤p)

≤-total : ∀ (m n : ℕ) → (m ≤ n) ⊎ (n ≤ m)
≤-total zero n = inj₁ z≤n
≤-total (suc m) zero = inj₂ z≤n
≤-total (suc m) (suc n) with ≤-total m n
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ n≤m = inj₂ (s≤s n≤m)

-- < is defined quite simply in terms of ≤
_<_ : ℕ → ℕ → Set
m < n = suc m ≤ n

data Dec (P : Set) : Set where
  yes : P   → Dec P
  no  : ¬ P → Dec P

¬s≤z : ∀ (n : ℕ) → ¬ (suc n ≤ zero)
¬s≤z n ()

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s ¬m≤n (s≤s m≤n) = ¬m≤n m≤n

≤? : ∀ (m n : ℕ) → Dec (m ≤ n)
≤? zero n = yes z≤n
≤? (suc m) zero = no (¬s≤z m)
≤? (suc m) (suc n) with ≤? m n
... | yes p = yes (s≤s p)
... | no np = no (¬s≤s np)