Abstract Refinements

5: module AbstractRefinements () where
6: 
7: import Language.Haskell.Liquid.Prelude
8: {-@ LIQUID "--no-termination" @-}

Abstract Refinements in Lists

Previous increasing Lists

17: data L a = N | C (x :: a) (xs :: L {v:a | x <= v})

Abstract over the refinement you care

22: data L a = N | C {forall a. (AbstractRefinements.L a) -> ax :: a, forall a. (AbstractRefinements.L a) -> (AbstractRefinements.L a)xs :: L a {- v:a | p v x -}}

Move it to the left-hand side

27: {-@ data L a <p :: a -> a -> Prop> = 
28:       N 
29:     | C (x :: a) (xs :: L <p> a<p x>)  @-}

We can get back increasing Lists:

36: {-@ type IncrL a = L <{\x v -> x <= v}> a @-}

Multiple Instantiations

Now increasing lists

44: type IncrL a = L <{\x v -> x <= v}> a

Co-exist with decreasing ones

50: type DecrL a = L <{\x v -> x >= v}> a

Ghc Sort

We can now verify algorithms that use both increasing and decreasing lists

59: {-@ type OList a = [a]<{\hd v -> hd <= v}> @-}
60: 
61: {-@ sort :: (Ord a) => [a] -> OList a  @-}
62: sort :: (Ord a) => [a] -> [a]
63: forall a. (GHC.Classes.Ord a) => [a] -> [a]<\hd4 VV -> (hd4 <= VV)>sort = {x5 : [{x9 : [a]<\x10 VV -> (x10 <= VV)> | ((len x9) >= 0)}]<\_ VV -> ((len x7) >= 0)> | ((len x5) > 0)}
-> {x2 : [a]<\x3 VV -> (x3 <= VV)> | ((len x2) >= 0)}mergeAll ({x24 : [{x28 : [a]<\x29 VV -> (x29 <= VV)> | ((len x28) >= 0)}]<\_ VV -> ((len x26) >= 0)> | ((len x24) > 0)}
 -> {x21 : [a]<\x22 VV -> (x22 <= VV)> | ((len x21) >= 0)})
-> ([a]
    -> {x24 : [{x28 : [a]<\x29 _ VV -> (x29 <= VV)> | ((len x28) >= 0)}]<\_ VV -> ((len x26) >= 0)> | ((len x24) > 0)})
