content: {-@ LIQUID "--reflection" @-}
  {-@ LIQUID "--ple" @-}
  
  -- | This module proves that unoptimized implementations of
  -- 'Data.List.permutations' are equivalent to the optimized
  -- implementation in [1].
  --
  -- Additionally, this module offers a proof of an approximation of the
  -- laziness requirement on permutations. See 'lemmaPermutationsDecomposition'.
  --
  -- [1] https://gitlab.haskell.org/ghc/ghc/-/blob/aec5a443bc45ca99cfeedc1777edb0aceca142cf/libraries/base/Data/OldList.hs#L1263
  --
  module Permutations where
  
  import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(Admit, QED), (?), pleUnfold)
  
  -- We need to redefine operations from the base package in order to
  -- have PLE reason with them. PLE is one of the algorithms in
  -- liquid-fixpoint that unfolds definitions automatically in proofs.
  --
  -- Therefore, we hide here the definitions comming from the Prelude.
  -- In an ideal world, we would be able to use the original definitions
  -- from base, and still would be able to use PLE.
  --
  import Prelude hiding ((!!), (++), asTypeOf, concat, const, drop, foldr, id, map, take, reverse)
  
  -- The following infixr directives are processed by Liquid Haskell.
  --
  -- They instruct the parser about the fixity and associativity of
  -- operators when reading specifications.
  --
  {-@ infixr 5 ++ @-}
  {-@ infixr 5 : @-}
  {-@ infixl 9 !! @-}
  
  
  -- We write first the definition of the optimized permutations.
  --
  -- The implementation in base uses local definitions in where clauses.
  -- We split it here in top-level functions to better reason about
  -- them in isolation. But it is possible to give Liquid Haskell
  -- specifications to local functions as well.
  
  -- Liquid Haskell requires functions to be terminating, in order
  -- to ensure soundness of the verified specifications.
  --
  -- We disable the termination checker with the lazy directive though.
  -- The termination checker is a bit tricky to convince once we start
  -- adding lemmas that refer to permutations calls in their parameters.
  --
  -- The termination of permutations is checked
  -- [here](https://github.com/ucsd-progsys/liquidhaskell/blob/d20d80d53949efbb7d2ac6eb1509a0ec822d3bea/tests/pos/Permutation.hs)
  -- though.
  --
  {-@ lazy permutations @-}
  {-@ reflect permutations @-}
  {-@ permutations :: ts:[a] -> [[a]] / [(len ts), 1, 0] @-}
  permutations :: [a] -> [[a]]
  permutations xs0 = xs0 : perms xs0 []
  
  -- @permutations xs0@ is equivalent to the following expressions
  --
  -- > xs0 : concat [ interleave (ts!!n) (drop (n+1) xs0) xs [] | n <- [0..len xs0 - 1], xs <- permutations (reverse (take n xs0)) ]
  -- > [ insertAt m (xs0!!n) xs ++ (drop (n+1) xs0) | n <- [0..len xs0 - 1], xs <- permutations (reverse (take n xs0)), m <- [0..len xs - 1] ]
  --
  
  
  -- | @perms ts is@ is equivalent to the following expressions
  --
  -- > concat [ interleave (ts!!n) (drop (n+1) ts) xs [] | n <- [0..len ts - 1], xs <- permutations (reverse (take n ts) ++ is) ]
  -- > [ insertAt m (ts!!n) xs ++ (drop (n+1) ts) | n <- [0..len ts - 1], xs <- permutations (reverse (take n ts) ++ is), m <- [0..len xs - 1] ]
  --
  -- The specification differs from this expressions in a few syntactic
  -- aspects.
  --
  -- 1) List ranges are not allowed in formulas. Therefore, we use the
  --    function 'fromTo'.
  -- 2) List comprehensions are not allowed in formulas. Therefore, we
  --    use functions 'concat' and 'map' instead.
  -- 3) Lambda expressions do not work well in formulas. Therefore, we
  --    use top-level functions 'aux1' and 'aux2' instead.
  
  {-@
  reflect perms
  perms
    :: ts:[a]
    -> is:[a]
    -> { v:[[a]]
       | v = concat (map (aux2 ts is) (fromTo 0 (len ts - 1)))
       } / [((len ts)+(len is)), 0, (len ts)]
  @-}
  perms :: [a] -> [a] -> [[a]]
  perms []     _  = []
  perms (t0:ts0) is =
      mapInterleave t0 ts0 (permutations is) (perms ts0 (t0:is))
      `const`
            lemmaMapAux2 t0 ts0 is 0 (length ts0 - 1)
      `const`
            lemmaAppendAssoc
               (concat (map (aux1 t0 ts0 []) (permutations is)))
               []
               (concat (map (aux2 (t0:ts0) is) (fromTo 1 (length (t0:ts0) - 1))))
       `const`
            mapInterleave t0 ts0 (permutations is) []
  
  -- For efficiency of the verification process, proofs are given in
  -- condensed form as above. The form starts from an expressions that
  -- is the result of the function, with multiple lemma applications
  -- appended with 'const'.
  --
  -- Discovering which lemma applications are needed is done by writing
  -- a longer step-by-step proof, where the need for each lemma can be
  -- observed between steps.
  --
  -- We start by writing the step-by-step proof, testing each new addition
  -- with Liquid Haskell. When we are finished, we comment out the
  -- step-by-step proof, and collect the lemmas into the condensed proof.
  --
  
  {-
      `asTypeOf`
      const (concat (map (aux1 t0 ts0 []) (permutations is)) ++ perms ts0 (t0:is))
            (mapInterleave t0 ts0 (permutations is) (perms ts0 (t0:is)))
      `asTypeOf`
      const (concat (map (aux1 t0 ts0 []) (permutations is)) ++ concat (map (aux2 ts0 (t0:is)) (fromTo 0 (length ts0 - 1))))
            (perms ts0 (t0:is))
      `asTypeOf`
      const (concat (map (aux1 t0 ts0 []) (permutations is)) ++ concat (map (aux2 (t0:ts0) is) (fromTo 1 (length (t0:ts0) - 1))))
            (lemmaMapAux2 t0 ts0 is 0 (length ts0 - 1))
      `asTypeOf`
            (concat (map (aux1 t0 ts0 []) (permutations is)) ++ ([] ++ concat (map (aux2 (t0:ts0) is) (fromTo 1 (length (t0:ts0) - 1)))))
      `asTypeOf`
       const ((concat (map (aux1 t0 ts0 []) (permutations is)) ++ []) ++ concat (map (aux2 (t0:ts0) is) (fromTo 1 (length (t0:ts0) - 1))))
            (lemmaAppendAssoc
               (concat (map (aux1 t0 ts0 []) (permutations is)))
               []
               (concat (map (aux2 (t0:ts0) is) (fromTo 1 (length (t0:ts0) - 1))))
            )
      `asTypeOf`
        (mapInterleave t0 ts0 (permutations is) [] ++ concat (map (aux2 (t0:ts0) is) (fromTo 1 (length (t0:ts0) - 1))))
      `asTypeOf`
        concat (map (aux2 (t0:ts0) is) (fromTo 0 (len (t0:ts0) - 1)))
  -}
  
  {-@
  reflect aux2
  aux2 :: ts:[a] -> [a] -> { n:Int | n < len ts && n >= 0 } -> [[a]]
  @-}
  aux2 :: [a] -> [a] -> Int -> [[a]]
  aux2 ts is n =
    mapInterleave (ts!!n) (drop (n+1) ts) (permutations (reverse (take n ts) ++ is)) []
  
  {-@ reflect aux0 @-}
  aux0 :: a -> ([a] -> b) -> [a] -> [a] -> Int -> b
  aux0 t f ys ts n = f (insertAt n t ys ++ ts)
  
  {-@ reflect aux1 @-}
  aux1 :: a -> [a] -> [[a]] -> [a] -> [[a]]
  aux1 t ts r p = interleave t ts p r
  
  -- | 'mapInterleave' is not part of the optimized definition of
  -- permutations. We factor it out from 'perms' to break down a
  -- bit the complexity of the verification.
  --
  -- @mapInterleave t ts ps r@ is equivalent to the expressions
  --
  -- > concat [ interleave t ts xs [] | xs <- ps ] ++ r
  -- > [ insertAt n t xs ++ ts | xs <- ps, n <- [0..len xs - 1] ] ++ r
  --
  
  {-@
  reflect mapInterleave
  mapInterleave
    :: t:a
    -> ts:[a]
    -> ps:[[a]]
    -> r:[[a]]
    -> { v:[[a]] | v == concat (map (aux1 t ts []) ps) ++ r }
  @-}
  mapInterleave :: a -> [a] -> [[a]] -> [[a]] -> [[a]]
  mapInterleave t ts ps r = foldr (interleave t ts) r ps `const` lemmaFoldrInterleave t ts ps r
  
  -- | @interleave t ts xs r@ is equivalent to the expression
  --
  -- > [ insertAt n t xs ++ ts | n <- [0..len xs - 1] ] ++ r
  --
  
  {-@
  reflect interleave
  interleave
    :: t:a
    -> ts:[a]
    -> xs:[a]
    -> r:[[a]]
    -> { v:[[a]] | v == map (aux0 t id xs ts) (fromTo 0 (len xs - 1)) ++ r }
  @-}
  interleave :: a -> [a] -> [a] -> [[a]] -> [[a]]
  interleave t ts xs r =
      let (_,zs) = interleave' t ts id xs r in zs
  
  -- | @interleave' t ts f ys r@ is equivalent to the expression
  --
  -- > (ys ++ ts, [ f (insertAt n t ys ++ ts) | n <- [0..len ys - 1] ] ++ r)
  --
  
  {-@
  reflect interleave'
  interleave'
    :: t:a
    -> ts:[a]
    -> f:([a] -> b)
    -> ys:[a]
    -> r:[b]
    -> ( { v:[a] | v == ys ++ ts }
       , { v:[b] | v == map (aux0 t f ys ts) (fromTo 0 (len ys-1)) ++ r }
       )
  @-}
  interleave' :: a -> [a] -> ([a] -> b) -> [a] -> [b] -> ([a], [b])
  interleave' t ts _ []     r = (ts, r)
  interleave' t ts f (y:ys) r =
    let (us, zs) = interleave' t ts (snoc f y) ys r
     in (y:us, f (t:y:us) : zs `const` (lemmaMapAux0 t f y ys ts 0 (length ys - 1)))
  
  
  ---------------------------------
  -- Laziness requirement
  ---------------------------------
  
  -- | The documentation of 'Data.List.permutations' states the laziness
  -- requirement as follows
  --
  -- > map (take n) (take (factorial n) $ permutations ([1..n] ++ undefined))
  -- >   =
  -- > permutations [1..n]
  --
  -- This property cannot be proved with Liquid Haskell as partially
  -- defined lists are not representable in formulas. Therefore, we
  -- would have to content ourselves with the weaker
  --
  -- > map (take n) (take (factorial n) $ permutations ([1..n] ++ r))
  -- >   =
  -- > permutations [1..n]
  --
  -- where @r@ stands for any list.
  --
  -- Now, when working out the proof, I didn't feel in the mood of
  -- computing the lengths of the lists returned by all of the functions
  -- implementing permutations, and therefore I aimed to rephrase the
  -- property without calls to 'take'. I arrived first to
  --
  -- > take (factorial n) (permutations ([1..n] ++ r))
  -- >   =
  -- > map (++ r) (permutations [1..n])
  --
  -- and then to
  --
  -- > permutations ([1..n] ++ r)
  -- >   =
  -- > map (++ r) (permutations [1..n]) ++ residue n r
  --
  -- where 'residue' is some expression that we really don't care about
  -- when considering the laziness requirement. Below are two
  -- formulations of it.
  --
  -- > residue n sfx = concat (map (aux2 ([1..n] ++ sfx) []) (fromTo n (n + len sfx - 1)))
  -- > residue n sfx =
  -- >   concat
  -- >     [ concat [ interleave (sfx!!m) (drop (m+1) sfx) xs []
  -- >              | xs <- permutations (reverse ([1..n] ++ take m sfx))
  -- >              ]
  -- >     | m <- [0 .. length sfx - 1]
  -- >     ]
  --
  
  {-@
  lemmaPermutationsDecomposition
    :: { n:Int | n >= 0 }
    -> r:[Int]
    -> { permutations (fromTo 1 n ++ r)
         ==
         map (flipAppend r) (permutations (fromTo 1 n)) ++ concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo n (n + len r - 1)))
       }
  @-}
  lemmaPermutationsDecomposition :: Int -> [Int] -> ()
  lemmaPermutationsDecomposition n r = lemmaPermsDecomposition n r
  
  
  {-@
  lemmaPermsDecomposition
    :: { n:Int | n >= 0 }
    -> r:[Int]
    -> { perms (fromTo 1 n ++ r) []
         ==
         map (flipAppend r) (perms (fromTo 1 n) []) ++ concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo n (n + len r - 1)))
       }
  @-}
  lemmaPermsDecomposition :: Int -> [Int] -> ()
  lemmaPermsDecomposition n r =
      ()
        `const` perms (fromTo 1 n ++ r) []
        `const` lemmaLengthAppend (fromTo 1 n) r
        `const` lemmaLengthFromTo 1 n
        `const` lemmaFromToSplit 0 (n - 1) (n + length r - 1)
        `const` lemmaMapAppend (aux2 (fromTo 1 n ++ r) []) (fromTo 0 (n - 1)) (fromTo n (n + length r - 1))
        `const` lemmaConcatAppend
                  (map (aux2 (fromTo 1 n ++ r) []) (fromTo 0 (n - 1)))
                  (map (aux2 (fromTo 1 n ++ r) []) (fromTo n (n + length r - 1)))
        `const` lemmaConcatMapInterleave (fromTo 1 n) r 0 (n - 1)
        `const` perms (fromTo 1 n) []
  {-
      perms (fromTo 1 n ++ r) []
      `asTypeOf`
      concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo 0 (length (fromTo 1 n ++ r) - 1)))
      `asTypeOf` case lemmaLengthAppend (fromTo 1 n) r of { () ->
      concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo 0 (length (fromTo 1 n) + length r - 1)))
      `asTypeOf` case lemmaLengthFromTo 1 n of { () ->
      concat (map (aux2 ((fromTo 1 n ++ r)) []) (fromTo 0 (n + length r - 1)))
      `asTypeOf`
      const (concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo 0 (n - 1) ++ fromTo n (n + length r - 1))))
            (lemmaFromToSplit 0 (n - 1) (n + length r - 1))
      `asTypeOf`
      const (
      const (concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo 0 (n - 1)))
               ++ concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo n (n + length r - 1)))
            )
            (lemmaMapAppend (aux2 (fromTo 1 n ++ r) []) (fromTo 0 (n - 1)) (fromTo n (n + length r - 1)))
            )
            (lemmaConcatAppend
              (map (aux2 (fromTo 1 n ++ r) []) (fromTo 0 (n - 1)))
              (map (aux2 (fromTo 1 n ++ r) []) (fromTo n (n + length r - 1)))
            )
      `asTypeOf`
      const (map (flipAppend r) (concat (map (aux2 (fromTo 1 n) []) (fromTo 0 (n - 1))))
               ++ concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo n (n + length r - 1))))
            (lemmaConcatMapInterleave (fromTo 1 n) r 0 (n - 1))
      `asTypeOf`
      (map (flipAppend r) (concat (map (aux2 (fromTo 1 n) []) (fromTo 0 (length (fromTo 1 n) - 1))))
         ++ concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo n (n + length r - 1))))
      `asTypeOf`
      (map (flipAppend r) (perms (fromTo 1 n) [])
         ++ concat (map (aux2 (fromTo 1 n ++ r) []) (fromTo n (n + length r - 1))))
      }}
      ***
      QED
  -}
  
  
  ------------------------------
  -- Auxiliary functions
  ------------------------------
  
  infixr 5 ++
  
  {-@ reflect id @-}
  id :: a -> a
  id x = x
  
  {-@ inline const @-}
  const :: a -> b -> a
  const x _ = x
  
  {-@
  inline asTypeOf
  asTypeOf :: x:a -> { y:a | x = y } -> { v:a | v = x }
  @-}
  asTypeOf :: a -> a -> a
  asTypeOf x _ = x
  
  {-@ reflect concat @-}
  concat :: [[a]] -> [a]
  concat [] = []
  concat (x:xs) = x ++ concat xs
  
  {-@
  reflect !!
  (!!) :: xs:[a] -> { n:Int | n < len xs && n >= 0 } -> a
  @-}
  (!!) :: [a] -> Int -> a
  (x:xs) !! 0 = x
  (x:xs) !! n = xs !! (n - 1)
  
  {-@ reflect take @-}
  take :: Int -> [a] -> [a]
  take n xs
    | n > 0 =
      case xs of
        [] -> []
        x:xs -> x : take (n-1) xs
    | otherwise =
      []
  
  {-@ reflect drop @-}
  drop :: Int -> [a] -> [a]
  drop n xs
    | n > 0 =
      case xs of
        [] -> []
        _:xs -> drop (n-1) xs
    | otherwise =
      xs
  
  {-@ reflect ++ @-}
  (++) :: [a] -> [a] -> [a]
  [] ++ ys = ys
  (x:xs) ++ ys = x : xs ++ ys
  
  {-@ reflect flipAppend @-}
  flipAppend :: [a] -> [a] -> [a]
  flipAppend xs ys = ys ++ xs
  
  {-@ reflect insertAt @-}
  insertAt :: Int -> a -> [a] -> [a]
  insertAt n y xs = take n xs ++ y : drop n xs
  
  {-@ reflect map @-}
  map :: (a -> b) -> [a] -> [b]
  map f [] = []
  map f (x:xs) = f x : map f xs
  
  {-@ reflect foldr @-}
  foldr :: (a -> b -> b) -> b -> [a] -> b
  foldr f z [] = z
  foldr f z (x:xs) = f x (foldr f z xs)
  
  {-@ reflect fromTo @-}
  {-@
  fromTo
    :: a:Int
    -> b:Int
    -> [{c:Int | a <= c && c <= b}]
       / [b-a+1]
  @-}
  fromTo :: Int -> Int -> [Int]
  fromTo a b = if a <= b then a : fromTo (a + 1) b
                 else []
  
  {-@ reflect reverse @-}
  reverse :: [a] -> [a]
  reverse [] = []
  reverse (x:xs) = reverse xs ++ [x]
  
  {-@
  lemmaElemAtAppend
    :: xs:[a]
    -> ys:[a]
    -> { i:Int | 0 <= i && i < len xs }
    -> { (xs ++ ys) !! i == xs !! i }
  @-}
  lemmaElemAtAppend :: [a] -> [a] -> Int -> ()
  lemmaElemAtAppend [] _ _ = ()
  lemmaElemAtAppend (_:xs) ys i =
    if i > 0 then lemmaElemAtAppend xs ys (i - 1) else ()
  
  {-@
  lemmaDropAppend
    :: xs:[a]
    -> ys:[a]
    -> { i:Int | 0 <= i && i <= len xs }
    -> { drop i (xs ++ ys) == drop i xs ++ ys }
  @-}
  lemmaDropAppend :: [a] -> [a] -> Int -> ()
  lemmaDropAppend [] _ _ = ()
  lemmaDropAppend (_:xs) ys i =
    if i > 0 then lemmaDropAppend xs ys (i - 1) else ()
  
  {-@
  lemmaTakeAppend
    :: xs:[a]
    -> ys:[a]
    -> { i:Int | 0 <= i && i <= len xs }
    -> { take i (xs ++ ys) == take i xs }
  @-}
  lemmaTakeAppend :: [a] -> [a] -> Int -> ()
  lemmaTakeAppend [] _ _ = ()
  lemmaTakeAppend (_:xs) ys i =
    if i > 0 then lemmaTakeAppend xs ys (i - 1) else ()
  
  {-@
  lemmaMapAppend
    :: f:(a -> b)
    -> xs:[a]
    -> ys:[a]
    -> { map f xs ++ map f ys == map f (xs ++ ys) }
  @-}
  lemmaMapAppend :: (a -> b) -> [a] -> [a] -> ()
  lemmaMapAppend f [] ys = ()
  lemmaMapAppend f (_:xs) ys = lemmaMapAppend f xs ys
  
  {-@
  lemmaConcatAppend
    :: xs:[[a]]
    -> ys:[[a]]
    -> { concat (xs ++ ys) = concat xs ++ concat ys }
  @-}
  lemmaConcatAppend :: [[a]] -> [[a]] -> ()
  lemmaConcatAppend [] _ = ()
  lemmaConcatAppend (x:xs) ys =
    lemmaConcatAppend xs ys
     `const` lemmaAppendAssoc x (concat xs) (concat ys)
  
  {-@
  lemmaLengthFromTo
    :: i:Int
    -> { j:Int | i <= j + 1 }
    -> { len (fromTo i j) == j - i + 1 } / [j - i + 1]
  @-}
  lemmaLengthFromTo :: Int -> Int -> ()
  lemmaLengthFromTo i j = if i <= j then lemmaLengthFromTo (i + 1) j else ()
  
  {-@
  lemmaLengthAppend
    :: xs:[a]
    -> ys:[a]
    -> { len (xs ++ ys) == len xs + len ys }
  @-}
  lemmaLengthAppend :: [a] -> [a] -> ()
  lemmaLengthAppend [] _ = ()
  lemmaLengthAppend (_:xs) ys = lemmaLengthAppend xs ys
  
  {-@
  lemmaFromToSplit
    :: a:Int
    -> { b:Int | a <= b + 1 }
    -> { c:Int | b <= c }
    -> { fromTo a b ++ fromTo (b + 1) c == fromTo a c } / [ b - a + 1 ]
  @-}
  lemmaFromToSplit :: Int -> Int -> Int -> ()
  lemmaFromToSplit a b c =
    if a + 1 <= b then lemmaFromToSplit (a+1) b c else if a <= b then () else ()
  
  {-
    if a + 1 <= b then
      (fromTo a b ++ fromTo (b + 1) c)
      `asTypeOf`
      (a:fromTo (a+1) b ++ fromTo (b + 1) c)
      `asTypeOf`
      const (a:fromTo (a+1) c)
            (lemmaFromToSplit (a+1) b c)
      `asTypeOf`
      fromTo a c
      ***
      QED
    else
      ()
  -}
  
  {-@ lemmaAppendId :: xs:[a] -> { xs = xs ++ [] } @-}
  lemmaAppendId :: [a] -> ()
  lemmaAppendId [] = ()
  lemmaAppendId (_:xs) = lemmaAppendId xs
  
  -- | The refinement predicate in the return type is equivalent to
  --
  -- > [ f (y : insertAt n t ys ts) | n <- [i..j] ]
  -- >   =
  -- > [ f (insertAt n t (y:ys) ts) | n <- [i+1 .. j+1] ]
  --
  
  {-@
  lemmaMapAux0
    :: t:a
    -> f:([a] -> b)
    -> y:a
    -> ys:[a]
    -> ts:[a]
    -> { i:Int | 0 <= i }
    -> j:Int
    -> { map (aux0 t (snoc f y) ys ts) (fromTo i j)
           == map (aux0 t f (y:ys) ts) (fromTo (i+1) (j+1))
       } / [j-i+1]
  @-}
  lemmaMapAux0 :: a -> ([a] -> b) -> a -> [a] -> [a] -> Int -> Int -> ()
  lemmaMapAux0 t f y ys ts i j =
      if i <= j then lemmaMapAux0 t f y ys ts (i+1) j else ()
  
  {-@ reflect snoc @-}
  snoc :: ([a] -> b) -> a -> [a] -> b
  snoc f y xs = f (y : xs)
  
  {-@
  lemmaInterleaveAppend
    :: t:a
    -> ts:[a]
    -> p:[a]
    -> r:[[a]]
    -> { interleave t ts p r == interleave t ts p [] ++ r }
  @-}
  lemmaInterleaveAppend :: a -> [a] -> [a] -> [[a]] -> ()
  lemmaInterleaveAppend t ts p r =
    ()
      ? interleave t ts p r
      ? interleave t ts p []
      ? lemmaAppendAssoc (map (aux0 t id p ts) (fromTo 0 (length p - 1))) [] r
  
  
  ---------------------------------
  
  -- Doesn't work:
  -- rewriteWith lemmaInterleaveAppend [lemmaAppendAssoc]
  
  {-@
  lemmaFoldrInterleave
    :: t:a
    -> ts:[a]
    -> ps:[[a]]
    -> r:[[a]]
    -> { foldr (interleave t ts) r ps == concat (map (aux1 t ts []) ps) ++ r }
  @-}
  lemmaFoldrInterleave :: a -> [a] -> [[a]] -> [[a]] -> ()
  lemmaFoldrInterleave t ts [] r = ()
  lemmaFoldrInterleave t ts (p:ps) r =
    lemmaFoldrInterleave t ts ps r
      ? lemmaInterleaveAppend t ts p (concat (map (aux1 t ts []) ps) ++ r)
      ? lemmaAppendAssoc (interleave t ts p []) (concat (map (aux1 t ts []) ps)) r
  
  {-@
  lemmaAppendAssoc :: xs:[a] -> ys:[a] -> zs:[a] -> { xs ++ ys ++ zs = (xs ++ ys) ++ zs }
  @-}
  lemmaAppendAssoc :: [a] -> [a] -> [a] -> ()
  lemmaAppendAssoc [] _ _ = ()
  lemmaAppendAssoc (_:xs) ys zs = lemmaAppendAssoc xs ys zs
  
  {-@
  lemmaConcatMapInterleave
    :: ts:[a]
    -> r:[a]
    -> { i:Int | i >= 0 }
    -> { j:Int | j < len ts }
    -> { concat (map (aux2 (ts ++ r) []) (fromTo i j))
           == map (flipAppend r) (concat (map (aux2 ts []) (fromTo i j))) } / [j - i + 1]
  @-}
  lemmaConcatMapInterleave :: [a] -> [a] -> Int -> Int -> ()
  lemmaConcatMapInterleave ts r i j =
      if i <= j then
        lemmaConcatMapInterleave ts r (i + 1) j
          `const` lemmaLengthAppend ts r
          `const` lemmaTakeAppend ts r i
          `const` lemmaElemAtAppend ts r i
          `const` lemmaDropAppend ts r (i + 1)
          `const` lemmaAppendInterleave (ts !! i) (drop (i + 1) ts) r (permutations (reverse (take i ts) ++ []))
          `const` lemmaMapAppend (flipAppend r) (aux2 ts [] i) (concat (map (aux2 ts []) (fromTo (i + 1) j)))
      else
        ()
  {-
      if i <= j then
        case lemmaLengthAppend ts r of { () ->
        concat (map (aux2 (ts ++ r) []) (fromTo i j))
        `asTypeOf`
        concat (map (aux2 (ts ++ r) []) (i : fromTo (i + 1) j))
        `asTypeOf`
        (aux2 (ts ++ r) [] i ++ concat (map (aux2 (ts ++ r) []) (fromTo (i + 1) j)))
        `asTypeOf`
        const (aux2 (ts ++ r) [] i ++ map (flipAppend r) (concat (map (aux2 ts []) (fromTo (i + 1) j))))
              (lemmaConcatMapInterleave ts r (i + 1) j)
        `asTypeOf`
        (mapInterleave ((ts ++ r) !! i) (drop (i + 1) (ts ++ r)) (permutations (reverse (take i (ts ++ r)) ++ [])) []
           ++ map (flipAppend r) (concat (map (aux2 ts []) (fromTo (i + 1) j))))
        `asTypeOf`
        const (mapInterleave ((ts ++ r) !! i) (drop (i + 1) (ts ++ r)) (permutations (reverse (take i ts) ++ [])) []
               ++ map (flipAppend r) (concat (map (aux2 ts []) (fromTo (i + 1) j))))
              (lemmaTakeAppend ts r i)
        `asTypeOf`
        const (mapInterleave (ts !! i) (drop (i + 1) (ts ++ r)) (permutations (reverse (take i ts) ++ [])) []
               ++ map (flipAppend r) (concat (map (aux2 ts []) (fromTo (i + 1) j))))
              (lemmaElemAtAppend ts r i)
        `asTypeOf`
        const (mapInterleave (ts !! i) (drop (i + 1) ts ++ r) (permutations (reverse (take i ts) ++ [])) []
               ++ map (flipAppend r) (concat (map (aux2 ts []) (fromTo (i + 1) j))))
              (lemmaDropAppend ts r (i + 1))
        `asTypeOf`
        const (map (flipAppend r) (aux2 ts [] i) ++ map (flipAppend r) (concat (map (aux2 ts []) (fromTo (i + 1) j))))
              (lemmaAppendInterleave (ts !! i) (drop (i + 1) ts) r (permutations (reverse (take i ts) ++ [])))
        `asTypeOf`
        const (map (flipAppend r) (aux2 ts [] i ++ concat (map (aux2 ts []) (fromTo (i + 1) j))))
              (lemmaMapAppend (flipAppend r) (aux2 ts [] i) (concat (map (aux2 ts []) (fromTo (i + 1) j))))
        `asTypeOf`
        map (flipAppend r) (concat (map (aux2 ts []) (fromTo i j)))
        }
        ***
        QED
      else
        ()
  -}
  
  {-@
  lemmaAppendInterleave
    :: t:a
    -> ts:[a]
    -> r:[a]
    -> ps:[[a]]
    -> { mapInterleave t (ts ++ r) ps [] == map (flipAppend r) (mapInterleave t ts ps []) }
  @-}
  lemmaAppendInterleave :: a -> [a] -> [a] -> [[a]] -> ()
  lemmaAppendInterleave t ts r [] = ()
    ? mapInterleave t (ts ++ r) [] []
    ? mapInterleave t ts [] []
  lemmaAppendInterleave t ts r (p:ps) =
    lemmaAppendInterleave t ts r ps
      `const` mapInterleave t (ts ++ r) (p:ps) []
      `const` mapInterleave t ts (p:ps) []
      `const` mapInterleave t (ts ++ r) ps []
      `const` mapInterleave t ts ps []
      `const` lemmaAppendAssoc (aux1 t (ts ++ r) [] p) (concat (map (aux1 t (ts ++ r) []) ps)) []
      `const` interleave t (ts ++ r) p []
      `const` lemmaAppendAux0 t p ts r (fromTo 0 (length p - 1))
      `const` lemmaAppendId (map (aux0 t id p ts) (fromTo 0 (length p - 1)))
      `const` lemmaAppendId (map (flipAppend r) (interleave t ts p []))
      `const` lemmaMapAppend (flipAppend r) (aux1 t ts [] p) (mapInterleave t ts ps [])
      `const` lemmaAppendAssoc (aux1 t ts [] p) (concat (map (aux1 t ts []) ps)) []
  
  {-
    mapInterleave t (ts ++ r) (p:ps) []
    `asTypeOf`
    const (concat (map (aux1 t (ts ++ r) []) (p:ps)) ++ [])
          (mapInterleave t (ts ++ r) (p:ps) [])
    `asTypeOf`
     ((aux1 t (ts ++ r) [] p ++ concat (map (aux1 t (ts ++ r) []) ps)) ++ [])
    `asTypeOf`
     const (aux1 t (ts ++ r) [] p ++ concat (map (aux1 t (ts ++ r) []) ps) ++ [])
           (lemmaAppendAssoc (aux1 t (ts ++ r) [] p) (concat (map (aux1 t (ts ++ r) []) ps)) [])
    `asTypeOf`
     const (aux1 t (ts ++ r) [] p ++ mapInterleave t (ts ++ r) ps [])
           (mapInterleave t (ts ++ r) ps [])
    `asTypeOf`
     const (aux1 t (ts ++ r) [] p ++ map (flipAppend r) (mapInterleave t ts ps []))
           (lemmaAppendInterleave t ts r ps)
    `asTypeOf`
     const ((map (aux0 t id p (ts ++ r)) (fromTo 0 (length p - 1)) ++ []) ++ map (flipAppend r) (mapInterleave t ts ps []))
           (interleave t (ts ++ r) p [])
    `asTypeOf`
     const ((map (flipAppend r) (map (aux0 t id p ts) (fromTo 0 (length p - 1))) ++ []) ++ map (flipAppend r) (mapInterleave t ts ps []))
           (lemmaAppendAux0 t p ts r (fromTo 0 (length p - 1)))
    `asTypeOf`
     const ((map (flipAppend r) (interleave t ts p []) ++ []) ++ map (flipAppend r) (mapInterleave t ts ps []))
           (lemmaAppendId (map (aux0 t id p ts) (fromTo 0 (length p - 1))))
    `asTypeOf`
     const (map (flipAppend r) (aux1 t ts [] p) ++ map (flipAppend r) (mapInterleave t ts ps []))
           (lemmaAppendId (map (flipAppend r) (interleave t ts p [])))
    `asTypeOf`
     const (map (flipAppend r) (aux1 t ts [] p ++ mapInterleave t ts ps []))
           (lemmaMapAppend (flipAppend r) (aux1 t ts [] p) (mapInterleave t ts ps []))
    `asTypeOf`
     const (map (flipAppend r) (aux1 t ts [] p ++ concat (map (aux1 t ts []) ps) ++ []))
           (mapInterleave t ts ps [])
    `asTypeOf`
     const (map (flipAppend r) ((aux1 t ts [] p ++ concat (map (aux1 t ts []) ps)) ++ []))
           (lemmaAppendAssoc (aux1 t ts [] p) (concat (map (aux1 t ts []) ps)) [])
    `asTypeOf`
     map (flipAppend r) (mapInterleave t ts (p:ps) [])
    ***
    QED
  -}
  
  {-@
  lemmaAppendAux0
    :: t:a
    -> p:[a]
    -> ts:[a]
    -> r:[a]
    -> xs:[Int]
    -> { map (aux0 t id p (ts ++ r)) xs == map (flipAppend r) (map (aux0 t id p ts) xs) }
  @-}
  lemmaAppendAux0  :: a -> [a] -> [a] -> [a] -> [Int] -> ()
  lemmaAppendAux0 t p ts r [] = ()
  lemmaAppendAux0 t p ts r (x:xs) =
    lemmaAppendAux0 t p ts r xs
      ? lemmaAppendAssoc (insertAt x t p) ts r
  
  -- | The refinement predicate in the return type is equivalent to
  --
  -- > [ interleave (ts!!n) (drop (n+1) ts) xs []
  -- > | n <- [i..j]
  -- > , xs <- permutations (reverse (take n ts) ++ t:is)
  -- > ]
  -- >
  -- >   =
  -- >
  -- > [ interleave ((t:ts)!!n) (drop (n+1) (t:ts)) xs []
  -- > | n <- [i+1..j+1]
  -- > , xs <- permutations (reverse (take n (t:ts)) ++ is)
  -- > ]
  --
  
  {-@
  lemmaMapAux2
    :: t:a
    -> ts:[a]
    -> is:[a]
    -> { i:Int | 0 <= i }
    -> { j:Int | j < len ts }
    -> { map (aux2 ts (t:is)) (fromTo i j)
           == map (aux2 (t:ts) is) (fromTo (i+1) (j+1))
       } / [j-i+1]
  @-}
  lemmaMapAux2 :: a -> [a] -> [a] -> Int -> Int -> ()
  lemmaMapAux2 t ts is i j =
    if i<=j then
      lemmaMapAux2 t ts is (i+1) j
        `const` lemmaAppendAssoc (reverse (take i ts)) [t] is
  
  {-
      map (aux2 ts (t:is)) (fromTo i j)
      ===
      aux2 ts (t:is) i : map (aux2 ts (t:is)) (fromTo (i+1) j)
      ===
      const (aux2 ts (t:is) i : map (aux2 (t:ts) is) (fromTo (i+2) (j+1)))
            (lemmaMapAux2 t ts is (i+1) j)
      ===
      (mapInterleave (ts!!i) (drop (i+1) ts) (permutations (reverse (take i ts) ++ (t:is))) []
        : map (aux2 (t:ts) is) (fromTo (i+2) (j+1))
      )
      ===
      (mapInterleave (ts!!i) (drop (i+1) ts) (permutations (reverse (take i ts) ++ [t] ++ is)) []
         : map (aux2 (t:ts) is) (fromTo (i+2) (j+1))
      )
      ===
      const (mapInterleave (ts!!i) (drop (i+1) ts) (permutations ((reverse (take i ts) ++ [t]) ++ is)) []
               : map (aux2 (t:ts) is) (fromTo (i+2) (j+1))
            )
            (lemmaAppendAssoc (reverse (take i ts)) [t] is)
      ===
      (mapInterleave ((t:ts)!!(i+1)) (drop (i+2) (t:ts)) (permutations (reverse (take (i+1) (t:ts)) ++ is)) []
         : map (aux2 (t:ts) is) (fromTo (i+2) (j+1))
      )
      ===
      (aux2 (t:ts) is (i+1) : map (aux2 (t:ts) is) (fromTo (i+2) (j+1))
      ***
      QED
      -}
    else
      ()
  