module MoreNat where

open import Data.Empty
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties

-------------------------------------------------------------------------------
-- Swap ordering
-------------------------------------------------------------------------------

swap : ∀ {m n} → Ordering m n → Ordering n m
swap {m} (less .m k) = greater m k
swap {.n} {n} (equal .n) = equal n
swap {.(suc (n + k))} {n} (greater .n k) = less n k

swap-swap : ∀ {m n} (c : Ordering m n) → swap (swap c) ≡ c
swap-swap {m} (less .m k) = refl
swap-swap {.n} {n} (equal .n) = refl
swap-swap {.(suc (n + k))} {n} (greater .n k) = refl

-------------------------------------------------------------------------------
-- Equal
-------------------------------------------------------------------------------

ordering-≡-equal : {n : ℕ} {c : Ordering n n} → c ≡ equal n
ordering-≡-equal {n} {c} = ordering-≡-equal-gen c refl
  where
    ordering-≡-equal-gen :
      ∀ {m n} (c : Ordering m n) → (h : n ≡ m)
      → subst (Ordering m) h c ≡ equal m
    ordering-≡-equal-gen (less m k) h = ⊥-elim (m≢1+m+n m (sym h))
    ordering-≡-equal-gen (equal n) refl = refl
    ordering-≡-equal-gen (greater n k) h = ⊥-elim (m≢1+m+n _ h)

-------------------------------------------------------------------------------
-- Less
-------------------------------------------------------------------------------

ordering-≡-less : ∀ {m k} (c : Ordering m (1 + m + k)) → c ≡ less m k
ordering-≡-less {m} {k} c = ordering-≡-less-gen c k refl
  where
    -- K is used as workaround for a problematic case analysis below.
    -- Can we do better than this?
    K : ∀ {ℓ} {A : Set ℓ} {x : A} (h : x ≡ x) → refl ≡ h
    K refl = refl

    lemma : ∀ {n k k₁} → n ≢ 2 + n + k + k₁
    lemma {0} ()
    lemma {suc m} h = lemma {m} (cong pred h)

    ordering-≡-less-gen :
      ∀ {m n} (c : Ordering m n) k (h : n ≡ 1 + m + k)
      → subst (Ordering m) h c ≡ less m k
    ordering-≡-less-gen (less m k) k₁ h with cancel-+-left (1 + m) h
    ordering-≡-less-gen (less m k₁) .k₁ h | refl =
      subst (λ h₁ → subst (Ordering m) h₁ (less m k₁) ≡ less m k₁) (K h) refl
    ordering-≡-less-gen (equal n) k h = ⊥-elim (m≢1+m+n n h)
    ordering-≡-less-gen (greater n k) k₁ h = ⊥-elim (lemma h)

-------------------------------------------------------------------------------
-- Greater
-------------------------------------------------------------------------------

ordering-≡-greater : ∀ {m k} (c : Ordering (suc (m + k)) m) → c ≡ greater m k
ordering-≡-greater {m} {k} c =
  subst (λ c → c ≡ greater m k)
        (swap-swap c)
        (cong swap (ordering-≡-less (swap c)))

-------------------------------------------------------------------------------
-- Uniqueness
-------------------------------------------------------------------------------

ordering-uniqueness : {m n : ℕ} {x y : Ordering m n} → x ≡ y
ordering-uniqueness {x = less m k} {y} = sym (ordering-≡-less y)
ordering-uniqueness {x = equal n} {y} = sym ordering-≡-equal
ordering-uniqueness {x = greater n k} {y} = sym (ordering-≡-greater y)

-------------------------------------------------------------------------------
-- Corollaries / tests
-------------------------------------------------------------------------------

private

  compare-refl : {n : ℕ} → compare n n ≡ equal n
  compare-refl = ordering-uniqueness

  compare-less : {m k : ℕ} → compare m (1 + m + k) ≡ less m k
  compare-less = ordering-uniqueness

  compare-greater : {n k : ℕ} → compare (1 + n + k) n ≡ greater n k
  compare-greater = ordering-uniqueness