7: module List where 8: 9: {-@ LIQUID "--no-termination" @-}
Recall the definition of lists
19: infixr `C` 20: data L a = N | C a (L a)
Lets parameterize the definition with an abstract refinement p
26: {-@ data L a <p :: a -> a -> Prop> 27: = N 28: | C (h :: a) (tl :: (L <p> a<p h>)) 29: @-}
p
is a binary relation between two a
values
definition relates head with all the tail elements
Recursive : So p
holds between every pair of list elements!
Consider a list with three elements
44: h1 `C` h2 `C` h3 `C` N :: L <p> a
If we unfold the list once we get
53: h1 :: a 54: h2 `C` h3 `C` N :: L <p> a<p h1>
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>
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.
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
106: {-@ type SL a = L <{\hd v -> hd <= v}> a @-}
The refinement says hd
is less than the arbitrary tail element v
.
Thus SL
denotes lists sorted in increasing order!
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
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.
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)}> @-}
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
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.
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!
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]
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]
Consider a Map
from keys of type k
to values of type a
Implemented as a binary tree:
310: data Map k a = Tip 311: | Bin Size k a (Map k a) (Map k a) 312: 313: type Size = Int
We abstract from the structure two refinements l
and r
l
relates root key
with left-subtree keys
r
relates root key
with right-subtree keys
326: {-@ 327: data Map k a <l :: k -> k -> Prop, r :: k -> k -> Prop> 328: = Tip 329: | Bin (sz :: Size) 330: (key :: k) 331: (value :: a) 332: (left :: Map <l, r> (k <l key>) a) 333: (right :: Map <l, r> (k <r key>) a) 334: @-}
Thus, if we instantiate the refinements thus:
346: {-@ type BST k a = Map <{\r v -> v < r }, {\r v -> v > r }> k a @-} 347: {-@ type MinHeap k a = Map <{\r v -> r <= v}, {\r v -> r <= v}> k a @-} 348: {-@ type MaxHeap k a = Map <{\r v -> r >= v}, {\r v -> r >= v}> k a @-}
BST k v
denotes binary-search ordered trees
MinHeap k v
denotes min-heap ordered trees
MaxHeap k v
denotes max-heap ordered trees.
We can use the BST
type to automatically verify that tricky functions ensure and preserve binary-search ordering.
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
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
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
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
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
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"
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