Put mouse over identifiers to see inferred types
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: lq_tmp$x##176:[a] -> {lq_tmp$x##0 : GHC.Types.Int | lq_tmp$x##0 >= 0
&& lq_tmp$x##0 == Reverse.length lq_tmp$x##176}length [] = 0
13: length (_:xs) = {lq_tmp$x##244 : GHC.Types.Int | lq_tmp$x##244 == (1 : int)}1 lq_tmp$x##277:GHC.Types.Int -> lq_tmp$x##278:GHC.Types.Int -> {lq_tmp$x##280 : GHC.Types.Int^"lq_tmp$x##279" | lq_tmp$x##280 == lq_tmp$x##277 + lq_tmp$x##278}+ {lq_tmp$x##0 : GHC.Types.Int | lq_tmp$x##0 >= 0
&& lq_tmp$x##0 == Reverse.length xs##aS1
&& lq_tmp$x##0 == Reverse.length xs##aS1}length xs
14:
15: {-@ infix : @-}
16: {-@ reflect reverse @-}
17: {-@ reverse :: is:[a] -> {os:[a] | length is == length os} @-}
18: reverse :: [a] -> [a]
19: lq_tmp$x##457:[a] -> {os : [a] | Reverse.length lq_tmp$x##457 == Reverse.length os}reverse [] = []
20: reverse (x:xs) = {os : [{lq_tmp$x##550 : a^"lq_tmp$x##549" | $k_##548[lq_tmp$x##457:=xs##aTw][VV##547:=lq_tmp$x##550]}] | Reverse.length xs##aTw == Reverse.length os
&& os == Reverse.reverse xs##aTw}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: [] lq_tmp$x##298:[a] -> lq_tmp$x##299:[a] -> {os : [a] | Reverse.length os == Reverse.length lq_tmp$x##298 + Reverse.length lq_tmp$x##299}++ [a]ys = ys
27: (x:xs) ++ ys = x:({os : [{lq_tmp$x##393 : a^"lq_tmp$x##392" | $k_##391[lq_tmp$x##299:=ys##aTx][lq_tmp$x##298:=xs##aTz][VV##390:=lq_tmp$x##393]}] | Reverse.length os == Reverse.length xs##aTz + Reverse.length ys##aTx
&& os == Reverse.++ xs##aTz ys##aTx}xs ++ ys)
28:
29:
30: singletonP :: a -> Proof
31: {-@ singletonP :: x:a -> { reverse [x] == [x] } @-}
32: lq_tmp$x##645:a -> {VV : () | Reverse.reverse (GHC.Types.: lq_tmp$x##645 GHC.Types.[]) == GHC.Types.: lq_tmp$x##645 GHC.Types.[]}singletonP ax
33: = {lq_tmp$x##701 : [{lq_tmp$x##710 : a^"lq_tmp$x##709" | $k_##708[VV##707:=lq_tmp$x##710][lq_tmp$x##704:=lq_anf$##7205759403792797828##d16c]}] | Reverse.length lq_anf$##7205759403792797828##d16c == Reverse.length lq_tmp$x##701
&& lq_tmp$x##701 == Reverse.reverse lq_anf$##7205759403792797828##d16c
&& lq_tmp$x##701 == (if is$GHC.Types.[] lq_anf$##7205759403792797828##d16c then GHC.Types.[] else Reverse.++ (Reverse.reverse (lqdc##$select##GHC.Types.:##2 lq_anf$##7205759403792797828##d16c)) (GHC.Types.: (lqdc##$select##GHC.Types.:##1 lq_anf$##7205759403792797828##d16c) GHC.Types.[]))
&& lq_tmp$x##701 == Reverse.reverse lq_anf$##7205759403792797828##d16c}reverse [x]
34: ==. {lq_tmp$x##739 : [{lq_tmp$x##748 : a^"lq_tmp$x##747" | $k_##746[lq_tmp$x##742:=lq_anf$##7205759403792797830##d16e][VV##745:=lq_tmp$x##748]}] | Reverse.length lq_anf$##7205759403792797830##d16e == Reverse.length lq_tmp$x##739
&& lq_tmp$x##739 == Reverse.reverse lq_anf$##7205759403792797830##d16e
&& lq_tmp$x##739 == (if is$GHC.Types.[] lq_anf$##7205759403792797830##d16e then GHC.Types.[] else Reverse.++ (Reverse.reverse (lqdc##$select##GHC.Types.:##2 lq_anf$##7205759403792797830##d16e)) (GHC.Types.: (lqdc##$select##GHC.Types.:##1 lq_anf$##7205759403792797830##d16e) GHC.Types.[]))
&& lq_tmp$x##739 == Reverse.reverse lq_anf$##7205759403792797830##d16e}reverse [] ++ [x]
35: ==. {lq_tmp$x##943 : [{lq_tmp$x##956 : a^"lq_tmp$x##955" | $k_##954[lq_tmp$x##949:=lq_anf$##7205759403792797838##d16m][lq_tmp$x##948:=lq_anf$##7205759403792797836##d16k][VV##953:=lq_tmp$x##956]}] | Reverse.length lq_tmp$x##943 == Reverse.length lq_anf$##7205759403792797836##d16k + Reverse.length lq_anf$##7205759403792797838##d16m
&& lq_tmp$x##943 == Reverse.++ lq_anf$##7205759403792797836##d16k lq_anf$##7205759403792797838##d16m
&& lq_tmp$x##943 == (if is$GHC.Types.[] lq_anf$##7205759403792797836##d16k then lq_anf$##7205759403792797838##d16m else GHC.Types.: (lqdc##$select##GHC.Types.:##1 lq_anf$##7205759403792797836##d16k) (Reverse.++ (lqdc##$select##GHC.Types.:##2 lq_anf$##7205759403792797836##d16k) lq_anf$##7205759403792797838##d16m))
&& lq_tmp$x##943 == Reverse.++ lq_anf$##7205759403792797836##d16k lq_anf$##7205759403792797838##d16m}[] ++ [x]
36: ==. [x]
37: *** QED