# Recursive Invariants

```7: module List where
8:
9: {-@ LIQUID "--no-termination" @-}
```

# Recursive Invariants

Recall the definition of lists

```19: infixr `C`
20: data L a = N | C a (L a)
```

Lets parameterize the definition with an abstract refinement `p`

```26: {-@ data L a <p :: a -> a -> Prop>
27:       = N
28:       | C (h :: a) (tl :: (L <p> a<p h>))
29:   @-}
```
• `p` is a binary relation between two `a` values

• definition relates head with all the tail elements

Recursive : So `p` holds between every pair of list elements!

# Recursive Invariants: Example

Consider a list with three elements

_
```44: h1 `C` h2 `C` h3 `C` N :: L <p> a
```

# Recursive Invariants: Example

If we unfold the list once we get

_
```53: h1              :: a
54: h2 `C` h3 `C` N :: L <p> a<p h1>
```

# Recursive Invariants: Example

If we unfold the list a second time we get

_
```63: h1       :: a
64: h2       :: a<p h1>
65: h3 `C` N :: L <p> a<p h1 && p h2>
```

# Recursive Invariants: Example

Finally, with a third unfold we get

_
```74: h1 :: a
75: h2 :: a<p h1>
76: h3 :: a<p h1 && p h2>
77: N  :: L <p> a<p h1 && p h2 && p h3>
```

Note how `p` holds between every pair of elements in the list.

# Using Recursive Invariants

That was a rather abstract.

How would we use the fact that `p` holds between every pair ?

# Using Recursive Invariants

That was a rather abstract.

How would we use the fact that `p` holds between every pair ?

Lets instantiate `p` with a concrete refinement

```106: {-@ type SL a = L <{\hd v -> hd <= v}> a @-}
```
• The refinement says `hd` is less than the arbitrary tail element `v`.

• Thus `SL` denotes lists sorted in increasing order!

# Using Recursive Invariants

LiquidHaskell verifies that the following list is indeed increasing...

```121: {-@ slist :: SL Int @-}
122: slist :: L Int
123: (List.L <\hd2 VV -> (hd2 <= VV)> (GHC.Types.Int))slist = {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p x1> | (VV > 0)})
-> (List.L <p> {VV : (GHC.Types.Int) | (VV > 0)})`C` {VV : (GHC.Types.Int) | (VV == (6  :  int))}6 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p x1> | (VV > 0)})
-> (List.L <p> {VV : (GHC.Types.Int) | (VV > 0)})`C` {VV : (GHC.Types.Int) | (VV == (12  :  int))}12 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p x1> | (VV > 0)})
-> (List.L <p> {VV : (GHC.Types.Int) | (VV > 0)})`C` (List.L <\_ VV -> false> {VV : (GHC.Types.Int) | false})N
```

... and complains that the following is not:

```130: {-@ slist' :: SL Int @-}
131: slist' :: L Int
132: (List.L <\hd2 VV -> (hd2 <= VV)> (GHC.Types.Int))slist' = {VV : (GHC.Types.Int) | (VV == (6  :  int))}6 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p x1> | (VV > 0)})
-> (List.L <p> {VV : (GHC.Types.Int) | (VV > 0)})`C` {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p x1> | (VV > 0)})
-> (List.L <p> {VV : (GHC.Types.Int) | (VV > 0)})`C` {VV : (GHC.Types.Int) | (VV == (12  :  int))}12 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p x1> | (VV > 0)})
-> (List.L <p> {VV : (GHC.Types.Int) | (VV > 0)})`C` (List.L <\_ VV -> false> {VV : (GHC.Types.Int) | false})N
```

# InsertSort

More interestingly, we can verify that various sorting algorithms return sorted lists.

```144: {-@ insertSort' :: (Ord a) => [a] -> SL a @-}
145: insertSort'     :: (Ord a) => [a] -> L a
146: forall a.
(GHC.Classes.Ord a) =>
[a] -> (List.L <\hd2 VV -> (hd2 <= VV)> a)insertSort'     = (a
-> (List.L <\x4 VV -> (VV >= x4)> a)
-> (List.L <\x4 VV -> (VV >= x4)> a))
-> (List.L <\x4 VV -> (VV >= x4)> a)
-> [a]
-> (List.L <\x4 VV -> (VV >= x4)> a)foldr a
-> (List.L <\x2 VV -> (VV >= x2)> a)
-> (List.L <\x1 VV -> (VV >= x1)> a)insert' (List.L <\_ VV -> false> {VV : a | false})N
```

The hard work is done by `insert` defined as

