7: module List where
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!
Consider a list with three elements
42: h1 `C` h2 `C` h3 `C` N :: L <p> a
If we unfold the list once we get
51: h1 :: a 52: h2 `C` h3 `C` N :: L <p> a<p h1>
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>
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.
That was a rather abstract.
How would we use the fact that p
holds between every pair ?
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!
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
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.
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)}> @-}
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
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.
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!
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]
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]
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
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: @-}
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.
We can use the BST
type to automatically verify that tricky functions ensure and preserve binary-search ordering.
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
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
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
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
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
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"
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