module Quox.FinExtra

import public Data.Fin
import Quox.Decidable

public export
data LT : Rel (Fin n) where
  LTZ : FZ `LT` FS i
  LTS : i `LT` j -> FS i `LT` FS j
%builtin Natural FinExtra.LT
%name FinExtra.LT lt

public export %inline
GT : Rel (Fin n)
GT = flip LT

export
Transitive (Fin n) LT where
  transitive LTZ     (LTS _) = LTZ
  transitive (LTS p) (LTS q) = LTS $ transitive p q

export Uninhabited (i `FinExtra.LT` i) where uninhabited (LTS p) = uninhabited p
export Uninhabited (FS i `LT` FZ) where uninhabited _ impossible


public export
data Compare : Rel (Fin n) where
  IsLT : (lt : i `LT` j) -> Compare i j
  IsEQ :                    Compare i i
  IsGT : (gt : i `GT` j) -> Compare i j
%name Compare cmp

export
compareS : Compare i j -> Compare (FS i) (FS j)
compareS (IsLT lt) = IsLT (LTS lt)
compareS IsEQ      = IsEQ
compareS (IsGT gt) = IsGT (LTS gt)

export
compareP : (i, j : Fin n) -> Compare i j
compareP FZ     FZ     = IsEQ
compareP FZ     (FS j) = IsLT LTZ
compareP (FS i) FZ     = IsGT LTZ
compareP (FS i) (FS j) = compareS $ compareP i j