```152: forall a.
(GHC.Classes.Ord a) =>
a
-> (List.L <\x2 VV -> (x2 <= VV)> a)
-> (List.L <\x1 VV -> (VV >= x1)> a)insert' ay N                      = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV == y)}
-> (List.L <p> {VV : a<p x1> | (VV == y)})
-> (List.L <p> {VV : a | (VV == y)})`C` (List.L <\_ VV -> false> {VV : a | false})N
153: insert' y (x `C` xs) | {VV : a | (VV == y)}y x1:a
-> x2:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : a | (VV == x)}x    = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x1:{VV : a | (y <= VV)}
-> (List.L <p> {VV : a<p x1> | (y <= VV)})
-> (List.L <p> {VV : a | (y <= VV)})`C` {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= x) && (VV >= y)}
-> (List.L <p> {VV : a<p x1> | (VV >= x) && (VV >= y)})
-> (List.L <p> {VV : a | (VV >= x) && (VV >= y)})`C` {VV : (List.L <\x1 VV -> (x1 <= VV)> {VV : a | (x <= VV)}) | (VV == xs)}xs
154:                      | otherwise = {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= x)}
-> (List.L <p> {VV : a<p x1> | (VV >= x)})
-> (List.L <p> {VV : a | (VV >= x)})`C` forall a.
(GHC.Classes.Ord a) =>
a
-> (List.L <\x2 VV -> (x2 <= VV)> a)
-> (List.L <\x1 VV -> (VV >= x1)> a)insert' {VV : a | (VV == y)}y {VV : (List.L <\x1 VV -> (x1 <= VV)> {VV : a | (x <= VV)}) | (VV == xs)}xs
```

Hover the mouse over `insert'` to see what type was inferred for it.

# Analyzing Plain Lists

Demo:

We can easily modify GHC's List definition to abstract over a refinement:

_
```172: data [a] <p :: a -> a -> Prop>
173:   = []
174:   | (:) (h :: a) (tl :: ([a<p h>]<p>))
```

So, we can define and use ordered versions of GHC Lists

```184: {-@ type OList a = [a]<{\hd v -> (hd <= v)}> @-}
```

# Insertion Sort

Now we can verify the usual sorting algorithms:

```195: {-@ insertSort :: (Ord a) => xs:[a] -> OList a @-}
196: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\hd6 VV -> (hd6 <= VV)>insertSort [a]xs  = (a
-> {VV : [a]<\x4 VV -> (VV >= x4)> | ((len VV) >= 0)}
-> {VV : [a]<\x4 VV -> (VV >= x4)> | ((len VV) >= 0)})
-> {VV : [a]<\x4 VV -> (VV >= x4)> | ((len VV) >= 0)}
-> [a]
-> {VV : [a]<\x4 VV -> (VV >= x4)> | ((len VV) >= 0)}foldr a
-> x2:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x2) && ((len VV) > 0) && ((len VV) > (len x2))}insert {VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((sumLens VV) == 0) && ((len VV) >= 0) && ((sumLens VV) >= 0)}[] {VV : [a] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs
```

where the helper does the work

```206: forall a.
(GHC.Classes.Ord a) =>
a
-> x1:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}insert ay []                   = {VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((sumLens VV) == 0) && ((len VV) >= 0) && ((sumLens VV) >= 0)}[{VV : a | (VV == y)}y]
207: insert y (x : xs) | {VV : a | (VV == y)}y x1:a
-> x2:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : a | (VV == x)}x    = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= y)}
-> x2:[{VV : a<p x1> | (VV >= y)}]<p>
-> {VV : [{VV : a | (VV >= y)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}: {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= x) && (VV >= y)}
-> x2:[{VV : a<p x1> | (VV >= x) && (VV >= y)}]<p>
-> {VV : [{VV : a | (VV >= x) && (VV >= y)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}: {VV : [{VV : a | (x <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs
208:                   | otherwise = {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= x)}
-> x2:[{VV : a<p x1> | (VV >= x)}]<p>
-> {VV : [{VV : a | (VV >= x)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}: forall a.
(GHC.Classes.Ord a) =>
a
-> x1:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}insert {VV : a | (VV == y)}y {VV : [{VV : a | (x <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs
```

# Merge Sort

Now we can verify the usual sorting algorithms:

