Some liquid-haskell proofs

power.hs

-- Proof that even powers of integers are natural.
{-@ powEven :: {a:Int | a /= 0} -> {b:Nat | b mod 2 = 0} -> Nat / [b] @-}
powEven :: Int -> Int -> Int
powEven a 0 = 1
powEven a b = a * a * powEven a (b - 2)

{-@ powOdd :: {a:Int | a /= 0} -> {k:Nat | k mod 2 == 1} -> Int / [k] @-}
powOdd :: Int -> Int -> Int
powOdd a 1 = a
powOdd a b = a * a * powOdd a (b - 2)

{-@ powDerived :: {a:Int | a /= 0} -> k:Nat -> Int / [k] @-}
powDerived :: Int -> Int -> Int
powDerived a b
  | b `mod` 2 == 0 = powEven a b
  | b `mod` 2 == 1 = powOdd a b

-- Will not be derived. Not that smart. See dependent types research, Agda, Coq and Idris.
-- {-@ pow2 :: {a:Int | a /= 0} -> {k:Nat | k == 2} -> Nat / [k] @-}
-- pow2 a b = powDerived a 2

-- Proof that exponentiating with natural power terminates with standard recursive definition.
{-@ powInt :: {a:Int | a /= 0} -> b:Nat -> Int / [b] @-}
powInt :: Int -> Int -> Int
powInt a 0 = 1
powInt a b = a * powInt a (b-1)

-- Same proof with zero case
{-@ powInt0 :: a:Int -> b:Nat -> Int / [b] @-}
powInt0 :: Int -> Int -> Int
powInt0 0 _ = 1
powInt0 a 0 = 1
powInt0 a b = a * powInt0 a (b-1)

-- Inequality - number above zero in negative integral power is below zero. Strictly.
{-@ powSpec :: {a:Double | a > 1 } -> {b:Int | b < 0} -> {r:Double | r < 1} / [0 - b] @-}
powSpec :: Double -> Int -> Double
powSpec a (-1) = 1 / a
powSpec a b = powSpec a (b + 1) / a

-- Exponentiating to integral power terminates always by abs(b) - lacking feature.
{-@ pow :: a -> b:Int -> a / [b*b] @-}
pow :: (Ord a, Fractional a, Num a) => a -> Int -> a
pow 0 _ = 1
pow a 0 = 1
pow a b
  | b > 0 = a * pow a (b - 1)
  | b < 0 = pow a (b + 1) / a

-- If it does not need to terminate, it will not be forced.
{-@ lazy powUn @-}
powUn :: (Ord a, Fractional a, Num a) => a -> Int -> a
powUn 0 _ = 1
powUn a 0 = 1
powUn a b
  | b > 0 = a * powUn a (b - 1)
  | b < 0 = powUn a (b + 1) / a