-> [a]
-> exists [{x24 : [{x28 : [a]<\x29 _ VV -> (x29 <= VV)> | ((len x28) >= 0)}]<\_ VV -> ((len x26) >= 0)> | ((len x24) > 0)}].{x21 : [a]<\x22 VV -> (x22 <= VV)> | ((len x21) >= 0)}. [a]
-> {x2 : [{x6 : [a]<\x7 VV -> (x7 <= VV)> | ((len x6) >= 0)}]<\_ VV -> ((len x4) >= 0)> | ((len x2) > 0)}sequences
64:   where
65:     [a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences (a:b:xs)
66:       | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {x4 : GHC.Types.Ordering | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:GHC.Types.Ordering
-> x2:GHC.Types.Ordering
-> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 == x2))}== {x3 : GHC.Types.Ordering | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}GT = x1:a
-> {VV : [{VV : a | (VV > x1)}]<\x2 VV -> (VV > x2) && (VV > x1)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending {VV : a | (VV == b)}b {x3 : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null x3)) <=> false) && ((len x3) >= 0)}[{VV : a | (VV == a)}a]  {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs
67:       | otherwise           = x1:a
-> (x3:{VV : [{VV : a | (VV >= x1)}]<\x3 VV -> (x3 <= VV) && (x1 <= VV)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x3) && ((len VV) > 0) && ((len VV) > (len x3))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending  {VV : a | (VV == b)}b ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a)}
-> x2:[{VV : a<p x1> | (VV >= a)}]<p>
-> {x3 : [{VV : a | (VV >= a)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}:) {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs
68:     sequences [x] = {x4 : [{x6 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x4)) <=> true) && ((len x4) == 0) && ((len x4) >= 0)}[{x3 : [{VV : a | (VV == a)}]<\_ VV -> false> | (((null x3)) <=> false) && ((len x3) >= 0)}[{VV : a | (VV == a)}x]]
69:     sequences []  = {x4 : [{x6 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x4)) <=> true) && ((len x4) == 0) && ((len x4) >= 0)}[{x4 : [{VV : a | false}]<\_ VV -> false> | (((null x4)) <=> true) && ((len x4) == 0) && ((len x4) >= 0)}[]]
70: 
71:     x1:a
-> {VV : [{VV : a | (VV > x1)}]<\x2 VV -> (VV > x2) && (VV > x1)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending aa {VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | ((len VV) > 0)}as (b:bs)
72:       | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {x4 : GHC.Types.Ordering | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:GHC.Types.Ordering
-> x2:GHC.Types.Ordering
-> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 == x2))}== {x3 : GHC.Types.Ordering | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}GT = x1:a
-> {VV : [{VV : a | (VV > x1)}]<\x2 VV -> (VV > x2) && (VV > x1)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}descending {VV : a | (VV == b)}b ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > b) && (a <= VV)}
-> x2:[{VV : a<p x1> | (VV > b) && (a <= VV)}]<p>
-> {x3 : [{VV : a | (VV > b) && (a <= VV)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}:{x4 : [{VV : a | (VV > a)}]<\x5 VV -> (VV > a) && (VV > x5)> | (x4 == as) && ((len x4) > 0) && ((len x4) >= 0)}as) {x3 : [a] | (x3 == bs) && ((len x3) >= 0)}bs
73:     descending a as bs      = ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (a <= VV)}
-> x2:[{VV : a<p x1> | (a <= VV)}]<p>
-> {x3 : [{VV : a | (a <= VV)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}:{x4 : [{VV : a | (VV > a)}]<\x5 VV -> (VV > a) && (VV > x5)> | (x4 == as) && ((len x4) > 0) && ((len x4) >= 0)}as)forall <p :: [a]-> [a]-> Bool>.
x1:{x14 : [a]<\x15 VV -> (x15 <= VV)> | ((len x14) >= 0)}
-> x2:[{x14 : [a]<\x15 VV -> (x15 <= VV)><p x1> | ((len x14) >= 0)}]<p>
-> {x3 : [{x14 : [a]<\x15 VV -> (x15 <= VV)> | ((len x14) >= 0)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}: [a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences {x2 : [a] | ((len x2) >= 0)}bs
74: 
75:     x1:a
-> (x3:{VV : [{VV : a | (VV >= x1)}]<\x3 VV -> (x3 <= VV) && (x1 <= VV)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x3) && ((len VV) > 0) && ((len VV) > (len x3))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending aa x1:{VV : [{VV : a | (VV >= a)}]<\x2 VV -> (a <= VV) && (x2 <= VV)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}as (b:bs)
76:       | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {x4 : GHC.Types.Ordering | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:GHC.Types.Ordering
-> x2:GHC.Types.Ordering
-> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 /= x2))}/= {x3 : GHC.Types.Ordering | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}GT = x1:a
-> (x3:{VV : [{VV : a | (VV >= x1)}]<\x3 VV -> (x3 <= VV) && (x1 <= VV)> | ((len VV) > 0)}
    -> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x3) && ((len VV) > 0) && ((len VV) > (len x3))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}ascending {VV : a | (VV == b)}b (x1:{x7 : [{VV : a | (VV >= a) && (VV >= b)}]<\x8 VV -> (a <= VV) && (b <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}\{VV : [{VV : a | (VV >= a) && (VV >= b)}]<\x1 VV -> (a <= VV) && (b <= VV) && (x1 <= VV)> | ((len VV) > 0)}ys -> x1:{x7 : [{VV : a | (VV >= a)}]<\x8 VV -> (a <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}as ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a)}
-> x2:[{VV : a<p x1> | (VV >= a)}]<p>
-> {x3 : [{VV : a | (VV >= a)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}:{x4 : [{VV : a | (VV >= a) && (VV >= b)}]<\x5 VV -> (a <= VV) && (b <= VV) && (x5 <= VV)> | (x4 == ys) && ((len x4) > 0) && ((len x4) >= 0)}ys)) {x3 : [a] | (x3 == bs) && ((len x3) >= 0)}bs
77:     ascending a as bs       = x1:{x7 : [{VV : a | (VV >= a)}]<\x8 VV -> (a <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}as {x3 : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null x3)) <=> false) && ((len x3) >= 0)}[{VV : a | (VV == a)}a]forall <p :: [a]-> [a]-> Bool>.
x1:{x14 : [a]<\x15 VV -> (x15 <= VV)> | ((len x14) >= 0)}
-> x2:[{x14 : [a]<\x15 VV -> (x15 <= VV)><p x1> | ((len x14) >= 0)}]<p>
-> {x3 : [{x14 : [a]<\x15 VV -> (x15 <= VV)> | ((len x14) >= 0)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}: [a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}sequences {x2 : [a] | ((len x2) >= 0)}bs

Ghc Sort : Helper Functions

84: forall a.
(GHC.Classes.Ord a) =>
{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}mergeAll [x] = {x3 : [a]<\x4 VV -> (x4 <= VV)> | (x3 == x) && ((len x3) >= 0)}x
85: mergeAll xs  = forall a.
(GHC.Classes.Ord a) =>
{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}mergeAll (x1:{x10 : [{x14 : [a]<\x15 VV -> (VV >= x15)> | ((len x14) >= 0)}]<\_ VV -> ((len x12) >= 0)> | ((len x10) >= 0)}
-> {x3 : [{x7 : [a]<\x8 VV -> (x8 <= VV)> | ((len x7) >= 0)}]<\_ VV -> ((len x5) >= 0)> | ((len x3) >= 0) && ((len x3) <= (len x1))}mergePairs {x2 : [{x6 : [a]<\x7 VV -> (x7 <= VV)> | ((len x6) >= 0)}]<\_ VV -> ((len x4) >= 0)> | ((len x2) >= 0)}xs)
86: 
87: forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x2))}mergePairs (a:b:xs) = x1:{x10 : [a]<\x11 VV -> (VV >= x11)> | ((len x10) >= 0)}
-> x2:{x7 : [a]<\x8 VV -> (VV >= x8)> | ((len x7) >= 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | ((len x4) >= 0) && ((len x4) >= (len x1)) && ((len x4) >= (len x2))}merge1 {x3 : [a]<\x4 VV -> (x4 <= VV)> | (x3 == a) && ((len x3) >= 0)}a {x3 : [a]<\x4 VV -> (x4 <= VV)> | (x3 == b) && ((len x3) >= 0)}bforall <p :: [a]-> [a]-> Bool>.
x1:{x14 : [a]<\x15 VV -> (x15 <= VV)> | ((len x14) >= 0)}
-> x2:[{x14 : [a]<\x15 VV -> (x15 <= VV)><p x1> | ((len x14) >= 0)}]<p>
-> {x3 : [{x14 : [a]<\x15 VV -> (x15 <= VV)> | ((len x14) >= 0)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}: forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x2))}mergePairs {x3 : [{x7 : [a]<\x8 VV -> (x8 <= VV)> | ((len x7) >= 0)}]<\_ VV -> ((len x5) >= 0)> | (x3 == xs) && ((len x3) >= 0)}xs
88: mergePairs [x]      = {x4 : [{x6 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x4)) <=> true) && ((len x4) == 0) && ((len x4) >= 0)}[{x3 : [a]<\x4 VV -> (x4 <= VV)> | (x3 == a) && ((len x3) >= 0)}x]
89: mergePairs []       = forall <p :: [a]-> [a]-> Bool>.
{x3 : [{x5 : [{VV : a | false}]<\_ VV -> false> | false}]<p> | (((null x3)) <=> true) && ((len x3) == 0)}[]
90: 
91: forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x3:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x2)) && ((len VV) >= (len x3))}merge1 (a:as') (b:bs')
92:   | {VV : a | (VV == a)}a x1:a
-> x2:a
-> {x4 : GHC.Types.Ordering | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}`compare` {VV : a | (VV == b)}b x1:GHC.Types.Ordering
-> x2:GHC.Types.Ordering
-> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 == x2))}== {x3 : GHC.Types.Ordering | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}GT = {VV : a | (VV == b)}bforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= b)}
-> x2:[{VV : a<p x1> | (VV >= b)}]<p>
-> {x3 : [{VV : a | (VV >= b)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}:forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x3:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x2)) && ((len VV) >= (len x3))}merge1 ({VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > b) && (VV >= a)}
-> x2:[{VV : a<p x1> | (VV > b) && (VV >= a)}]<p>
-> {x3 : [{VV : a | (VV > b) && (VV >= a)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}:{x3 : [{VV : a | (a <= VV)}]<\x4 VV -> (x4 <= VV)> | (x3 == as') && ((len x3) >= 0)}as')  {x3 : [{VV : a | (VV >= b)}]<\x4 VV -> (VV >= x4)> | (x3 == bs') && ((len x3) >= 0)}bs'
93:   | otherwise           = {VV : a | (VV == a)}aforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a)}
-> x2:[{VV : a<p x1> | (VV >= a)}]<p>
-> {x3 : [{VV : a | (VV >= a)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}:forall a.
(GHC.Classes.Ord a) =>
x2:{VV : [a]<\x3 VV -> (x3 <= VV)> | ((len VV) >= 0)}
-> x3:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0) && ((len VV) >= (len x2)) && ((len VV) >= (len x3))}merge1 {x3 : [{VV : a | (a <= VV)}]<\x4 VV -> (x4 <= VV)> | (x3 == as') && ((len x3) >= 0)}as' ({VV : a | (VV == b)}bforall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a) && (VV >= b)}
-> x2:[{VV : a<p x1> | (VV >= a) && (VV >= b)}]<p>
-> {x3 : [{VV : a | (VV >= a) && (VV >= b)}]<p> | (((null x3)) <=> false) && ((len x3) == (1 + (len x2)))}:{x3 : [{VV : a | (VV >= b)}]<\x4 VV -> (VV >= x4)> | (x3 == bs') && ((len x3) >= 0)}bs')
94: merge1 [] bs            = {x2 : [a]<\x3 VV -> (VV >= x3)> | ((len x2) >= 0)}bs
95: merge1 as []            = {x2 : [a]<\x3 VV -> (x3 <= VV)> | ((len x2) >= 0)}as

100: data IL a = IN | IC a (IL a)