module reverse where

open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

data List {i} (A : Set i) : Set i where
  [] : List A
  _∷_ : A → List A → List A
infixr 6 _∷_

_++_ : ∀ {i}{A : Set i} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
infixl 5 _++_

++-right-unit : ∀ {i}{A : Set i}
              → (xs : List A)
              → xs ++ [] ≡ xs
++-right-unit [] = refl
++-right-unit (x ∷ xs) = cong (_∷_ x) (++-right-unit xs)

++-assoc : ∀ {i}{A : Set i}
         → (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)

reverse : ∀ {i}{A : Set i} → List A → List A
reverse [] = []
reverse (x ∷ xs) = reverse xs ++ x ∷ []

reverse-hom : ∀ {i}{A : Set i}
            → (xs ys : List A)
            → reverse (xs ++ ys)
            ≡ reverse ys ++ reverse xs
reverse-hom [] ys = sym (++-right-unit (reverse ys))
reverse-hom (x ∷ xs) ys = begin
    reverse ((x ∷ xs) ++ ys)
  ≡⟨ cong (λ α → α ++ x ∷ []) (reverse-hom xs ys) ⟩
    reverse ys ++ reverse xs ++ x ∷ []
  ≡⟨ ++-assoc (reverse ys) (reverse xs) (x ∷ []) ⟩
    reverse ys ++ reverse (x ∷ xs)
  ∎

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