liquidhaskell-0.8.0.2: tests/strings/pos/DivideAndQunquer.hs
{-@ LIQUID "--higherorder" @-}
{-@ LIQUID "--totality" @-}
{-@ LIQUID "--exactdc" @-}
module DivideAndQunquer where
import Prelude hiding (mconcat, map, split, take, drop)
import Language.Haskell.Liquid.ProofCombinators
{-@ divideAndQunquer
:: f:(List i -> List o)
-> thm:(x1:List i -> x2:List i -> {f (append x1 x2) == append (f x1) (f x2)} )
-> is:List i
-> n:Int
-> m:Int
-> {f is == pmconcat m (map f (chunk n is))}
/ [llen is]
@-}
divideAndQunquer
:: (List i -> List o)
-> (List i -> List i -> Proof)
-> List i -> Int -> Int -> Proof
divideAndQunquer f thm is n m
= pmconcat m (map f (chunk n is))
==. mconcat (map f (chunk n is))
? pmconcatEquivalence m (map f (chunk n is))
==. f is
? distributeInput f thm is n
*** QED
{-@ distributeInput
:: f:(List i -> List o)
-> thm:(x1:List i -> x2:List i -> {f (append x1 x2) == append (f x1) (f x2)} )
-> is:List i
-> n:Int
-> {f is == mconcat (map f (chunk n is))}
/ [llen is]
@-}
distributeInput
:: (List i -> List o)
-> (List i -> List i -> Proof)
-> List i -> Int -> Proof
distributeInput f thm is n
| llen is <= n || n <= 1
= mconcat (map f (chunk n is))
==. mconcat (map f (C is N))
==. mconcat (f is `C` map f N)
==. mconcat (f is `C` N)
==. append (f is) (mconcat N)
==. append (f is) N
==. f is ? appendRightIdentity (f is)
*** QED
| otherwise
= mconcat (map f (chunk n is))
==. mconcat (map f (C (take n is) (chunk n (drop n is))))
==. mconcat (f (take n is) `C` map f (chunk n (drop n is)))
==. append (f (take n is)) (mconcat (map f (chunk n (drop n is))))
==. append (f (take n is)) (f (drop n is))
? distributeInput f thm (drop n is) n
==. f (append (take n is) (drop n is))
? thm (take n is) (drop n is)
==. f is
? appendTakeDrop n is
*** QED
pmconcatEquivalence ::Int -> List (List a) -> Proof
{-@ pmconcatEquivalence :: i:Int -> is:List (List a)
-> {pmconcat i is == mconcat is}
/ [llen is] @-}
pmconcatEquivalence i is
| i <= 1
= pmconcat i is ==. mconcat is *** QED
pmconcatEquivalence i N
= pmconcat i N
==. N
==. mconcat N
*** QED
pmconcatEquivalence i (C x N)
= pmconcat i (C x N)
==. x
==. append x N
? appendRightIdentity x
==. mconcat (C x (mconcat N))
==. mconcat (C x N)
*** QED
pmconcatEquivalence i xs
| llen xs <= i
= pmconcat i xs
==. pmconcat i (map mconcat (chunk i xs))
==. pmconcat i (map mconcat (C xs N))
==. pmconcat i (mconcat xs `C` map mconcat N)
==. pmconcat i (mconcat xs `C` N)
==. mconcat xs
*** QED
pmconcatEquivalence i xs
= pmconcat i xs
==. pmconcat i (map mconcat (chunk i xs))
==. mconcat (map mconcat (chunk i xs))
? pmconcatEquivalence i (map mconcat (chunk i xs))
==. mconcat xs
? mconcatAssoc i xs
*** QED
-------------------------------------------------------------------------------
----------- List Definition --------------------------------------------------
-------------------------------------------------------------------------------
{-@ data List [llen] a = N | C {lhead :: a, ltail :: List a} @-}
data List a = N | C a (List a)
llen :: List a -> Int
{-@ measure llen @-}
{-@ llen :: List a -> Nat @-}
llen N = 0
llen (C _ xs) = 1 + llen xs
-------------------------------------------------------------------------------
----------- List Manipulation ------------------------------------------------
-------------------------------------------------------------------------------
-- Distribution
{-@ reflect map @-}
{-@ map :: (a -> b) -> xs:List a -> {v:List b | llen v == llen xs } @-}
map :: (a -> b) -> List a -> List b
map _ N = N
map f (C x xs) = f x `C` map f xs
{-@ reflect chunk @-}
{-@ chunk :: i:Int -> xs:List a -> {v:List (List a) | if (i <= 1 || llen xs <= i) then (llen v == 1) else (llen v < llen xs) } / [llen xs] @-}
chunk :: Int -> List a -> List (List a)
chunk i xs
| i <= 1
= C xs N
| llen xs <= i
= C xs N
| otherwise
= C (take i xs) (chunk i (drop i xs))
{-@ reflect drop @-}
{-@ drop :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == llen xs - i } @-}
drop :: Int -> List a -> List a
drop i N = N
drop i (C x xs)
| i == 0
= C x xs
| otherwise
= drop (i-1) xs
{-@ reflect take @-}
{-@ take :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == i} @-}
take :: Int -> List a -> List a
take i N = N
take i (C x xs)
| i == 0
= N
| otherwise
= C x (take (i-1) xs)
-- Monoid
{-@ reflect mconcat @-}
mconcat :: List (List a) -> List a
mconcat N = N
mconcat (C x xs) = append x (mconcat xs)
{-@ reflect pmconcat @-}
pmconcat :: Int -> List (List a) -> List a
{-@ pmconcat :: i:Int -> is:List (List a) -> List a /[llen is] @-}
pmconcat i xs
| i <= 1
= mconcat xs
pmconcat i N
= N
pmconcat i (C x N)
= x
pmconcat i xs
= pmconcat i (map mconcat (chunk i xs))
{-@ reflect append @-}
append :: List a -> List a -> List a
append N ys = ys
append (C x xs) ys = x `C` (append xs ys)
-------------------------------------------------------------------------------
----------- Helper Theorems --------------------------------------------------
-------------------------------------------------------------------------------
-- List is a Monoid
appendRightIdentity :: List a -> Proof
{-@ appendRightIdentity :: xs:List a -> { append xs N == xs } @-}
appendRightIdentity N
= append N N ==. N *** QED
appendRightIdentity (C x xs)
= append (C x xs) N
==. C x (append xs N) ? appendRightIdentity xs
==. C x xs
*** QED
appendAssoc :: List a -> List a -> List a -> Proof
{-@ appendAssoc :: x:List a -> y:List a -> z:List a
-> {append (append x y) z == append x (append y z)} @-}
appendAssoc N y z
= append (append N y) z
-- ==. append y z
==. append N (append y z)
*** QED
appendAssoc (C x xs) y z
= append (append (C x xs) y) z
==. append (x `C` (append xs y)) z
==. x `C` (append (append xs y) z)
==. x `C` (append xs (append y z))
? appendAssoc xs y z
==. append (C x xs) (append y z)
*** QED
-- | Monoid implications
mconcatAssocOne :: Int -> List (List a) -> Proof
{-@ mconcatAssocOne :: i:Nat -> xs:{List (List a) | i <= llen xs}
-> {mconcat xs == append (mconcat (take i xs)) (mconcat (drop i xs))}
/[i]
@-}
mconcatAssocOne i N
= append (mconcat (take i N)) (mconcat (drop i N))
==. append (mconcat N) (mconcat N)
==. append N N
-- ? leftIdentity N
==. N
==. mconcat N
*** QED
mconcatAssocOne i (C x xs)
| i == 0
= append (mconcat (take i (C x xs))) (mconcat (drop i (C x xs)))
==. append (mconcat N) (mconcat (C x xs))
==. append N (mconcat (C x xs))
==. mconcat (C x xs)
-- ? leftIdentity (C x xs)
*** QED
| otherwise
= append (mconcat (take i (C x xs))) (mconcat (drop i (C x xs)))
==. append (mconcat (C x (take (i-1) xs))) (mconcat (drop (i-1) xs))
==. append (append x (mconcat (take (i-1) xs))) (mconcat (drop (i-1) xs))
? appendAssoc x (mconcat (take (i-1) xs)) (mconcat (drop (i-1) xs))
==. append x (append (mconcat (take (i-1) xs)) (mconcat (drop (i-1) xs)))
? mconcatAssocOne (i-1) xs
==. append x (mconcat xs)
==. mconcat (C x xs)
*** QED
-- Generalization to chunking
mconcatAssoc :: Int -> List (List a) -> Proof
{-@ mconcatAssoc ::
i:Int -> xs:List (List a)
-> { mconcat xs == mconcat (map mconcat (chunk i xs))}
/ [llen xs] @-}
mconcatAssoc i xs
| i <= 1 || llen xs <= i
= mconcat (map mconcat (chunk i xs))
==. mconcat (map mconcat (C xs N))
==. mconcat (mconcat xs `C` map mconcat N)
==. mconcat (mconcat xs `C` N)
==. append (mconcat xs) (mconcat N)
==. append (mconcat xs) N
==. mconcat xs
? appendRightIdentity (mconcat xs)
*** QED
| otherwise
= mconcat (map mconcat (chunk i xs))
==. mconcat (map mconcat (take i xs `C` chunk i (drop i xs)))
==. mconcat (mconcat (take i xs) `C` map mconcat (chunk i (drop i xs)))
==. append (mconcat (take i xs)) (mconcat (map mconcat (chunk i (drop i xs))))
==. append (mconcat (take i xs)) (mconcat (drop i xs))
? mconcatAssoc i (drop i xs)
==. mconcat xs
? mconcatAssocOne i xs
*** QED
-- | For input Distribution
{-@ appendTakeDrop :: i:Nat -> xs:{List a | i <= llen xs}
-> {xs == append (take i xs) (drop i xs) } @-}
appendTakeDrop :: Int -> List a -> Proof
appendTakeDrop i N
= append (take i N) (drop i N)
==. append N N
==. N
*** QED
appendTakeDrop i (C x xs)
| i == 0
= append (take 0 (C x xs)) (drop 0 (C x xs))
==. append N (C x xs)
==. C x xs
*** QED
| otherwise
= append (take i (C x xs)) (drop i (C x xs))
==. append (C x (take (i-1) xs)) (drop (i-1) xs)
==. C x (append (take (i-1) xs) (drop (i-1) xs))
==. C x xs ? appendTakeDrop (i-1) xs
*** QED