{-# OPTIONS --universe-polymorphism #-}
module Data.Nat.NP where
open import Data.Nat public
open import Data.Nat.Properties as Props
open import Data.Bool
open import Data.Empty using (⊥-elim)
open import Function
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.PropositionalEquality as ≡
open ≡ using (_≡_)
suc-injective : ∀ {n m : ℕ} → (suc n ∶ ℕ) ≡ suc m → n ≡ m
suc-injective ≡.refl = ≡.refl
_==_ : (x y : ℕ) → Bool
zero == zero = true
zero == suc _ = false
suc _ == zero = false
suc m == suc n = m == n
module == where
_≈_ : (m n : ℕ) → Set
m ≈ n = T (m == n)
subst : ∀ {ℓ} → Substitutive _≈_ ℓ
subst _ {zero} {zero} _ = id
subst P {suc _} {suc _} p = subst (P ∘ suc) p
subst _ {zero} {suc _} ()
subst _ {suc _} {zero} ()
sound : ∀ m n → T (m == n) → m ≡ n
sound m n p = subst (_≡_ m) p ≡.refl
refl : Reflexive _≈_
refl {zero} = _
refl {suc n} = refl {n}
sym : Symmetric _≈_
sym {m} {n} eq rewrite sound m n eq = refl {n}
trans : Transitive _≈_
trans {m} {n} {o} m≈n n≈o rewrite sound m n m≈n | sound n o n≈o = refl {o}
isEquivalence : IsEquivalence _≈_
isEquivalence = record { refl = λ {x} → refl {x}
; sym = λ {x} {y} → sym {x} {y}
; trans = λ {x} {y} {z} → trans {x} {y} {z} }
setoid : Setoid _ _
setoid = record { Carrier = ℕ; _≈_ = _≈_ ; isEquivalence = isEquivalence }
_<=_ : (x y : ℕ) → Bool
zero <= _ = true
suc _ <= zero = false
suc m <= suc n = m <= n
module <= where
sound : ∀ m n → T (m <= n) → m ≤ n
sound zero _ _ = z≤n
sound (suc m) (suc n) p = s≤s (sound m n p)
sound (suc m) zero ()
complete : ∀ {m n} → m ≤ n → T (m <= n)
complete z≤n = _
complete (s≤s m≤n) = complete m≤n
private
module ℕcmp = StrictTotalOrder Props.strictTotalOrder
module ℕ≤ = DecTotalOrder decTotalOrder
¬≤ : ∀ {m n} → ¬(m < n) → n ≤ m
¬≤ {m} {n} p with ℕcmp.compare m n
... | tri< m<n _ _ = ⊥-elim (p m<n)
... | tri≈ _ eq _ = ℕ≤.reflexive (≡.sym eq)
... | tri> _ _ 1+n≤m = ≤-pred (Props.≤-steps 1 1+n≤m)