module Control.Total

-- Antisymmetricity (Reflexivity also follows)
public export
interface Ord ty => AntiSym ty where
    antisym : (x,y:ty) -> (compare x y) = contra (compare y x)

export
possibles : Ordering -> Ordering -> Type
possibles LT GT = Void
possibles GT LT = Void
possibles _ _ = ()

-- Transitivity
public export
interface Ord ty => Trans ty where
    trans : (x,y,z:ty) -> {auto p: possibles (compare x y) (compare y z)} -> compare x y <+> compare y z = compare x z

public export
interface (AntiSym ty, Trans ty) => Total ty where

export
AntiSym Nat where
    antisym 0 0 = Refl
    antisym 0 (S k) = Refl
    antisym (S k) 0 = Refl
    antisym (S k) (S j) = antisym k j

export
Trans Nat where
    trans 0 0 0 = Refl
    trans 0 0 (S _) = Refl
    trans 0 (S _) (S _) = Refl
    trans (S _) 0 0 = Refl
    trans (S i) (S j) 0 with (compare i j)
        _ | EQ = Refl
        _ | GT = Refl
    trans (S i) (S j) (S k) = trans i j k

export
Total Nat where