Decouple Invariants From Data {#recursive} ========================================== Recursive Structures --------------------
Lets see another example of decoupling...
Decouple Invariants From Recursive Data ======================================= Recall: Lists ------------- 
35: data L a = N 
36:          | C a (L a)
Recall: Refined Constructors ---------------------------- Define *increasing* Lists with strengthened constructors: 
46: data L a where
47:   N :: L a
48:   C :: hd:a -> tl: L {v:a | hd <= v} -> L a
Problem: Decreasing Lists? -------------------------- What if we need *both* [increasing and decreasing lists](http://web.cecs.pdx.edu/~sheard/Code/QSort.html)?
*Separate* types are tedious...
Abstract That Refinement! ------------------------- 
67: {-@ data L a <p :: a -> a -> Prop>
68:       = N 
69:       | C (hd :: a) (tl :: (L <p> a<p hd>)) @-}

-
`p` is a *binary* relation between two `a` values
-
Definition relates `hd` with *all* the elements of `tl`
-
Recursive: `p` holds for *every pair* of elements!
Example ------- Consider a list with *three* or more elements 
86: x1 `C` x2 `C` x3 `C` rest :: L <p> a
Example: Unfold Once -------------------- 
93: x1                 :: a
94: x2 `C` x3 `C` rest :: L <p> a<p x1>
Example: Unfold Twice --------------------- 
101: x1          :: a
102: x2          :: a<p x1>  
103: x3 `C` rest :: L <p> a<p x1 && p x2>
Example: Unfold Thrice ---------------------- 
110: x1   :: a
111: x2   :: a<p x1>  
112: x3   :: a<p x1 && p x2>  
113: rest :: L <p> a<p x1 && p x2 && p x3>

Note how `p` holds between **every pair** of elements in the list.
A Concrete Example ------------------ That was a rather *abstract*!
How can we *use* fact that `p` holds between *every pair* ? Example: Increasing Lists ------------------------- *Instantiate* `p` with a *concrete* refinement 
140: {-@ type IncL a = L <{\hd v -> hd <= v}> a @-}

-
Refinement says `hd` less than each tail element `v`,
-
Thus, `IncL` denotes *increaing* lists.
Example: Increasing Lists ------------------------- LiquidHaskell verifies that `slist` is indeed increasing... 
155: {-@ slist :: IncL Int @-}
156: (L <\hd2 VV -> (hd2 <= VV)> (Int))slist     = {x2 : (Int) | (x2 == (1  :  int))}1 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})`C` {x2 : (Int) | (x2 == (6  :  int))}6 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})`C` {x2 : (Int) | (x2 == (12  :  int))}12 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})`C` (L <\_ VV -> false> {x3 : (Int) | false})N

... and protests that `slist'` is not: 
166: {-@ slist' :: IncL Int @-}
167: (L <\hd2 VV -> (hd2 <= VV)> (Int))slist' = {x2 : (Int) | (x2 == (6  :  int))}6 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})`C` {x2 : (Int) | (x2 == (1  :  int))}1 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})`C` {x2 : (Int) | (x2 == (12  :  int))}12 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})`C` (L <\_ VV -> false> {x3 : (Int) | false})N
Insertion Sort -------------- 
175: {-@ insertSort :: (Ord a) => [a] -> IncL a @-}
176: forall a. (Ord a) => [a] -> (L <\hd2 VV -> (hd2 <= VV)> a)insertSort     = (a
 -> (L <\x11 VV -> (VV >= x11)> a)
 -> (L <\x11 VV -> (VV >= x11)> a))
-> (L <\x11 VV -> (VV >= x11)> a)
-> [a]
-> (L <\x11 VV -> (VV >= x11)> a)foldr a -> (L <\x4 VV -> (VV >= x4)> a) -> (L <\x2 VV -> (VV >= x2)> a)insert (L <\_ VV -> false> {VV : a | false})N
177: 
178: forall a.
(Ord a) =>
a -> (L <\x2 VV -> (VV >= x2)> a) -> (L <\x1 VV -> (VV >= x1)> a)insert ay N          = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV == y)}
-> (L <p> {VV : a<p x1> | (VV == y)})
-> (L <p> {VV : a | (VV == y)})`C` (L <\_ VV -> false> {VV : a | false})N
179: insert y (x `C` xs) 
180:   | {VV : a | (VV == y)}y x1:a -> x2:a -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}< {VV : a | (VV == x)}x           = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= y)}
-> (L <p> {VV : a<p x1> | (VV >= y)})
-> (L <p> {VV : a | (VV >= y)})`C` ({VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > y) && (VV >= x)}
-> (L <p> {VV : a<p x1> | (VV > y) && (VV >= x)})
-> (L <p> {VV : a | (VV > y) && (VV >= x)})`C` {x2 : (L <\x3 VV -> (VV >= x3)> {VV : a | (VV >= x)}) | (x2 == xs)}xs)
181:   | otherwise       = {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= x)}
-> (L <p> {VV : a<p x1> | (VV >= x)})
-> (L <p> {VV : a | (VV >= x)})`C` forall a.
(Ord a) =>
a -> (L <\x2 VV -> (VV >= x2)> a) -> (L <\x1 VV -> (VV >= x1)> a)insert {VV : a | (VV == y)}y {x2 : (L <\x3 VV -> (VV >= x3)> {VV : a | (VV >= x)}) | (x2 == xs)}xs

