ReverseReverse1 by trigott

module Theorem where

open import Definitions

open import Data.List
open import Relation.Binary.PropositionalEquality as P hiding ([_])
open P.≡-Reasoning

revsnoc : ∀ {a} {A : Set a} → (x : A) → (xs : List A)
          → myreverse (xs ++ [ x ]) ≡ x ∷ myreverse xs
revsnoc x [] = refl
revsnoc x (a ∷ rest) = begin
  myreverse (a ∷ rest ++ [ x ]) ≡⟨ refl ⟩
  myreverse (rest ++ [ x ]) ++ [ a ] ≡⟨ cong (\l → l ++ [ a ]) (revsnoc x rest) ⟩
  (x ∷ myreverse rest) ++ [ a ] ≡⟨ refl ⟩
  x ∷ (myreverse rest ++ [ a ]) ≡⟨ refl ⟩
  x ∷ myreverse (a ∷ rest)
  ∎
  
revrev : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs
revrev [] = refl
revrev (a ∷ rest) = begin
  myreverse (myreverse (a ∷ rest)) ≡⟨ refl ⟩
  myreverse (myreverse rest ++ [ a ]) ≡⟨ revsnoc a (myreverse rest) ⟩
  a ∷ myreverse (myreverse rest) ≡⟨ cong (\l → a ∷ l) (revrev rest) ⟩
  a ∷ rest
  ∎