```218: {-@ mergeSort :: (Ord a) => [a] -> OList a @-}
219: mergeSort     :: Ord a => [a] -> [a]
220: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\hd6 VV -> (hd6 <= VV)>mergeSort []  = forall <p :: a-> a-> Bool>.
{VV : [{VV : a | false}]<p> | (((null VV)) <=> true) && ((len VV) == 0) && ((sumLens VV) == 0)}[]
221: mergeSort [x] = {VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((sumLens VV) == 0) && ((len VV) >= 0) && ((sumLens VV) >= 0)}[{VV : a | (VV == x)}x]
222: mergeSort xs  = forall a.
(GHC.Classes.Ord a) =>
xs:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge ([a] -> [a]<\hd6 VV -> (hd6 <= VV)>mergeSort {VV : [a] | (VV == xs1) && (VV == xs1) && ((len VV) == (len xs1)) && ((len VV) >= 0) && ((len VV) >= (len xs2)) && ((sumLens VV) >= 0)}xs1) ([a] -> [a]<\hd6 VV -> (hd6 <= VV)>mergeSort {VV : [a] | (VV == xs2) && (VV == xs2) && ((len VV) == (len xs2)) && ((len VV) >= 0) && ((sumLens VV) >= 0) && ((len VV) <= (len xs1)) && ((len VV) <= (len xs1))}xs2)
223:   where
224:    ({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) = 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 {VV : [a] | ((len VV) >= 0) && ((sumLens VV) >= 0)}xs
225:
226: split :: [a]    -> ([a], [a])
227: 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}
-> {VV : (a, b)<p2> | ((fst VV) == x1) && ((snd VV) == x2)}({VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {VV : [a]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}:{VV : [a] | (VV == xs) && (VV == xs) && ((len VV) == (len xs)) && ((len VV) >= 0) && ((len VV) >= (len ys)) && ((sumLens VV) >= 0) && ((len VV) <= (len zs))}xs, {VV : a | (VV == y)}yforall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {VV : [a]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}:{VV : [a] | (VV == ys) && (VV == ys) && ((len VV) == (len ys)) && ((len VV) >= 0) && ((sumLens VV) >= 0) && ((len VV) <= (len xs)) && ((len VV) <= (len xs)) && ((len VV) <= (len zs))}ys) where ({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 {VV : [a] | (VV == zs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}zs
228: split xs         = forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : (a, b)<p2> | ((fst VV) == x1) && ((snd VV) == x2)}({VV : [a] | ((len VV) >= 0) && ((sumLens VV) >= 0)}xs, {VV : [{VV : a | false}]<\_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((sumLens VV) == 0) && ((len VV) >= 0) && ((sumLens VV) >= 0)}[])
229:
230: merge :: Ord a => [a] -> [a] -> [a]
231: forall a.
(GHC.Classes.Ord a) =>
xs:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}xs [] = {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs
232: merge [] ys = {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0) && ((sumLens VV) >= 0)}ys
233: merge (x:xs) (y:ys) | {VV : a | (VV == x)}x x1:a
-> x2:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : a | (VV == y)}y    = {VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
x1:{VV : a | (x <= VV)}
-> x2:[{VV : a<p x1> | (x <= VV)}]<p>
-> {VV : [{VV : a | (x <= VV)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}:(forall a.
(GHC.Classes.Ord a) =>
xs:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge {VV : [{VV : a | (x <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs ({VV : a | (VV == y)}yforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= x) && (VV >= y)}
-> x2:[{VV : a<p x1> | (VV >= x) && (VV >= y)}]<p>
-> {VV : [{VV : a | (VV >= x) && (VV >= y)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}:{VV : [{VV : a | (y <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == ys) && ((len VV) >= 0) && ((sumLens VV) >= 0)}ys))
234:                     | otherwise = {VV : a | (VV == y)}yforall <p :: a-> a-> Bool>.
x1:{VV : a | (y <= VV)}
-> x2:[{VV : a<p x1> | (y <= VV)}]<p>
-> {VV : [{VV : a | (y <= VV)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}:(forall a.
(GHC.Classes.Ord a) =>
xs:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}merge ({VV : a | (VV == x)}xforall <p :: a-> a-> Bool>.
x1:{VV : a | (y < VV) && (x <= VV)}
-> x2:[{VV : a<p x1> | (y < VV) && (x <= VV)}]<p>
-> {VV : [{VV : a | (y < VV) && (x <= VV)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}:{VV : [{VV : a | (x <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs) {VV : [{VV : a | (y <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == ys) && ((len VV) >= 0) && ((sumLens VV) >= 0)}ys)
```

A significant amount of inference happens above. See the types.

# QuickSort

Now we can verify the usual sorting algorithms:

