0 | module Data.List.Palindrome
 1 |
 2 | import Data.List
 3 | import Data.List.Views.Extra
 4 | import Data.List.Reverse
 5 | import Data.List.Equalities
 6 |
 7 | %hide Prelude.reverse
 8 | %default total
 9 |
10 | ||| Do geese see God?
11 | public export
12 | data Palindrome : (xs : List a) -> Type where
13 |   Empty  : Palindrome []
14 |   Single : Palindrome [_]
15 |   Multi  : Palindrome xs -> Palindrome (x :: (xs `snoc` x))
16 |
17 | ||| A Palindrome reversed is itself.
18 | export
19 | palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs
20 | palindromeReverse [] Empty = Refl
21 | palindromeReverse [_] Single = Refl
22 | palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =
23 |   rewrite sym $ revAppend ([x] ++ ys) [x] in
24 |     rewrite sym $ revAppend [x] ys in
25 |       rewrite palindromeReverse ys pf in
26 |         Refl
27 |
28 | private
29 | reversePalindromeEqualsLemma
30 |   : (x, x' : a)
31 |   -> (xs : List a)
32 |   -> reverse (x :: (xs ++ [x'])) = (x :: (xs ++ [x']))
33 |   -> (reverse xs = xs, x = x')
34 | reversePalindromeEqualsLemma x x' xs prf = equateInnerAndOuter flipHeadX
35 |   where
36 |     flipHeadX : reverse (xs ++ [x']) ++ [x] = x :: (xs ++ [x'])
37 |     flipHeadX = rewrite (sym (reverseCons x (xs ++ [x']))) in prf
38 |     flipLastX' : reverse (xs ++ [x']) = x :: xs -> (x' :: reverse xs) = (x :: xs)
39 |     flipLastX' prf = rewrite (revAppend xs [x']) in prf
40 |     cancelOuter : (reverse (xs ++ [x'])) = x :: xs -> reverse xs = xs
41 |     cancelOuter prf = snd (biinjective (flipLastX' prf))
42 |     equateInnerAndOuter
43 |       : reverse (xs ++ [x']) ++ [x] = (x :: xs) ++ [x']
44 |       -> (reverse xs = xs, x = x')
45 |     equateInnerAndOuter prf =
46 |       let (prf', xEqualsX') = snocInjective prf
47 |        in (cancelOuter prf', xEqualsX')
48 |
49 | ||| Only Palindromes are equal to their own reverse.
50 | export
51 | reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs
52 | reversePalindrome input prf with (vList input)
53 |   reversePalindrome [] _ | VNil = Empty
54 |   reversePalindrome [x] _ | VOne = Single
55 |   reversePalindrome (x :: (inner `snoc` y)) prf | VCons rec with (reversePalindromeEqualsLemma x y inner prf)
56 |     reversePalindrome (x :: (inner `snoc` y)) prf | VCons rec | (revInnerIsIdentical, xIsY) =
57 |       rewrite xIsY in
58 |         Multi $ reversePalindrome inner revInnerIsIdentical | Force rec
59 |