# Recursive Invariants

```7: module List where
```

# Recursive Invariants

Recall the definition of lists

```17: infixr `C`
18: data L a = N | C a (L a)
```

Lets parameterize the definition with an abstract refinement `p`

```24: {-@ data L a <p :: a -> a -> Prop>
25:       = N
26:       | C (h :: a) (tl :: (L <p> a<p h>))
27:   @-}
```
• `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

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

# Recursive Invariants: Example

If we unfold the list once we get

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

# Recursive Invariants: Example

If we unfold the list a second time we get

_
```61: h1       :: a
62: h2       :: a<p h1>
63: h3 `C` N :: L <p> a<p h1 && p h2>
```

# Recursive Invariants: Example

Finally, with a third unfold we get

_
```72: h1 :: a
73: h2 :: a<p h1>
74: h3 :: a<p h1 && p h2>
75: 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

```104: {-@ 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...

```119: {-@ slist :: SL Int @-}
120: slist :: L Int
121: (List.L <\hd VV -> (hd <= VV)> (GHC.Types.Int))slist = {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
h_List.C:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p h_List.C> | (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>.
h_List.C:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p h_List.C> | (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>.
h_List.C:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p h_List.C> | (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:

```128: {-@ slist' :: SL Int @-}
129: slist' :: L Int
130: (List.L <\hd VV -> (hd <= VV)> (GHC.Types.Int))slist' = {VV : (GHC.Types.Int) | (VV == (6  :  int))}6 forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
h_List.C:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p h_List.C> | (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>.
h_List.C:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p h_List.C> | (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>.
h_List.C:{VV : (GHC.Types.Int) | (VV > 0)}
-> (List.L <p> {VV : (GHC.Types.Int)<p h_List.C> | (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.

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

The hard work is done by `insert` defined as

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

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

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

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

# Insertion Sort

Now we can verify the usual sorting algorithms:

```193: {-@ insertSort :: (Ord a) => xs:[a] -> OList a @-}
194: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\hd VV -> (hd <= VV)>insertSort [a]xs  = (a
-> {VV : [a]<\x4 VV -> (x4 <= VV)> | ((len VV) >= 0)}
-> {VV : [a]<\x4 VV -> (x4 <= VV)> | ((len VV) >= 0)})
-> {VV : [a]<\x4 VV -> (x4 <= VV)> | ((len VV) >= 0)}
-> [a]
-> {VV : [a]<\x4 VV -> (x4 <= VV)> | ((len VV) >= 0)}foldr a
-> {VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) > 0)}insert {VV : [{VV : a | false}]<\_ VV -> false> | ((len VV) == 0) && ((len VV) >= 0)}[] {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs
```

where the helper does the work

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

# Merge Sort

Now we can verify the usual sorting algorithms:

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

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

# QuickSort

Now we can verify the usual sorting algorithms:

```243: {-@ quickSort    :: (Ord a) => [a] -> OList a @-}
244: 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> | ((len VV) == 0)}[]
245: quickSort (x:xs) = x1:a
-> {VV : [{VV : a | (VV < x1)}]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> {VV : [{VV : a | (VV >= x1)}]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) > 0)}append {VV : a | (VV == x)}x {VV : [{VV : a | (VV < x)}]<\x1 VV -> (VV >= x1)> | (VV == lts) && ((len VV) >= 0)}lts {VV : [{VV : a | (VV >= x)}]<\x1 VV -> (VV >= x1)> | (VV == gts) && ((len VV) >= 0)}gts
246:   where
247:     {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)}[ay | y <- {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs, ay x:a -> y:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x < y))}< {VV : a | (VV == x)}x]
248:     {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 | (VV >= x)}]<\_ VV -> (VV >= x)> | ((len VV) >= 0)}[az | z <- {VV : [a] | (VV == xs) && ((len VV) >= 0)}xs, az x:a -> y:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x >= y))}>= {VV : a | (VV == x)}x]
```

We require a special `append` parameterized by the pivot

```254: forall a.
k:a
-> {VV : [{VV : a | (VV < k)}]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> {VV : [{VV : a | (k <= VV)}]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) > 0)}append ak []     {VV : [{VV : a | (k <= VV)}]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}ys  = {VV : a | (VV == k)}k forall <p :: a-> a-> Bool>.
y:{VV : a | (k <= VV)}
-> ys:[{VV : a<p y> | (k <= VV)}]<p>
-> {VV : [{VV : a | (k <= VV)}]<p> | ((len VV) == (1 + (len ys)))}: {VV : [{VV : a | (k <= VV)}]<\x1 VV -> (VV >= x1)> | (VV == ys) && ((len VV) >= 0)}ys
255: append k (x:xs) ys  = {VV : a | (VV == x) && (VV < k)}x forall <p :: a-> a-> Bool>.
y:{VV : a | (x <= VV)}
-> ys:[{VV : a<p y> | (x <= VV)}]<p>
-> {VV : [{VV : a | (x <= VV)}]<p> | ((len VV) == (1 + (len ys)))}: forall a.
k:a
-> {VV : [{VV : a | (VV < k)}]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> {VV : [{VV : a | (k <= VV)}]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) > 0)}append {VV : a | (VV == k)}k {VV : [{VV : a | (VV >= x) && (VV < k)}]<\x1 VV -> (VV >= x1)> | (VV == xs) && ((len VV) >= 0)}xs {VV : [{VV : a | (k <= VV)}]<\x1 VV -> (VV >= x1)> | (VV == ys) && ((len 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

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

After which we can check that

```275: {-@ decList :: DecrList Int @-}
276: decList :: [Int]
277: [(GHC.Types.Int)]<\hd VV -> (hd >= VV)>decList = {VV : [{VV : (GHC.Types.Int) | (VV >= 0)}]<\x3 VV -> (x3 /= VV) && (VV >= 0) && (x3 >= VV) && (VV < x3)> | ((len 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

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

After which we can check that

```294: {-@ diffList :: DiffList Int @-}
295: diffList :: [Int]
296: [(GHC.Types.Int)]<\hd VV -> (hd /= VV)>diffList = {VV : [{VV : (GHC.Types.Int) | (VV >= 0)}]<\x3 VV -> (x3 /= VV) && (VV >= 0) && (x3 >= VV) && (VV < x3)> | ((len 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:

```308: data Map k a = Tip
309:              | Bin Size k a (Map k a) (Map k a)
310:
311: 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

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

# Ordered Trees

Thus, if we instantiate the refinements thus:

```344: {-@ type BST k a     = Map <{\r v -> v < r }, {\r v -> v > r }> k a @-}
345: {-@ type MinHeap k a = Map <{\r v -> r <= v}, {\r v -> r <= v}> k a @-}
346: {-@ 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
```364: empty :: BST k a
365:
366: insert :: Ord k => k:k -> a:a -> t:BST k a -> BST k a
367:
368: delete :: (Ord k) => k:k -> t:BST k a -> BST k a
```

# Binary Search Ordering: Empty

```375: {-@ empty :: BST k a @-}
376: empty     :: Map k a
377: forall a b. (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> 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

```384: {-@ insertBST :: Ord k => k:k -> a:a -> t:BST k a -> BST k a @-}
385: insertBST     :: Ord k => k -> a -> Map k a -> Map k a
386: forall a b.
(GHC.Classes.Ord a) =>
a
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)insertBST akx ax (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)t
387:   = case {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b) | (VV == t)}t of
388:      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
389:      Bin sz ky y l r
390:          -> case x:a
-> y:a
-> {VV : (GHC.Types.Ordering) | ((VV == EQ) <=> (x == y)) && ((VV == GT) <=> (x > y)) && ((VV == LT) <=> (x < y))}compare {VV : a | (VV == kx)}kx {VV : a | (VV == ky)}ky of
391:               LT -> key:a
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < key)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)balance {VV : a | (VV == ky)}ky {VV : a | (VV == y)}y ({VV : a | (VV < ky)}
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < ky)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < ky)} b)insertBST {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < ky)} b) | (VV == l)}l) {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > ky)} b) | (VV == r)}r
392:               GT -> key:a
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < key)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)balance {VV : a | (VV == ky)}ky {VV : a | (VV == y)}y {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < ky)} b) | (VV == l)}l ({VV : a | (ky < VV)}
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (ky < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (ky < VV)} b)insertBST {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > ky)} b) | (VV == r)}r)
393:               EQ -> forall <r :: a-> a-> Bool, l :: a-> a-> Bool>.
(GHC.Types.Int)
-> key_List.Bin:a
-> b
-> (List.Map <l, r> {VV : a<l key_List.Bin> | true} b)
-> (List.Map <l, r> {VV : a<r key_List.Bin> | 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 <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < ky)} b) | (VV == l)}l {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > ky)} b) | (VV == r)}r
```

# Binary Search Ordering: Delete

```400: {-@ delete :: (Ord k) => k:k -> t:BST k a -> BST k a @-}
401: delete :: Ord k => k -> Map k a -> Map k a
402: forall a b.
(GHC.Classes.Ord a) =>
a
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)delete ak (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)t
403:   = case {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b) | (VV == t)}t of
404:       Tip -> forall <r :: a-> a-> Bool, l :: a-> a-> Bool>.
(List.Map <l, r> {VV : a | false} {VV : b | false})Tip
405:       Bin _ kx x l r
406:           -> case x:a
-> y:a
-> {VV : (GHC.Types.Ordering) | ((VV == EQ) <=> (x == y)) && ((VV == GT) <=> (x > y)) && ((VV == LT) <=> (x < y))}compare {VV : a | (VV == k)}k {VV : a | (VV == kx)}kx of
407:                LT -> key:a
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < key)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)balance {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x ({VV : a | (VV < kx)}
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < kx)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < kx)} b)delete {VV : a | (VV == k)}k {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < kx)} b) | (VV == l)}l) {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > kx)} b) | (VV == r)}r
408:                GT -> key:a
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < key)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)balance {VV : a | (VV == kx)}kx {VV : a | (VV == x)}x {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < kx)} b) | (VV == l)}l ({VV : a | (VV > kx)}
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > kx)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > kx)} b)delete {VV : a | (VV == k)}k {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > kx)} b) | (VV == r)}r)
409:                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 <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < kx)} b) | (VV == l)}l {VV : (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > kx)} b) | (VV == r)}r
```

# Helper Functions: Constructors

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

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

# Helper Functions: Extractors

```438: 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>deleteFindMax (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> a b)t
439:   = case {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> a b) | (VV == t)}t of
440:       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 -> (VV > x2)> {VV : a | (VV < k)} b) | (VV == l)}l)
441:       Bin _ k x l r -> let ({VV : a | (VV == km3) && (VV > k)}km3, {VV : a | (VV == vm)}vm, {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV > k) && (VV < km3) && (VV < km3)} b) | (VV == rm)}rm) = 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>deleteFindMax (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV > k)} b)r in
442:                        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) && (VV > k)}km3, {VV : a | (VV == vm) && (VV == vm)}vm, (key:{VV : a | (VV < km3) && (VV < km3)}
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < key) && (VV < km3) && (VV < km3)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < km3) && (VV < km3) && (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {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 -> (VV > x2)> {VV : a | (VV < k)} b) | (VV == l)}l {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV > k) && (VV < km3) && (VV < km3)} b) | (VV == rm) && (VV == rm)}rm))
443:       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)}ms, [(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | (VV == ms) && ((len VV) >= 0)}ms, (List.Map <\_ VV -> false, \_ VV -> false> {VV : a | false} {VV : b | false})Tip)
444:   where
445:     [(GHC.Types.Char)]ms = [(GHC.Types.Char)]"Map.deleteFindMax : empty Map"
446:
447: 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
448:   = case {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> a b) | (VV == t)}t of
449:       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)
450:       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 -> (VV > x2)> {VV : a | (VV > km4) && (VV > km4) && (VV < k)} 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
451:                        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 | (VV > km4) && (VV > km4)}
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > km4) && (VV > km4) && (VV < key)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > km4) && (VV > km4) && (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV > km4) && (VV > km4)} b)balance {VV : a | (VV == k)}k {VV : a | (VV == x)}x {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV > km4) && (VV > km4) && (VV < k)} 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))
452:       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)}ms, [(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | (VV == ms) && ((len VV) >= 0)}ms, (List.Map <\_ VV -> false, \_ VV -> false> {VV : a | false} {VV : b | false})Tip)
453:   where
454:     [(GHC.Types.Char)]ms = [(GHC.Types.Char)]"Map.deleteFindMin : empty Map"
```

# Helper Functions: Connectors

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

```463: glue :: k -> Map k a -> Map k a -> Map k a
464: 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
465: glue k l Tip = (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (x2 < VV)> {VV : a | (VV < k)} b)l
466: glue k l r
467:   | (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 x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x > y))}> (List.Map {VV : a | (VV > k)} 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 -> (VV > x2)> {VV : a | (VV < k) && (VV < km1) && (VV < km1)} b) | (VV == lm)}lm) = (List.Map <\x4 VV -> (VV < x4), \x5 VV -> (VV > x5)> {VV : a | (VV < k)} b)
-> ({VV : a | (VV < k)}, b, (List.Map <\x2 VV -> (VV < x2), \x3 VV -> (VV > x3)> {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
468:                       in key:{VV : a | (VV /= k)}
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV /= k) && (VV < key)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV /= k) && (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {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 -> (VV > x2)> {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
469:
470:   | otherwise       = let ({VV : a | (VV == km2) && (VV > k)}km2, {VV : a | (VV == vm)}vm, {VV : (List.Map <\x1 VV -> (VV < x1), \x2 VV -> (VV > x2)> {VV : a | (VV > k) && (VV > km2) && (VV > km2)} b) | (VV == rm)}rm) = (List.Map <\x4 VV -> (VV < x4), \x5 VV -> (VV > x5)> {VV : a | (VV > k)} b)
-> ({VV : a | (VV > k)}, b, (List.Map <\x2 VV -> (VV < x2), \x3 VV -> (VV > x3)> {VV : a | (VV > k)} 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
471:                       in key:{VV : a | (VV /= k)}
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV /= k) && (VV < key)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV /= k) && (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV /= k)} b)balance {VV : a | (VV == km2) && (VV == km2) && (VV > k)}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 -> (VV > x2)> {VV : a | (VV > k) && (VV > km2) && (VV > km2)} b) | (VV == rm) && (VV == rm)}rm
472:
473: {-@ balance :: key:k
474:             -> a
475:             -> (BST {v:k | v < key} a)
476:             -> (BST {v:k| key < v} a) -> (BST k a) @-}
477: balance :: k -> a -> Map k a -> Map k a -> Map k a
478: forall a b.
key:a
-> b
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < key)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (key < VV)} b)
-> (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> a b)balance ak ax (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (VV < k)} b)l (List.Map <\r VV -> (VV < r), \r VV -> (VV > r)> {VV : a | (k < VV)} b)r = forall a. aundefined
```