Palindrome.agda

open import Data.Char
open import Data.List
open import Function using (flip; _$_)
open import Relation.Nullary.Core
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality renaming ([_] to [_]ev)
open ≡-Reasoning

data Pal : List Char → Set where
    nil  :                                        Pal []
    sing :                   (c : Char)         → Pal [ c ]
    cons : (s : List Char) → (c : Char) → Pal s → Pal ([ c ] ++ s ++ [ c ])

-- examples
o : Pal [ 'o' ]
o = sing 'o'

lol : Pal ('l' ∷ 'o' ∷ 'l' ∷ [])
lol = cons ('o' ∷ []) 'l' (sing 'o')

*lol* : Pal ('*' ∷ 'l' ∷ 'o' ∷ 'l' ∷ '*' ∷ [])
*lol* = cons ('l' ∷ 'o' ∷ 'l' ∷ []) '*'
            (cons ('o' ∷ []) 'l' (sing 'o'))

-- lemmata
++-right-identity : ∀ {a} → {A : Set a} → (s : List A) → s ++ [] ≡ s
++-right-identity []       = refl
++-right-identity (x ∷ xs) = cong (_∷_ x) (++-right-identity xs)

++-assoc : ∀ {a} → {A : Set a}
          → (xs ys zs : List A)
          → xs ++ ys ++ zs ≡ (xs ++ ys) ++ zs
++-assoc []       ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)

unfold-reverse : ∀ {a} {A : Set a}
                 → (xs ys : List A)
                 → foldl (flip _∷_) xs ys ≡ reverse ys ++ xs
unfold-reverse xs []       = refl
unfold-reverse xs (y ∷ ys) =
    begin
        foldl (flip _∷_) (y ∷ xs) ys
    ≡⟨ unfold-reverse (y ∷ xs) ys ⟩
        reverse ys ++ [ y ] ++ xs
    ≡⟨ ++-assoc (reverse ys) [ y ] xs ⟩
        (reverse ys ++ [ y ]) ++ xs
    ≡⟨ cong (λ w → w ++ xs) (sym (unfold-reverse [ y ] ys)) ⟩
        foldl (flip _∷_) [ y ] ys ++ xs
    ∎

reverse-∷ : ∀ {a} → {A : Set a}
            → (x : A)
            → (xs : List A)
            → reverse (x ∷ xs) ≡ reverse xs ++ [ x ]
reverse-∷ x xs = unfold-reverse [ x ] xs

reverse-++ : ∀ {a} → {A : Set a}
             → (xs ys : List A)
             → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ []       ys = sym (++-right-identity (reverse ys))
reverse-++ (x ∷ xs) ys =
    begin
        reverse (x ∷ xs ++ ys)
    ≡⟨ reverse-∷ x (xs ++ ys) ⟩
        reverse (xs ++ ys) ++ [ x ]
    ≡⟨ cong (flip _++_ [ x ]) (reverse-++ xs ys) ⟩
        (reverse ys ++ reverse xs) ++ [ x ]
    ≡⟨ sym (++-assoc (reverse ys) (reverse xs) [ x ]) ⟩
        reverse ys ++ reverse xs ++ [ x ]
    ≡⟨ cong (_++_ (reverse ys)) (sym (reverse-∷ x xs)) ⟩
        reverse ys ++ reverse (x ∷ xs)
    ∎

reverse-twice : ∀ {a} → {A : Set a}
                → (xs : List A)
                → reverse (reverse xs) ≡ xs
reverse-twice [] = refl
reverse-twice (x ∷ xs) =
    begin
        reverse (reverse (x ∷ xs))
    ≡⟨ cong reverse (reverse-∷ x xs) ⟩
        reverse (reverse xs ++ [ x ])
    ≡⟨ reverse-++ (reverse xs) [ x ] ⟩
        reverse [ x ] ++ reverse (reverse xs)
    ≡⟨ cong (_++_ (reverse [ x ])) (reverse-twice xs) ⟩
        reverse [ x ] ++ xs
    ≡⟨ refl ⟩
        x ∷ xs
    ∎

∷-right-cancellative : ∀ {a} → {A : Set a}
                       → (z : A)
                       → (xs ys : List A)
                       → z ∷ xs ≡ z ∷ ys
                       → xs ≡ ys
∷-right-cancellative z [] .[] refl = refl
∷-right-cancellative z (x ∷ xs) .(x ∷ xs) refl = refl

++-left-cancellative : ∀ {a} → {A : Set a}
                        → (xs ys zs : List A)
                        → zs ++ xs ≡ zs ++ ys
                        → xs ≡ ys