```245: {-@ quickSort    :: (Ord a) => [a] -> OList a @-}
246: forall a.
(GHC.Classes.Ord a) =>
[a] -> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}quickSort []     = forall <p :: a-> a-> Bool>.
{VV : [{VV : a | false}]<p> | (((null VV)) <=> true) && ((len VV) == 0) && ((sumLens VV) == 0)}[]
247: quickSort (x:xs) = x1:a
-> x2:{VV : [{VV : a | (VV < x1)}]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x3:{VV : [{VV : a | (VV >= x1)}]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x2) && (VV /= x3) && ((len VV) > 0) && ((len VV) > (len x2)) && ((len VV) > (len x3))}append {VV : a | (VV == x)}x {VV : [{VV : a | (VV < x)}]<\x1 VV -> (VV >= x1)> | (VV == lts) && ((len VV) >= 0) && ((sumLens VV) >= 0)}lts {VV : [{VV : a | (VV >= x)}]<\x1 VV -> (VV >= x1)> | (VV == gts) && ((len VV) >= 0) && ((sumLens VV) >= 0)}gts
248:   where
249:     {VV : [{VV : a | (VV < x)}]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}lts          = forall a.
(GHC.Classes.Ord a) =>
[a] -> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}quickSort {VV : [{VV : a | (VV < x)}]<\_ VV -> (VV < x)> | ((len VV) >= 0) && ((sumLens VV) >= 0) && ((len VV) <= (len xs))}[ay | y <- {VV : [a] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs, ay x1:a
-> x2:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 < x2))}< {VV : a | (VV == x)}x]
250:     {VV : [{VV : a | (VV >= x)}]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}gts          = forall a.
(GHC.Classes.Ord a) =>
[a] -> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}quickSort {VV : [{VV : a | (x <= VV)}]<\_ VV -> (VV >= x)> | ((len VV) >= 0) && ((sumLens VV) >= 0) && ((len VV) <= (len xs))}[az | z <- {VV : [a] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs, az x1:a
-> x2:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 >= x2))}>= {VV : a | (VV == x)}x]
```

We require a special `append` parameterized by the pivot

```256: forall a.
k:a
-> x1:{VV : [{VV : a | (VV < k)}]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> ys:{VV : [{VV : a | (VV >= k)}]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && (VV /= ys) && ((len VV) > 0) && ((len VV) > (len x1)) && ((len VV) > (len ys))}append ak []     {VV : [{VV : a | (VV >= k)}]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}ys  = {VV : a | (VV == k)}k forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= k)}
-> x2:[{VV : a<p x1> | (VV >= k)}]<p>
-> {VV : [{VV : a | (VV >= k)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}: {VV : [{VV : a | (VV >= k)}]<\x1 VV -> (VV >= x1)> | (VV == ys) && ((len VV) >= 0) && ((sumLens VV) >= 0)}ys
257: append k (x:xs) ys  = {VV : a | (VV == x) && (VV < k)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= x)}
-> x2:[{VV : a<p x1> | (VV >= x)}]<p>
-> {VV : [{VV : a | (VV >= x)}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2))) && ((sumLens VV) == ((len x1) + (sumLens x2)))}: forall a.
k:a
-> x1:{VV : [{VV : a | (VV < k)}]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> ys:{VV : [{VV : a | (VV >= k)}]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | (VV /= x1) && (VV /= ys) && ((len VV) > 0) && ((len VV) > (len x1)) && ((len VV) > (len ys))}append {VV : a | (VV == k)}k {VV : [{VV : a | (VV < k) && (x <= VV)}]<\x1 VV -> (x1 <= VV)> | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs {VV : [{VV : a | (VV >= k)}]<\x1 VV -> (VV >= x1)> | (VV == ys) && ((len VV) >= 0) && ((sumLens VV) >= 0)}ys
```

Look at the inferred type to understand why!

# Other Instantiations: Decreasing Lists

We may instantiate `p` with many different concrete relations

Decreasing Lists

```271: {-@ type DecrList a = [a]<{\hd v -> (hd >= v)}> @-}
```

After which we can check that

```277: {-@ decList :: DecrList Int @-}
278: decList :: [Int]
279: [(GHC.Types.Int)]<\hd13 VV -> (hd13 >= VV)>decList = {VV : [{VV : (GHC.Types.Int) | (VV >= 0)}]<\x3 VV -> (x3 /= VV) && (VV >= 0) && (x3 >= VV) && (VV < x3)> | (((null VV)) <=> false) && ((len VV) >= 0) && ((sumLens VV) >= 0)}[{VV : (GHC.Types.Int) | (VV == (3  :  int))}3, {VV : (GHC.Types.Int) | (VV == (2  :  int))}2, {VV : (GHC.Types.Int) | (VV == (1  :  int))}1, {VV : (GHC.Types.Int) | (VV == (0  :  int))}0]
```

# Multiple Instantiations: Distinct Lists

We may instantiate `p` with many different concrete relations

Distinct Lists: Lists not containing any duplicate values

```290: {-@ type DiffList a = [a]<{\hd v -> (hd /= v)}> @-}
```

