BetterRefl.idr

data SignedNat : Bool -> Nat -> Type where
  Neg : (n:Nat) -> SignedNat True n
  Pos : (n:Nat) -> SignedNat False n

interface MagnitudeSN sn where
  magSN : sn -> Nat

implementation MagnitudeSN (SignedNat True Z) where
  magSN _ = Z

implementation (MagnitudeSN (SignedNat True n)) => MagnitudeSN (SignedNat True (S n)) where
  magSN (Neg (S n)) = S (magSN (Neg n))

implementation MagnitudeSN (SignedNat False Z) where
  magSN _ = Z

implementation (MagnitudeSN (SignedNat False n)) => MagnitudeSN (SignedNat False (S n)) where
  magSN (Pos (S n)) = S (magSN (Pos n))

interface GreaterSN sna snb where
  gtrSN : sna -> snb -> Bool

implementation GreaterSN (SignedNat False Z) (SignedNat True Z) where
  gtrSN _ _ = False

implementation GreaterSN (SignedNat False (S _)) (SignedNat True _) where
  gtrSN _ _ = True

implementation GreaterSN (SignedNat True _) (SignedNat False _) where
  gtrSN _ _ = False

implementation GreaterSN (SignedNat False Z) (SignedNat False _) where
  gtrSN _ _ = False

implementation GreaterSN (SignedNat False (S a)) (SignedNat False Z) where
  gtrSN _ _ = True

implementation (GreaterSN (SignedNat False a) (SignedNat False b)) => GreaterSN (SignedNat False (S a)) (SignedNat False (S b)) where
  gtrSN (Pos (S a)) (Pos (S b)) = gtrSN (Pos a) (Pos b)

implementation GreaterSN (SignedNat True _) (SignedNat True Z) where
  gtrSN _ _ = False

implementation GreaterSN (SignedNat True Z) (SignedNat True (S a)) where
  gtrSN _ _ = True

implementation (GreaterSN (SignedNat True a) (SignedNat True b)) => GreaterSN (SignedNat True (S a)) (SignedNat True (S b)) where
  gtrSN (Neg (S a)) (Neg (S b)) = gtrSN (Neg a) (Neg b)

proveNeg15GreaterThanNeg30 : gtrSN (Neg 15) (Neg 30) = True
proveNeg15GreaterThanNeg30 = Refl