++-left-cancellative xs ys [] rel = rel
++-left-cancellative xs ys (z ∷ zs) rel =
    ++-left-cancellative xs ys zs
        (∷-right-cancellative z (zs ++ xs) (zs ++ ys) rel)
--
-- reverse-[] : ∀ {a} → {A : Set a}
--              → (xs : List A)
--              → reverse xs ≡ []
--              → xs ≡ []
-- reverse-[] []       rel = refl
-- reverse-[] (x ∷ xs) rel with reverse (x ∷ xs) | inspect reverse (x ∷ xs)
-- reverse-[] (x ∷ xs) refl | [] | [ eq ]ev =
--     begin
--         x ∷ xs
--     ≡⟨ sym (reverse-twice (x ∷ xs)) ⟩
--         reverse (reverse (x ∷ xs))
--     ≡⟨ cong reverse (reverse-∷ x xs) ⟩
--         reverse (reverse xs ++ [ x ])
--     ≡⟨ cong reverse (sym (unfold-reverse [ x ] xs)) ⟩
--         reverse (foldl (flip _∷_) [ x ] xs)
--     ≡⟨ cong reverse eq ⟩
--         []
--     ∎
-- reverse-[] (x ∷ xs) rel | z ∷ zs | [ eq ]ev =
--     begin
--         x ∷ xs
--     ≡⟨ sym (reverse-twice (x ∷ xs)) ⟩
--         reverse (reverse (x ∷ xs))
--     ≡⟨ cong reverse (reverse-∷ x xs) ⟩
--         reverse (reverse xs ++ [ x ])
--     ≡⟨ cong reverse (sym (unfold-reverse [ x ] xs)) ⟩
--         reverse (foldl (flip _∷_) [ x ] xs)
--     ≡⟨ cong reverse eq ⟩
--         reverse (z ∷ zs)
--     ≡⟨ cong reverse rel ⟩
--         []
--     ∎

reverse-injective : ∀ {a} → {A : Set a}
                    → (xs ys : List A)
                    → reverse xs ≡ reverse ys
                    → xs ≡ ys
reverse-injective xs ys rel =
    begin
        xs
    ≡⟨ sym (reverse-twice xs) ⟩
        reverse (reverse xs)
    ≡⟨ cong reverse rel ⟩
        reverse (reverse ys)
    ≡⟨ reverse-twice ys ⟩
        ys
    ∎

++-right-cancellative : ∀ {a} → {A : Set a}
                        → (xs ys zs : List A)
                        → xs ++ zs ≡ ys ++ zs
                        → xs ≡ ys
++-right-cancellative xs ys [] rel =
    begin
        xs
    ≡⟨ sym (++-right-identity xs) ⟩
        xs ++ []
    ≡⟨ rel ⟩
        ys ++ []
    ≡⟨ ++-right-identity ys ⟩
        ys
    ∎
++-right-cancellative xs ys (z ∷ zs) rel = reverse-injective xs ys $
    ∷-right-cancellative z (reverse xs) (reverse ys) $
        begin
            [ z ] ++ reverse xs
        ≡⟨ sym (reverse-++ xs (z ∷ [])) ⟩
            reverse (xs ++ [ z ])
        ≡⟨ cong reverse (++-right-cancellative (xs ++ [ z ]) (ys ++ [ z ]) zs (
            begin
                (xs ++ [ z ]) ++ zs
            ≡⟨ sym (++-assoc xs [ z ] zs) ⟩
                xs ++ z ∷ zs
            ≡⟨ rel ⟩
                ys ++ z ∷ zs
            ≡⟨ ++-assoc ys [ z ] zs ⟩
                (ys ++ [ z ]) ++ zs
            ∎)) ⟩
            reverse (ys ++ [ z ])
        ≡⟨ reverse-++ ys [ z ] ⟩
            [ z ] ++ reverse ys
        ∎


prop : ∀ {xs} → Pal xs → reverse xs ≡ xs
prop nil          = refl
prop (sing c)     = refl
prop (cons s c P) =
    begin
        reverse (c ∷ s ++ [ c ])
    ≡⟨ reverse-++ (c ∷ s) [ c ] ⟩
        c ∷ reverse (c ∷ s)
    ≡⟨ cong (_∷_ c) (reverse-∷ c s) ⟩
        c ∷ reverse s ++ [ c ]
    ≡⟨ cong (λ x → (c ∷ x) ++ [ c ]) (prop P) ⟩
        c ∷ s ++ [ c ]
    ∎