After which we can check that

```296: {-@ diffList :: DiffList Int @-}
297: diffList :: [Int]
298: [(GHC.Types.Int)]<\hd15 VV -> (hd15 /= VV)>diffList = {VV : [{VV : (GHC.Types.Int) | (VV >= 0)}]<\x3 VV -> (x3 /= VV) && (VV >= 0) && (x3 >= VV) && (VV < x3)> | (((null VV)) <=> false) && ((len VV) >= 0) && ((sumLens VV) >= 0)}[{VV : (GHC.Types.Int) | (VV == (2  :  int))}2, {VV : (GHC.Types.Int) | (VV == (3  :  int))}3, {VV : (GHC.Types.Int) | (VV == (1  :  int))}1, {VV : (GHC.Types.Int) | (VV == (0  :  int))}0]
```

# Binary Trees

• Consider a `Map` from keys of type `k` to values of type `a`

• Implemented as a binary tree:

```310: data Map k a = Tip
311:              | Bin Size k a (Map k a) (Map k a)
312:
313: type Size    = Int
```

# Binary Trees

We abstract from the structure two refinements `l` and `r`

• `l` relates root `key` with left-subtree keys

• `r` relates root `key` with right-subtree keys

```326: {-@
327:   data Map k a <l :: k -> k -> Prop, r :: k -> k -> Prop>
328:       = Tip
329:       | Bin (sz    :: Size)
330:             (key   :: k)
331:             (value :: a)
332:             (left  :: Map <l, r> (k <l key>) a)
333:             (right :: Map <l, r> (k <r key>) a)
334:   @-}
```

# Ordered Trees

Thus, if we instantiate the refinements thus:

```346: {-@ type BST k a     = Map <{\r v -> v < r }, {\r v -> v > r }> k a @-}
347: {-@ type MinHeap k a = Map <{\r v -> r <= v}, {\r v -> r <= v}> k a @-}
348: {-@ type MaxHeap k a = Map <{\r v -> r >= v}, {\r v -> r >= v}> k a @-}
```
• `BST k v` denotes binary-search ordered trees

• `MinHeap k v` denotes min-heap ordered trees

• `MaxHeap k v` denotes max-heap ordered trees.

# Binary Search Ordering

We can use the `BST` type to automatically verify that tricky functions ensure and preserve binary-search ordering.

Demo:

So, we can have
```366: empty :: BST k a
367:
368: insert :: Ord k => k:k -> a:a -> t:BST k a -> BST k a
369:
370: delete :: (Ord k) => k:k -> t:BST k a -> BST k a
```

# Binary Search Ordering: Empty

```377: {-@ empty :: BST k a @-}
378: empty     :: Map k a
379: forall a b.
(List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)empty     = forall <r :: a-> a-> Bool, l :: a-> a-> Bool>.
(List.Map <l, r> {VV : a | false} {VV : b | false})Tip
```

# Binary Search Ordering: Insert

```386: {-@ insertBST :: Ord k => k:k -> a:a -> t:BST k a -> BST k a @-}
387: insertBST     :: Ord k => k -> a -> Map k a -> Map k a
388: forall a b.
(GHC.Classes.Ord a) =>
a
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)insertBST akx ax (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)t
389:   = case {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b) | (VV == t)}t of
390:      Tip -> k:{VV : a | (VV == kx)}
-> x:{VV : b | (VV == x)}
-> (List.Map <\_ VV -> false, \_ VV -> false> {VV : a | (VV == k) && (VV == kx)} {VV : b | (VV == x) && (VV == x)})singleton {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x
391:      Bin sz ky y l r
392:          -> case x1:a
-> x2:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x1 == x2)) && ((VV == GHC.Types.GT) <=> (x1 > x2)) && ((VV == GHC.Types.LT) <=> (x1 < x2))}compare {VV : a | (VV == kx)}kx {VV : a | (VV == ky)}ky of
393:               LT -> key:a
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < key)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (key < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)balance {VV : a | (VV == ky)}ky {VV : a | (VV == y)}y ({VV : a | (VV < ky)}
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < ky)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < ky)} b)insertBST {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < ky)} b) | (VV == l)}l) {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV > ky)} b) | (VV == r)}r
394:               GT -> key:a
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < key)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (key < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)balance {VV : a | (VV == ky)}ky {VV : a | (VV == y)}y {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < ky)} b) | (VV == l)}l ({VV : a | (ky < VV)}
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (ky < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (ky < VV)} b)insertBST {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV > ky)} b) | (VV == r)}r)
395:               EQ -> forall <r :: a-> a-> Bool, l :: a-> a-> Bool>.
(GHC.Types.Int)
-> x2:a
-> b
-> (List.Map <l, r> {VV : a<l x2> | true} b)
-> (List.Map <l, r> {VV : a<r x2> | true} b)
-> (List.Map <l, r> a b)Bin {VV : (GHC.Types.Int) | (VV == sz)}sz {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < ky)} b) | (VV == l)}l {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV > ky)} b) | (VV == r)}r
```

