Rev.agda

module Rev where

open import Data.List.Reverse
open import Relation.Binary.PropositionalEquality as PE
open import Relation.Binary.HeterogeneousEquality
open import Data.List
open import Data.Empty
open import Data.Product
open import Data.List.Properties

open ≡-Reasoning

lemma : ∀ {A : Set}{B : Set} xs {x : B} -> (xs ++ x ∷ [] ≡ []) -> A
lemma [] ()
lemma (x' ∷ xs') ()

reverse-[] : ∀ {A : Set} (xs : List A) -> xs ≡ [] ->  (y : Reverse xs) -> _≅_ {A = Reverse {A = A} []} [] y
reverse-[] .[] eq [] = refl
reverse-[] .(xs ++ x ∷ []) eq (xs ∶ rs ∶ʳ x) = lemma xs eq


reverse-∷ʳ : ∀ {A : Set} xs (x : A) ys -> ys ≡ xs ∷ʳ x -> (y : Reverse ys) -> ∃ λ rs -> xs ∶ rs ∶ʳ x ≅ y
reverse-∷ʳ xs x .[] eq [] = lemma xs (PE.sym eq)
reverse-∷ʳ xs x .(xs' ++ x' ∷ []) eq (xs' ∶ rs ∶ʳ x') with ∷ʳ-injective xs' xs eq
... | x'≡x , xs'≡xs rewrite x'≡x | xs'≡xs = rs , refl

unique : ∀ {A : Set} {xs : List A} (x y : Reverse xs) → x ≡ y
unique {_} {.[]} [] y = ≅-to-≡ (reverse-[] [] refl y)
unique (xs ∶ rsx ∶ʳ x) y = begin xs ∶ rsx ∶ʳ x ≡⟨ PE.cong (λ r -> xs ∶ r ∶ʳ x) (unique rsx rsy) ⟩
                                 xs ∶ rsy ∶ʳ x ≡⟨ ≅-to-≡ (proj₂ rec) ⟩
                                 y ∎
 where
  rec = reverse-∷ʳ xs x _ refl y
  rsy : Reverse xs
  rsy = proj₁ rec

reverseView-∷ʳ : ∀ {A : Set} xs (x : A) → reverseView (xs ∷ʳ x) ≡ xs ∶ reverseView xs ∶ʳ x
reverseView-∷ʳ xs x = unique _ _