Rotate proof

Rotate.hs

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}

module Rotate where

import Language.Haskell.Liquid.ProofCombinators

{-@ measure length' @-}
{-@ length' :: [a] -> Nat @-}
length' :: [a] -> Int
length' []     = 0
length' (x:xs) = 1 + length' xs

{-@ reflect take' @-}
{-@ take' :: n:Nat -> { xs:[a] | length' xs >= n } -> { xs:[a] | length' xs = n } @-}
take' :: Int -> [a] -> [a]
take' 0 xs     = []
take' n (x:xs) = x : take' (n - 1) xs

{-@ reflect drop' @-}
{-@ drop' :: n:Nat -> { xs:[a] | length' xs >= n } -> { ys:[a] | length' ys = length' xs -n } @-}
drop' :: Int -> [a] -> [a]
drop' 0 xs     = xs
drop' n (x:xs) = drop' (n - 1) xs

{-@ reflect concat' @-}
concat' :: [a] -> [a] -> [a]
concat' []     ys = ys
concat' (x:xs) ys = x : concat' xs ys

{-@ reflect rotate @-}
{-@ rotate :: n:Nat -> { xs:[a] | length' xs >= n } -> [a] @-}
rotate :: Int -> [a] -> [a]
rotate n xs = concat' (drop' (length' xs - n) xs) (take' (length' xs - n) xs)

{-@ reflect lookup' @-}
{-@ lookup' :: n:Nat -> { xs:[a] | length' xs > n } -> a @-}
lookup' :: Int -> [a] -> a
lookup' 0 (x:xs) = x
lookup' n (x:xs) = lookup' (n - 1) xs

{-@ rotateCorrect :: o:Nat -> i:Nat -> { xs:[a] | i < length' xs && o <= length' xs }
                  -> { lookup' i xs = lookup' (i + o mod length' xs) (rotate o xs) } @-}
rotateCorrect :: Int -> Int -> [a] -> Proof
rotateCorrect o i xs | i >= length' xs - o = trivial
  ? lookupConcatLeft (drop' (length' xs - o) xs) (take' (length' xs - o) xs) (i - (length' xs - o))
  ? lookupDrop xs (length' xs - o) i
rotateCorrect o i xs | i <  length' xs - o = trivial
  ? lookupConcatRight (drop' (length' xs - o) xs) (take' (length' xs - o) xs) (i + o)
  ? lookupTake xs (length' xs - o) i

{-@ lookupConcatRight :: xs:[a] -> ys:[a] -> { n:Nat | n < length' xs + length' ys && n >= length' xs }
                 ->  { lookup' n (concat' xs ys) = lookup' (n - length' xs) ys } @-}
lookupConcatRight :: [a] -> [a] -> Int -> Proof
lookupConcatRight []     ys n = trivial
lookupConcatRight (x:xs) ys n = trivial ? lookupConcatRight xs ys (n - 1)

{-@ lookupConcatLeft :: xs:[a] -> ys:[a] -> { n:Nat | n < length' xs }
                 ->  { lookup' n (concat' xs ys) = lookup' n xs } @-}
lookupConcatLeft :: [a] -> [a] -> Int -> Proof
lookupConcatLeft []     ys n = trivial
lookupConcatLeft xs     ys 0 = trivial
lookupConcatLeft (x:xs) ys n = trivial ? lookupConcatLeft xs ys (n - 1)

{-@ lookupDrop :: xs:[a] -> { n:Nat | n <= length' xs } -> { i:Nat | i >= n && i < length' xs }
              -> { lookup' i xs = lookup' (i - n) (drop' n xs) } @-}
lookupDrop :: [a] -> Int -> Int -> Proof
lookupDrop xs     0 i = trivial
lookupDrop (x:xs) n i = lookupDrop xs (n - 1) (i - 1)

{-@ lookupTake :: xs:[a] -> { n:Nat | n <= length' xs } -> { i:Nat | i < n }
               -> { lookup' i xs = lookup' i (take' n xs) } @-}
lookupTake :: [a] -> Int -> Int -> Proof
lookupTake (x:xs) n 0 = trivial
lookupTake (x:xs) n i = trivial ? lookupTake xs (n - 1) (i - 1)