# Binary Search Ordering: Delete

```402: {-@ delete :: (Ord k) => k:k -> t:BST k a -> BST k a @-}
403: delete :: Ord k => k -> Map k a -> Map k a
404: forall a b.
(GHC.Classes.Ord a) =>
a
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)delete ak (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)t
405:   = case {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b) | (VV == t)}t of
406:       Tip -> forall <r :: a-> a-> Bool, l :: a-> a-> Bool>.
(List.Map <l, r> {VV : a | false} {VV : b | false})Tip
407:       Bin _ kx x l r
408:           -> case x1:a
-> x2:a
-> {VV : (GHC.Types.Ordering) | ((VV == GHC.Types.EQ) <=> (x1 == x2)) && ((VV == GHC.Types.GT) <=> (x1 > x2)) && ((VV == GHC.Types.LT) <=> (x1 < x2))}compare {VV : a | (VV == k)}k {VV : a | (VV == kx)}kx of
409:                LT -> key:a
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < key)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (key < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)balance {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x ({VV : a | (VV < kx)}
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < kx)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < kx)} b)delete {VV : a | (VV == k)}k {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < kx)} b) | (VV == l)}l) {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV > kx)} b) | (VV == r)}r
410:                GT -> key:a
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < key)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (key < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)balance {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < kx)} b) | (VV == l)}l ({VV : a | (kx < VV)}
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (kx < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (kx < VV)} b)delete {VV : a | (VV == k)}k {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV > kx)} b) | (VV == r)}r)
411:                EQ -> k:a
-> (List.Map <\x5 VV -> (VV < x5), \x6 VV -> (x6 < VV)> {VV : a | (VV < k)} b)
-> (List.Map <\x3 VV -> (VV < x3), \x4 VV -> (x4 < VV)> {VV : a | (k < VV)} b)
-> (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV /= k)} b)glue {VV : a | (VV == kx)}kx {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < kx)} b) | (VV == l)}l {VV : (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV > kx)} b) | (VV == r)}r
```

# Helper Functions: Constructors

Below are the helper functions used by `insert` and `delete`:

```421: singleton :: k -> a -> Map k a
422: forall a b.
k:a
-> x:b
-> (List.Map <\_ VV -> false, \_ VV -> false> {VV : a | (VV == k)} {VV : b | (VV == x)})singleton ak ax
423:   = forall <r :: a-> a-> Bool, l :: a-> a-> Bool>.
(GHC.Types.Int)
-> x2:{VV : a | (VV == k)}
-> {VV : b | (VV == x)}
-> (List.Map <l, r> {VV : a<l x2> | (VV == k)} {VV : b | (VV == x)})
-> (List.Map <l, r> {VV : a<r x2> | (VV == k)} {VV : b | (VV == x)})
-> (List.Map <l, r> {VV : a | (VV == k)} {VV : b | (VV == x)})Bin {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 {VV : a | (VV == k)}k {VV : a | (VV == x)}x (List.Map <\_ VV -> false, \_ VV -> false> {VV : a | false} {VV : b | false})Tip (List.Map <\_ VV -> false, \_ VV -> false> {VV : a | false} {VV : b | false})Tip
424:
425: bin :: k -> a -> Map k a -> Map k a -> Map k a
426: forall a b.
a -> b -> (List.Map a b) -> (List.Map a b) -> (List.Map a b)bin ak ax (List.Map a b)l (List.Map a b)r
427:   = forall <r :: a-> a-> Bool, l :: a-> a-> Bool>.
(GHC.Types.Int)
-> x2:a
-> b
-> (List.Map <l, r> {VV : a<l x2> | true} b)
-> (List.Map <l, r> {VV : a<r x2> | true} b)
-> (List.Map <l, r> a b)Bin ((List.Map a b) -> (GHC.Types.Int)size {VV : (List.Map a b) | (VV == l)}l x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ (List.Map a b) -> (GHC.Types.Int)size {VV : (List.Map a b) | (VV == r)}r x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == (1  :  int))}1) {VV : a | (VV == k)}k {VV : a | (VV == x)}x {VV : (List.Map a b) | (VV == l)}l {VV : (List.Map a b) | (VV == r)}r
428:
429: size :: Map k a -> Int
430: forall a b. (List.Map a b) -> (GHC.Types.Int)size (List.Map a b)t
431:   = case {VV : (List.Map a b) | (VV == t)}t of
432:       Tip            -> x1:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x1  :  int))}0
433:       Bin sz _ _ _ _ -> {VV : (GHC.Types.Int) | (VV == sz)}sz
```

