RevRev.agda

module RevRev  where

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

Rev : {A : Set} (_~_ : A -> A -> Set) (x y : A) -> Set
Rev _~_ y x = x ~ y

data All {A} (P : A -> Set) : List A -> Set where
  [] : All P []
  _::_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)

data Ordered {A} (_~_ : A -> A -> Set) : List A -> Set where
  [] : Ordered _~_ []
  _::_ : forall {y xs} -> All (\ x -> y ~ x) xs -> Ordered _~_ xs -> Ordered _~_ (y :: xs)

reverseAux : forall {A} -> List A -> List A -> List A
reverseAux xs [] = xs
reverseAux xs (y :: ys) = reverseAux (y :: xs) ys

reverse : forall {A} -> List A -> List A
reverse xs = reverseAux [] xs

allAllAux : forall {A} {_~_ : A -> A -> Set} -> (xs : List A) (y : A) (zs : List A) -> All (y ~_) zs -> All (\ z -> All (_~ z) xs) zs -> All (\ z -> All (_~ z) (y :: xs)) zs
allAllAux xs y [] y~[] xs~[] = []
allAllAux xs y (z :: zs) (y~z :: y~zs) (xs~z :: xs~zs) = (y~z :: xs~z) :: allAllAux xs y zs y~zs xs~zs

revRevAux : forall {A _~_} (xs zs : List A) -> Ordered (Rev _~_) xs -> Ordered _~_ zs -> All (\ z -> All (Rev _~_ z) xs) zs -> Ordered (Rev _~_) (reverseAux xs zs)
revRevAux xs [] P Q AllAll = P
revRevAux xs (y :: zs) P (Py :: Pzs) (Ally :: Allzs) = revRevAux (y :: xs) zs (Ally :: P) Pzs (allAllAux xs y zs Py Allzs)

all[]Aux : forall {A} {_~_ : A -> A -> Set} -> (xs : List A) -> All (\ x -> All (x ~_) []) xs
all[]Aux [] = []
all[]Aux (x :: xs) = [] :: all[]Aux xs

revRev : forall {A _~_} -> (xs : List A) -> Ordered _~_ xs -> Ordered (Rev _~_) (reverse xs)
revRev xs P = revRevAux [] xs [] P (all[]Aux xs)