(*Hover* over `insert'` to see inferred type.) Checking GHC Lists ------------------ Demo: Above applies to GHC's List definition: 
195: data [a] <p :: a -> a -> Prop>
196:   = [] 
197:   | (:) (h :: a) (tl :: ([a<p h>]<p>))
Checking GHC Lists ------------------ Increasing Lists 
208: {-@ type Incs a = [a]<{\h v -> h <= v}> @-}
209: 
210: {-@ iGoUp :: Incs Int @-}
211: [(Int)]<\h6 VV -> (h6 <= VV)>iGoUp     = {x4 : [{x14 : (Int) | (x14 > 0)}]<\x11 VV -> (x11 /= x12) && (x12 > 0) && (x12 > x11) && (x11 <= x12)> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}[{x2 : (Int) | (x2 == (1  :  int))}1,{x2 : (Int) | (x2 == (2  :  int))}2,{x2 : (Int) | (x2 == (3  :  int))}3]
Checking GHC Lists ------------------ Decreasing Lists 
222: {-@ type Decs a = [a]<{\h v -> h >= v}> @-}
223: 
224: {-@ iGoDn :: Decs Int @-}
225: [(Int)]<\h8 VV -> (h8 >= VV)>iGoDn     = {x4 : [{x15 : (Int) | (x15 > 0)}]<\x13 VV -> (x12 == 1) && (x13 /= x12) && (x12 > 0) && (x13 >= x12) && (x12 < x13)> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}[{x2 : (Int) | (x2 == (3  :  int))}3,{x2 : (Int) | (x2 == (2  :  int))}2,{x2 : (Int) | (x2 == (1  :  int))}1]
Checking GHC Lists ------------------ Duplicate-free Lists 
237: {-@ type Difs a = [a]<{\h v -> h /= v}> @-}
238: 
239: {-@ iDiff :: Difs Int @-}
240: [(Int)]<\h10 VV -> (h10 /= VV)>iDiff     = {x4 : [{x14 : (Int) | (x14 > 0)}]<\x12 VV -> (x12 /= x11) && (x11 > 0) && (x12 >= x11) && (x11 < x12)> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}[{x2 : (Int) | (x2 == (1  :  int))}1,{x2 : (Int) | (x2 == (3  :  int))}3,{x2 : (Int) | (x2 == (2  :  int))}2]
Checking GHC Lists ------------------ Now we can check all the usual list sorting algorithms Example: `mergeSort` [1/2] -------------------------- 
252: {-@ mergeSort  :: (Ord a) => [a] -> Incs a @-}
253: forall a. (Ord a) => [a] -> [a]<\h6 VV -> (h6 <= VV)>mergeSort []   = forall <p :: a-> a-> Bool>.
{x4 : [{VV : a | false}]<p> | (((null x4)) <=> true) && ((len x4) == 0) && ((sumLens x4) == 0)}[]
254: mergeSort [x]  = {x6 : [{VV : a | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}[{VV : a | (VV == x)}x]
255: mergeSort xs   = x1:{x10 : [a]<\x11 VV -> (VV >= x11)> | ((len x10) >= 0)}
-> x2:{x7 : [a]<\x8 VV -> (VV >= x8)> | ((len x7) >= 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | ((len x4) >= 0) && ((len x4) >= (len x1)) && ((len x4) >= (len x2))}merge {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 == xs1') && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs1' {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 == xs2') && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs2' 
256:   where 
257:    ({VV : [a] | (VV == xs1) && ((len VV) == (len xs1)) && ((len VV) >= 0) && ((len VV) >= (len xs2))}xs1, {VV : [a] | (VV == xs2) && ((len VV) == (len xs2)) && ((len VV) >= 0) && ((len VV) <= (len xs1)) && ((len VV) <= (len xs1))}xs2)  = x1:{x14 : [a] | ((len x14) > 0)}
-> ({x9 : [a] | ((len x9) >= 0) && ((len x9) <= (len x1))}, {x12 : [a] | ((len x12) >= 0) && ((len x12) <= (len x1))})<\x5 VV -> ((len x6) >= 0) && ((len x6) <= (len x5)) && ((len x6) <= (len x1))>split {x3 : [a] | ((len x3) >= 0) && ((sumLens x3) >= 0)}xs
258:    [a]<\x2 VV -> (x2 <= VV)>xs1'        = [a] -> [a]<\x2 VV -> (x2 <= VV)>mergeSort {x7 : [a] | (x7 == xs1) && (x7 == xs1) && ((len x7) == (len xs1)) && ((len x7) >= 0) && ((len x7) >= (len xs2)) && ((sumLens x7) >= 0)}xs1
259:    [a]<\x2 VV -> (x2 <= VV)>xs2'        = [a] -> [a]<\x2 VV -> (x2 <= VV)>mergeSort {x8 : [a] | (x8 == xs2) && (x8 == xs2) && ((len x8) == (len xs2)) && ((len x8) >= 0) && ((sumLens x8) >= 0) && ((len x8) <= (len xs1)) && ((len x8) <= (len xs1))}xs2
Example: `mergeSort` [1/2] -------------------------- 
266: forall a.
x1:{VV : [a] | ((len VV) >= 0)}
-> ({VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))}, {VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))})<\x1 VV -> ((len VV) >= 0) && ((len VV) <= (len x1)) && ((len VV) <= (len x1))>split (x:y:zs) = forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {x3 : (a, b)<p2> | ((fst x3) == x1) && ((snd x3) == x2)}({VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {x4 : [a]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}:{x8 : [a] | (x8 == xs) && (x8 == xs) && ((len x8) == (len xs)) && ((len x8) >= 0) && ((len x8) >= (len ys)) && ((sumLens x8) >= 0) && ((len x8) <= (len zs))}xs, {VV : a | (VV == y)}yforall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {x4 : [a]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}:{x9 : [a] | (x9 == ys) && (x9 == ys) && ((len x9) == (len ys)) && ((len x9) >= 0) && ((sumLens x9) >= 0) && ((len x9) <= (len xs)) && ((len x9) <= (len xs)) && ((len x9) <= (len zs))}ys) 
267:   where 
268:     ({VV : [a] | (VV == xs) && ((len VV) == (len xs)) && ((len VV) >= 0) && ((len VV) >= (len ys)) && ((len VV) <= (len zs))}xs, {VV : [a] | (VV == ys) && ((len VV) == (len ys)) && ((len VV) >= 0) && ((len VV) <= (len xs)) && ((len VV) <= (len xs)) && ((len VV) <= (len zs))}ys)   = forall a.
x1:{VV : [a] | ((len VV) >= 0)}
-> ({VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))}, {VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))})<\x1 VV -> ((len VV) >= 0) && ((len VV) <= (len x1)) && ((len VV) <= (len x1))>split {x4 : [a] | (x4 == zs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}zs
269: split xs       = forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {x3 : (a, b)<p2> | ((fst x3) == x1) && ((snd x3) == x2)}({x3 : [a] | ((len x3) >= 0) && ((sumLens x3) >= 0)}xs, {x6 : [{VV : a | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}[])
270: 
271: forall a.
(Ord a) =>
xs:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}xs []    = {x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs
272: merge [] ys    = {x3 : [a]<\x4 VV -> (VV >= x4)> | ((len x3) >= 0) && ((sumLens x3) >= 0)}ys
273: merge (x:xs) (y:ys) 
274:   | {VV : a | (VV == x)}x x1:a -> x2:a -> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}<= {VV : a | (VV == y)}y     = {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (x <= VV)}
-> x2:[{VV : a<p x1> | (x <= VV)}]<p>
-> {x4 : [{VV : a | (x <= VV)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}: forall a.
(Ord a) =>
xs:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge {x4 : [{VV : a | (VV >= x)}]<\x5 VV -> (VV >= x5)> | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs ({VV : a | (VV == y)}yforall <p :: a-> a-> Bool>.
x1:{VV : a | (x <= VV) && (y <= VV)}
-> x2:[{VV : a<p x1> | (x <= VV) && (y <= VV)}]<p>
-> {x4 : [{VV : a | (x <= VV) && (y <= VV)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}:{x4 : [{VV : a | (VV >= y)}]<\x5 VV -> (VV >= x5)> | (x4 == ys) && ((len x4) >= 0) && ((sumLens x4) >= 0)}ys)
275:   | otherwise  = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= y)}
-> x2:[{VV : a<p x1> | (VV >= y)}]<p>
-> {x4 : [{VV : a | (VV >= y)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}: forall a.
(Ord a) =>
xs:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge ({VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > y)}
-> x2:[{VV : a<p x1> | (VV > y)}]<p>
-> {x4 : [{VV : a | (VV > y)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}:{x4 : [{VV : a | (VV >= x)}]<\x5 VV -> (VV >= x5)> | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs) {x4 : [{VV : a | (VV >= y)}]<\x5 VV -> (VV >= x5)> | (x4 == ys) && ((len x4) >= 0) && ((sumLens x4) >= 0)}ys
Example: `Data.List.sort` ------------------------- GHC's "official" list sorting routine Juggling lists of increasing & decreasing lists Ex: `Data.List.sort` [1/4] -------------------------- Juggling lists of increasing & decreasing lists 
294: {-@ sort :: (Ord a) => [a] -> Incs a  @-}
295: forall a. (Ord a) => [a] -> [a]<\h6 VV -> (h6 <= VV)>sort = {x5 : [{x9 : [a]<\x10 VV -> (x10 <= VV)> | ((len x9) >= 0)}]<\_ VV -> ((len x7) >= 0)> | ((len x5) > 0)}
-> {x2 : [a]<\x3 VV -> (x3 <= VV)> | ((len x2) >= 0)}mergeAll forall <q :: [a]-> [[a]]-> Bool, p :: [[a]]-> [a]-> Bool>.
(x:{x26 : [{x30 : [a]<\x31 VV -> (x31 <= VV)> | ((len x30) >= 0)}]<\_ VV -> ((len x28) >= 0)> | ((len x26) > 0)}
 -> {x23 : [a]<\x24 VV -> (x24 <= VV)><p x> | ((len x23) >= 0)})
-> (y:[a]
    -> {x26 : [{x30 : [a]<\x31 VV -> (x31 <= VV)> | ((len x30) >= 0)}]<\_ VV -> ((len x28) >= 0)><q y> | ((len x26) > 0)})
-> x3:[a]
-> exists [z:{x26 : [{x30 : [a]<\x31 VV -> (x31 <= VV)> | ((len x30) >= 0)}]<\_ VV -> ((len x28) >= 0)><q x3> | ((len x26) > 0)}].{x23 : [a]<\x24 VV -> (x24 <= VV)><p z> | ((len x23) >= 0)}. [a]
-> {x2 : [{x6 : [a]<\x7 VV -> (x7 <= VV)> | ((len x6) >= 0)}]<\_ VV -> ((len x4) >= 0)> | ((len x2) > 0)}sequences
296: 
297: forall a.
(Ord a) =>
[a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences (a:b:xs)
298:   | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {x4 : (Ordering) | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:(Ordering)
-> x2:(Ordering) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 == x2))}== {x3 : (Ordering) | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}GT = forall a.
(Ord a) =>
a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending {VV : a | (VV == b)}b {x4 : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}[{VV : a | (VV == a)}a]  {x4 : [a] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs
299:   | otherwise           = forall a.
(Ord a) =>
a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (a <= VV) && (x3 <= VV)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending  {VV : a | (VV == b)}b ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (a <= VV)}
-> x2:[{VV : a<p x1> | (a <= VV)}]<p>
-> {x4 : [{VV : a | (a <= VV)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}:) {x4 : [a] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs
300: sequences [x]           = {x6 : [{x8 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}[{x4 : [{VV : a | (VV == a)}]<\_ VV -> false> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}[{VV : a | (VV == a)}x]]
301: sequences []            = {x6 : [{x8 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}[{x6 : [{VV : a | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}[]]
Ex: `Data.List.sort` [2/4] -------------------------- Juggling lists of increasing & decreasing lists 
312: forall a.
(Ord a) =>
a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending aa {VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | ((len VV) > 0)}as (b:bs)
313:   | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {x4 : (Ordering) | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:(Ordering)
-> x2:(Ordering) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 == x2))}== {x3 : (Ordering) | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}GT 
314:   = forall a.
(Ord a) =>
a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending {VV : a | (VV == b)}b ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > b)}
-> x2:[{VV : a<p x1> | (VV > b)}]<p>
-> {x4 : [{VV : a | (VV > b)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}:{x5 : [{VV : a | (VV > a)}]<\x6 VV -> (VV > a) && (VV > x6)> | (x5 == as) && ((len x5) > 0) && ((len x5) >= 0) && ((sumLens x5) >= 0)}as) {x4 : [a] | (x4 == bs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}bs
315: descending a as bs      
316:   = ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (a <= VV)}
-> x2:[{VV : a<p x1> | (a <= VV)}]<p>
-> {x4 : [{VV : a | (a <= VV)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}:{x5 : [{VV : a | (VV > a)}]<\x6 VV -> (VV > a) && (VV > x6)> | (x5 == as) && ((len x5) > 0) && ((len x5) >= 0) && ((sumLens x5) >= 0)}as)forall <p :: [a]-> [a]-> Bool>.
x1:{x15 : [a]<\x16 VV -> (x16 <= VV)> | ((len x15) >= 0)}
-> x2:[{x15 : [a]<\x16 VV -> (x16 <= VV)><p x1> | ((len x15) >= 0)}]<p>
-> {x4 : [{x15 : [a]<\x16 VV -> (x16 <= VV)> | ((len x15) >= 0)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}: forall a.
(Ord a) =>
[a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences {x3 : [a] | ((len x3) >= 0) && ((sumLens x3) >= 0)}bs
Ex: `Data.List.sort` [3/4] -------------------------- Juggling lists of increasing & decreasing lists 
328: forall a.
(Ord a) =>
a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (a <= VV) && (x3 <= VV)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending aa x1:{VV : [{VV : a | (VV >= a)}]<\x2 VV -> (a <= VV) && (x2 <= VV)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}as (b:bs)
329:   | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {x4 : (Ordering) | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:(Ordering)
-> x2:(Ordering) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 /= x2))}/= {x3 : (Ordering) | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}GT 
330:   = forall a.
(Ord a) =>
a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (a <= VV) && (x3 <= VV)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending {VV : a | (VV == b)}b (x1:{x7 : [{VV : a | (VV >= a) && (VV >= b)}]<\x8 VV -> (a <= VV) && (b <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}\{VV : [{VV : a | (VV >= a) && (VV >= b)}]<\x1 VV -> (a <= VV) && (b <= VV) && (x1 <= VV)> | ((len VV) > 0)}ys -> x1:{x7 : [{VV : a | (VV >= a)}]<\x8 VV -> (a <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}as ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a)}
-> x2:[{VV : a<p x1> | (VV >= a)}]<p>
-> {x4 : [{VV : a | (VV >= a)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}:{x5 : [{VV : a | (VV >= a) && (VV >= b)}]<\x6 VV -> (a <= VV) && (b <= VV) && (x6 <= VV)> | (x5 == ys) && ((len x5) > 0) && ((len x5) >= 0) && ((sumLens x5) >= 0)}ys)) {x4 : [a] | (x4 == bs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}bs
331: ascending a as bs      
332:   = x1:{x7 : [{VV : a | (VV >= a)}]<\x8 VV -> (a <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}as {x4 : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}[{VV : a | (VV == a)}a]forall <p :: [a]-> [a]-> Bool>.
x1:{x15 : [a]<\x16 VV -> (x16 <= VV)> | ((len x15) >= 0)}
-> x2:[{x15 : [a]<\x16 VV -> (x16 <= VV)><p x1> | ((len x15) >= 0)}]<p>
-> {x4 : [{x15 : [a]<\x16 VV -> (x16 <= VV)> | ((len x15) >= 0)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}: forall a.
(Ord a) =>
[a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences {x3 : [a] | ((len x3) >= 0) && ((sumLens x3) >= 0)}bs
Ex: `Data.List.sort` [4/4] -------------------------- Juggling lists of increasing & decreasing lists 
343: forall a.
(Ord a) =>
{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}mergeAll [x]        = {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 == x) && ((len x4) >= 0) && ((sumLens x4) >= 0)}x
344: mergeAll xs         = forall a.
(Ord a) =>
{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}mergeAll (x1:{x10 : [{x14 : [a]<\x15 VV -> (VV >= x15)> | ((len x14) >= 0)}]<\_ VV -> ((len x12) >= 0)> | ((len x10) >= 0)}
-> {x3 : [{x7 : [a]<\x8 VV -> (VV >= x8)> | ((len x7) >= 0)}]<\_ VV -> ((len x5) >= 0)> | ((len x3) >= 0) && ((len x3) <= (len x1))}mergePairs {x3 : [{x7 : [a]<\x8 VV -> (x8 <= VV)> | ((len x7) >= 0)}]<\_ VV -> ((len x5) >= 0)> | ((len x3) >= 0) && ((sumLens x3) >= 0)}xs)
345: 
346: forall a.
(Ord a) =>
x1:{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x1))}mergePairs (a:b:xs) = x1:{x10 : [a]<\x11 VV -> (VV >= x11)> | ((len x10) >= 0)}
-> x2:{x7 : [a]<\x8 VV -> (VV >= x8)> | ((len x7) >= 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | ((len x4) >= 0) && ((len x4) >= (len x1)) && ((len x4) >= (len x2))}merge {x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 == a) && ((len x4) >= 0) && ((sumLens x4) >= 0)}a {x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 == b) && ((len x4) >= 0) && ((sumLens x4) >= 0)}bforall <p :: [a]-> [a]-> Bool>.
x1:{x15 : [a]<\x16 VV -> (VV >= x16)> | ((len x15) >= 0)}
-> x2:[{x15 : [a]<\x16 VV -> (VV >= x16)><p x1> | ((len x15) >= 0)}]<p>
-> {x4 : [{x15 : [a]<\x16 VV -> (VV >= x16)> | ((len x15) >= 0)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}: forall a.
(Ord a) =>
x1:{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x1))}mergePairs {x4 : [{x8 : [a]<\x9 VV -> (VV >= x9)> | ((len x8) >= 0)}]<\_ VV -> ((len x6) >= 0)> | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}xs
347: mergePairs [x]      = {x6 : [{x8 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}[{x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 == a) && ((len x4) >= 0) && ((sumLens x4) >= 0)}x]
348: mergePairs []       = forall <p :: [a]-> [a]-> Bool>.
{x4 : [{x6 : [{VV : a | false}]<\_ VV -> false> | false}]<p> | (((null x4)) <=> true) && ((len x4) == 0) && ((sumLens x4) == 0)}[]
Phew! ----- Lets see one last example... Example: Binary Trees --------------------- ... `Map` from keys of type `k` to values of type `a`
Implemented, in `Data.Map` as a binary tree: 
371: data Map k a = Tip
372:              | Bin Size k a (Map k a) (Map k a)
373: 
374: type Size    = Int
Two Abstract Refinements ------------------------ - `l` : relates root `key` with `left`-subtree keys - `r` : relates root `key` with `right`-subtree keys 
385: {-@ data Map k a < l :: k -> k -> Prop
386:                  , r :: k -> k -> Prop >
387:     = Tip
388:     | Bin (sz :: Size) (key :: k) (val :: a)
389:           (left  :: Map <l,r> (k<l key>) a)
390:           (right :: Map <l,r> (k<r key>) a) @-}
Ex: Binary Search Trees ----------------------- Keys are *Binary-Search* Ordered 
402: {-@ type BST k a = 
403:       Map <{\r v -> v < r }, 
404:            {\r v -> v > r }> 
405:           k a                   @-}
Ex: Minimum Heaps ----------------- Root contains *minimum* value 
416: {-@ type MinHeap k a = 
417:       Map <{\r v -> r <= v}, 
418:            {\r v -> r <= v}> 
419:            k a               @-}
Ex: Maximum Heaps ----------------- Root contains *maximum* value 
430: {-@ type MaxHeap k a = 
431:       Map <{\r v -> r >= v}, 
432:            {\r v -> r >= v}> 
433:            k a               @-}
Example: Data.Map ----------------- Standard Key-Value container -
1300+ non-comment lines
-
`insert`, `split`, `merge`,...
-
Rotation, Rebalance,...
SMT & inference crucial for [verification](https://github.com/ucsd-progsys/liquidhaskell/blob/master/benchmarks/esop2013-submission/Base.hs)

Demo:Try online!
Recap: Abstract Refinements ---------------------------
Decouple invariants from *functions* + `max` + `loop` + `foldr`
Decouple invariants from *data* + `Vector` + `List` + `Tree`
Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3. **Measures:** Strengthened Constructors 4. **Abstract Refinements:* Decouple Invariants 5.
Er, what of *lazy evaluation*?