ReverseReverse2 by trigott

module Theorem where

open import Definitions

open import Data.List
open import Relation.Binary.PropositionalEquality

revs₁ : ∀ {a} {A : Set a} (x : A) (xs rest : List A) →
          foldl (λ rev x → x ∷ rev) (rest ++ x ∷ []) xs ≡
          foldl (λ rev x → x ∷ rev) rest xs ++ x ∷ []
revs₁ x [] rest = refl
revs₁ x (y ∷ xs) rest = revs₁ x xs (y ∷ rest)

revs₂ : ∀ {a} {A : Set a} (x : A) (xs rest : List A) →
       foldl (λ rev x → x ∷ rev) rest (xs ++ x ∷ []) ≡
       x ∷ foldl (λ rev x → x ∷ rev) rest xs
revs₂ x [] rest = refl
revs₂ x (y ∷ xs) rest = revs₂ x xs (y ∷ rest)

revrev : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs
revrev [] = refl
revrev (x ∷ xs) rewrite revs₁ x xs [] | revs₂ x (myreverse xs) [] = cong (_∷_ x) (revrev xs)