1: GHC.Types.Module{-@ LIQUID "--exactdc" @-}
 2: {-@ LIQUID "--higherorder" @-}
 3: 
 4: module Reverse where 
 5: 
 6: import LiquidHaskell.ProofCombinators 
 7: import Prelude hiding (reverse, (++), length)
 8: 
 9: {-@ measure length @-}
10: {-@ length :: [a] -> Nat @-} 
11: length :: [a] -> Int 
12: x1:[a] -> {v : GHC.Types.Int | v >= 0
                               && v == Reverse.length x1}length []     = 0 
13: length (_:xs) = {v : GHC.Types.Int | v == (1 : int)}1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : GHC.Types.Int | v >= 0
                     && v == Reverse.length xs}length xs
14: 
15: {-@ infix   : @-}
16: {-@ reflect reverse @-}
17: {-@ reverse :: is:[a] -> {os:[a] | length is == length os} @-}
18: reverse :: [a] -> [a]
19: x1:[a] -> {os : [a] | Reverse.length x1 == Reverse.length os}reverse []     = []
20: reverse (x:xs) = {os : [a] | Reverse.length xs == Reverse.length os
            && os == Reverse.reverse xs}reverse xs ++ [x]
21: 
22: {-@ infix   ++ @-}
23: {-@ reflect ++ @-}
24: {-@ (++) :: xs:[a] -> ys:[a] -> {os:[a] | length os == length xs + length ys} @-}
25: (++) :: [a] -> [a] -> [a]
26: []     x1:[a] -> x2:[a] -> {os : [a] | Reverse.length os == Reverse.length x1 + Reverse.length x2}++ [a]ys = ys
27: (x:xs) ++ ys = x:({os : [a] | Reverse.length os == Reverse.length xs + Reverse.length ys
            && os == Reverse.++ xs ys}xs ++ ys)
28: 
29: 
30: singletonP :: a -> Proof
31: {-@ singletonP :: x:a -> { reverse [x] == [x] } @-}
32: x1:a -> {VV : () | Reverse.reverse (GHC.Types.: x1 GHC.Types.[]) == GHC.Types.: x1 GHC.Types.[]}singletonP ax
33:   =   [a]reverse [x]
34:   ==. [a]reverse [] ++ [x]
35:   ==. [a][] ++ [x]
36:   ==. [x]
37:   *** QED