Fold duality theorems proved in Liquid Haskell - (from An introduction to functional programming Richard Bird, Philip Wadler)

Proof.hs

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


import Language.Haskell.Liquid.ProofCombinators
import Prelude hiding (flip, foldl, foldr, reverse, (++))

{-@ reflect foldr @-}
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f a [] = a
foldr f a (x : xs) = f x (foldr f a xs)

{-@ reflect foldl @-}
foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f a [] = a
foldl f a (x : xs) = foldl f (f a x) xs

-- first duality theorem

{-@ t1 :: op:(a -> a -> a) ->
        v:a ->
          xs:[a] ->
            distr:(x:a -> y:a -> z:a -> {op x (op y z) = op (op x y) z}) ->
            commL:(x:a -> {op v x = x}) ->
            commR:(x:a -> {op x v = x}) ->
            {foldr op v xs == foldl op v xs} @-}
t1 :: (a -> a -> a) -> a -> [a] -> (a -> a -> a -> ()) -> (a -> ()) -> (a -> ()) -> ()
t1 op v [] dist commL commR =
  foldr op v [] === v === foldl op v [] *** QED
t1 op v [x] dist commL commR =
  foldr op v [x]
    === op x (foldr op v [])
    === op x v
    ? commR x
    === x
    ? commL x
    === op v x
    === foldl op (op v x) []
    === foldl op v [x]
    *** QED
t1 op v (x : xs) dist commL commR =
  foldr op v (x : xs)
    === op x (foldr op v xs)
    ? t1 op v xs dist commL commR
    === op x (foldl op v xs)
    ? t1lemma op dist x v xs
    === foldl op (op x v) xs
    ? commR x
    === foldl op x xs
    ? commL x
    === foldl op (op v x) xs
    === foldl op v (x : xs)
    *** QED

{-@
t1lemma ::
        f:(a -> a -> a)
    ->  assoc : (x:a -> y:a -> z:a -> { f x (f y z) = f (f x y) z } )
    ->  x:a
    ->  y:a
    ->  xs:[a]
    ->  { f x (foldl f y xs) = foldl f (f x y) xs }
@-}
t1lemma :: (a -> a -> a) -> (a -> a -> a -> Proof) -> a -> a -> [a] -> Proof
t1lemma f assoc x y [] =
  f x (foldl f y [])
    === f x y
    === foldl f (f x y) []
    *** QED
t1lemma f assoc x y (z : zs) =
  f x (foldl f y (z : zs))
    === f x (foldl f (f y z) zs)
    ? t1lemma f assoc x (f y z) zs
    === foldl f (f x (f y z)) zs
    ? assoc x y z
    === foldl f (f (f x y) z) zs
    === foldl f (f x y) (z : zs)
    *** QED

-- first duality theorem by using that is is a generalization of the third
{-@ t1_by_t2 :: op:(a -> a -> a) ->
        v:a ->
          xs:[a] ->
            distr:(x:a -> y:a -> z:a -> {op x (op y z) = op (op x y) z}) ->
            comm:(x:a -> {op x v = x && op v x = x}) ->
            {foldr op v xs == foldl op v xs} @-}
t1_by_t2 :: (a -> a -> a) -> a -> [a] -> (a -> a -> a -> ()) -> (a -> ()) -> ()
t1_by_t2 op v xs dist comm = t2 op op v xs dist comm

-- second duality theorem
{-@ t2 :: op:(a -> b -> b) ->
        op2:(b -> a -> b) ->
        v:b ->
          xs:[a] ->
            distr:(x:a -> y:b -> z:a -> {op x (op2 y z) = op2 (op x y) z}) ->
            comm:(x:a -> {op x v = op2 v x}) ->
            {foldr op v xs == foldl op2 v xs} @-}
t2 :: (a -> b -> b) -> (b -> a -> b) -> b -> [a] -> (a -> b -> a -> ()) -> (a -> ()) -> ()
t2 op op2 v [] dist comm =
  foldr op v [] === v === foldl op2 v [] *** QED
t2 op op2 v (x : xs) dist comm =
  foldr op v (x : xs)
    === op x (foldr op v xs)
    ? t2 op op2 v xs dist comm
    === op x (foldl op2 v xs)
    ? oplemma x op op2 v xs dist
    === foldl op2 (op x v) xs
    ? comm x
    === foldl op2 (op2 v x) xs
    === foldl op2 v (x : xs)
    *** QED

{-@ oplemma :: y:a -> op:(a -> b -> b) -> op2:(b -> a -> b) -> v:b -> xs:[a] ->
            distr:(x:a -> y:b -> z:a -> {op x (op2 y z) = op2 (op x y) z}) ->
              {
                (op y (foldl op2 v xs)) = (foldl op2 (op y v) xs)
              }
@-}
oplemma :: a -> (a -> b -> b) -> (b -> a -> b) -> b -> [a] -> (a -> b -> a -> ()) -> ()
oplemma y op op2 v [] distr =
  op y (foldl op2 v [])
    === op y v
    === (foldl op2 (op y v) [])
    *** QED
oplemma y op op2 v (x : xs) distr =
  op y (foldl op2 v (x : xs))
    === op y (foldl op2 (op2 v x) xs)
    ? oplemma y op op2 (op2 v x) xs distr
    === foldl op2 (op y (op2 v x)) xs
    ? distr y v x
    === foldl op2 (op2 (op y v) x) xs
    === foldl op2 (op y v) (x : xs)
    *** QED

-- third duality lemma

{-@ reflect flip @-}
flip f a b = f b a

{-@ reflect ++ @-}
{-@ infixr ++ @-}
[] ++ xs = xs
(x : xs) ++ ys = x : xs ++ ys

{-@ reflect reverse @-}
reverse [] = []
reverse (x : xs) = reverse xs ++ [x]

{-@ foldllem :: f:(b-> a -> b) -> a:b -> xs:[a] -> ys:[a] -> {foldl f a (xs ++ ys) = foldl f (foldl f a xs) ys} @-}
foldllem :: (b -> a -> b) -> b -> [a] -> [a] -> ()
foldllem f v [] ys =
  foldl f v ([] ++ ys)
    === foldl f v ys
    === foldl f (foldl f v []) ys
    *** QED
foldllem f v (x : xs) ys =
  foldl f v ((x : xs) ++ ys)
    === foldl f v (x : (xs ++ ys))
    === foldl f (f v x) (xs ++ ys)
    ? foldllem f (f v x) xs ys
    === foldl f (foldl f (f v x) xs) ys
    === foldl f (foldl f v (x : xs)) ys
    *** QED

-- third duality theorem
{-@ t3 :: op:(a -> b -> b) ->
        v:b ->
          xs:[a] ->
            {foldr op v xs == foldl (flip op) v (reverse xs)} @-}
t3 :: (a -> b -> b) -> b -> [a] -> ()
t3 op v [] =
  foldr op v []
    === v
    === foldl (flip op) v (reverse [])
    *** QED
t3 op v (x : xs) =
  foldr op v (x : xs)
    === op x (foldr op v xs)
    ? t3 op v xs
    === op x (foldl fop v (reverse xs))
    === fop (foldl fop v (reverse xs)) x
    === foldl fop (foldl fop v (reverse xs)) [x]
    ? foldllem fop v (reverse xs) [x]
    === foldl fop v (reverse xs ++ [x])
    === foldl fop v (reverse (x : xs))
    *** QED
 where
  fop = flip op