ReverseReverse3 FIXED by Lost_dog_

module Theorem where

open import Definitions

open import Algebra
open import Data.List
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning
module LM {a} {A : Set a} = Monoid (monoid A)


myunfold-reverse : ∀ {a} {A : Set a} (x : A) (xs : List A) → myreverse (x ∷ xs) ≡ myreverse xs ∷ʳ x
myunfold-reverse x xs = begin
    myreverse (x ∷ xs)    ≡⟨ lem xs ([ x ]) ⟩
    rev xs [] ∷ʳ x
    ∎
  where
  lem : ∀ {a} {A : Set a} (xs ys : List A) → rev xs ys ≡ myreverse xs ++ ys
  lem [] ys = refl
  lem (x ∷ xs) ys
    rewrite lem xs (x ∷ ys)
          | myunfold-reverse x xs
          | LM.assoc (rev xs []) ([ x ]) ys
    = refl

lem : ∀ {a} {A : Set a} (x : A) (xs : List A) → myreverse (xs ∷ʳ x) ≡ x ∷ myreverse xs
lem x [] = refl
lem x (x' ∷ xs)
  rewrite myunfold-reverse x' (xs ∷ʳ x)
        | myunfold-reverse x' xs
        | lem x xs
  = refl

revrev : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs
revrev [] = refl
revrev (x ∷ xs)
  rewrite myunfold-reverse x xs
        | lem x xs
        | lem x (myreverse xs)
        | revrev xs
  = refl