Recursive Invariants

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:   @-}

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 @-}

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

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

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 @-}

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