# Helper Functions: Extractors

```440: forall a b.
(List.Map <\x4 VV -> (VV < x4), \x5 VV -> (x5 < VV)> a b)
-> (a, b, (List.Map <\x2 VV -> (VV < x2), \x3 VV -> (VV > x3)> a b))<\_ VV -> True, \_ x1 VV -> True>deleteFindMax (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> a b)t
441:   = case {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> a b) | (VV == t)}t of
442:       Bin _ k x l Tip -> forall a b c <p3 :: b-> a-> c-> Bool, p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : c<p3 x2 x1> | true}
-> (a, b, c)<p2, p3>({VV : a | (VV == k)}k, {VV : a | (VV == x)}x, {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k)} b) | (VV == l)}l)
443:       Bin _ k x l r -> let ({VV : a | (VV == km3) && (k < VV)}km3, {VV : a | (VV == vm)}vm, {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < km3) && (VV < km3) && (k < VV)} b) | (VV == rm)}rm) = forall a b.
(List.Map <\x4 VV -> (VV < x4), \x5 VV -> (x5 < VV)> a b)
-> (a, b, (List.Map <\x2 VV -> (VV < x2), \x3 VV -> (VV > x3)> a b))<\_ VV -> True, \_ x1 VV -> True>deleteFindMax (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (k < VV)} b)r in
444:                        forall a b c <p3 :: b-> a-> c-> Bool, p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : c<p3 x2 x1> | true}
-> (a, b, c)<p2, p3>({VV : a | (VV == km3) && (VV == km3) && (k < VV)}km3, {VV : a | (VV == vm) && (VV == vm)}vm, (key:{VV : a | (VV < km3) && (VV < km3)}
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < key) && (VV < km3) && (VV < km3)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < km3) && (VV < km3) && (key < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < km3) && (VV < km3)} b)balance {VV : a | (VV == k)}k {VV : a | (VV == x)}x {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k)} b) | (VV == l)}l {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < km3) && (VV < km3) && (k < VV)} b) | (VV == rm) && (VV == rm)}rm))
445:       Tip           -> forall a b c <p3 :: b-> a-> c-> Bool, p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : c<p3 x2 x1> | true}
-> (a, b, c)<p2, p3>([(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | (VV == ms) && ((len VV) >= 0) && ((sumLens VV) >= 0)}ms, [(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | (VV == ms) && ((len VV) >= 0) && ((sumLens VV) >= 0)}ms, (List.Map <\_ VV -> false, \_ VV -> false> {VV : a | false} {VV : b | false})Tip)
446:   where
447:     [(GHC.Types.Char)]ms = [(GHC.Types.Char)]"Map.deleteFindMax : empty Map"
448:
449: forall a b.
(List.Map <\x4 VV -> (VV < x4), \x5 VV -> (VV > x5)> a b)
-> (a, b, (List.Map <\x2 VV -> (VV < x2), \x3 VV -> (VV > x3)> a b))<\_ VV -> True, \_ x1 VV -> True>deleteFindMin (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> a b)t
450:   = case {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> a b) | (VV == t)}t of
451:       Bin _ k x Tip r -> forall a b c <p3 :: b-> a-> c-> Bool, p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : c<p3 x2 x1> | true}
-> (a, b, c)<p2, p3>({VV : a | (VV == k)}k, {VV : a | (VV == x)}x, {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV > k)} b) | (VV == r)}r)
452:       Bin _ k x l r -> let ({VV : a | (VV == km4) && (VV < k)}km4, {VV : a | (VV == vm)}vm, {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k) && (km4 < VV) && (km4 < VV)} b) | (VV == lm)}lm) = forall a b.
(List.Map <\x4 VV -> (VV < x4), \x5 VV -> (VV > x5)> a b)
-> (a, b, (List.Map <\x2 VV -> (VV < x2), \x3 VV -> (VV > x3)> a b))<\_ VV -> True, \_ x1 VV -> True>deleteFindMin (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV < k)} b)l in
453:                        forall a b c <p3 :: b-> a-> c-> Bool, p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : c<p3 x2 x1> | true}
-> (a, b, c)<p2, p3>({VV : a | (VV == km4) && (VV == km4) && (VV < k)}km4, {VV : a | (VV == vm) && (VV == vm)}vm, (key:{VV : a | (km4 < VV) && (km4 < VV)}
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < key) && (km4 < VV) && (km4 < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (key < VV) && (km4 < VV) && (km4 < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (km4 < VV) && (km4 < VV)} b)balance {VV : a | (VV == k)}k {VV : a | (VV == x)}x {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k) && (km4 < VV) && (km4 < VV)} b) | (VV == lm) && (VV == lm)}lm {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV > k)} b) | (VV == r)}r))
454:       Tip             -> forall a b c <p3 :: b-> a-> c-> Bool, p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : c<p3 x2 x1> | true}
-> (a, b, c)<p2, p3>([(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | (VV == ms) && ((len VV) >= 0) && ((sumLens VV) >= 0)}ms, [(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | (VV == ms) && ((len VV) >= 0) && ((sumLens VV) >= 0)}ms, (List.Map <\_ VV -> false, \_ VV -> false> {VV : a | false} {VV : b | false})Tip)
455:   where
456:     [(GHC.Types.Char)]ms = [(GHC.Types.Char)]"Map.deleteFindMin : empty Map"
```

# Helper Functions: Connectors

Below are the helper functions used by `insert` and `delete`:

```465: glue :: k -> Map k a -> Map k a -> Map k a
466: forall a b.
k:a
-> (List.Map <\x5 VV -> (VV < x5), \x6 VV -> (x6 < VV)> {VV : a | (VV < k)} b)
-> (List.Map <\x3 VV -> (VV < x3), \x4 VV -> (x4 < VV)> {VV : a | (k < VV)} b)
-> (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV /= k)} b)glue ak Tip (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (k < VV)} b)r = {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (k < VV)} b) | (VV == r)}r
467: glue k l Tip = (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k)} b)l
468: glue k l r
469:   | (List.Map {VV : a | (VV < k)} b) -> (GHC.Types.Int)size (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k)} b)l x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 > x2))}> (List.Map {VV : a | (k < VV)} b) -> (GHC.Types.Int)size {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (k < VV)} b) | (VV == r)}r = let ({VV : a | (VV == km1) && (VV < k)}km1, {VV : a | (VV == vm)}vm, {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k) && (VV < km1) && (VV < km1)} b) | (VV == lm)}lm) = (List.Map <\x4 VV -> (VV < x4), \x5 VV -> (x5 < VV)> {VV : a | (VV < k)} b)
-> ({VV : a | (VV < k)}, b, (List.Map <\x2 VV -> (VV < x2), \x3 VV -> (x3 < VV)> {VV : a | (VV < k)} b))<\_ VV -> True, \_ x1 VV -> True>deleteFindMax (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k)} b)l
470:                       in key:{VV : a | (VV /= k)}
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV /= k) && (VV < key)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV /= k) && (key < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV /= k)} b)balance {VV : a | (VV == km1) && (VV == km1) && (VV < k)}km1 {VV : a | (VV == vm) && (VV == vm)}vm {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k) && (VV < km1) && (VV < km1)} b) | (VV == lm) && (VV == lm)}lm {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (k < VV)} b) | (VV == r)}r
471:
472:   | otherwise       = let ({VV : a | (VV == km2) && (k < VV)}km2, {VV : a | (VV == vm)}vm, {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (k < VV) && (km2 < VV) && (km2 < VV)} b) | (VV == rm)}rm) = (List.Map <\x4 VV -> (VV < x4), \x5 VV -> (x5 < VV)> {VV : a | (k < VV)} b)
-> ({VV : a | (k < VV)}, b, (List.Map <\x2 VV -> (VV < x2), \x3 VV -> (x3 < VV)> {VV : a | (k < VV)} b))<\_ VV -> True, \_ x1 VV -> True>deleteFindMin {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (k < VV)} b) | (VV == r)}r
473:                       in key:{VV : a | (VV /= k)}
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV /= k) && (VV < key)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV /= k) && (key < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV /= k)} b)balance {VV : a | (VV == km2) && (VV == km2) && (k < VV)}km2 {VV : a | (VV == vm) && (VV == vm)}vm (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k)} b)l {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (k < VV) && (km2 < VV) && (km2 < VV)} b) | (VV == rm) && (VV == rm)}rm
474:
475: {-@ balance :: key:k
476:             -> a
477:             -> (BST {v:k | v < key} a)
478:             -> (BST {v:k| key < v} a) -> (BST k a) @-}
479: balance :: k -> a -> Map k a -> Map k a -> Map k a
480: forall a b.
key:a
-> b
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < key)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (key < VV)} b)
-> (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> a b)balance ak ax (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (VV < k)} b)l (List.Map <\r21 VV -> (VV < r21), \r23 VV -> (VV > r23)> {VV : a | (k < VV)} b)r = forall a. aundefined
```