Reverse.agda

module Reverse where

open import Data.List as List hiding (reverse)
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality

record ReverseLike (reverse : ∀ {A : Set} → List A → List A) : Set₁ where
  constructor rl
  field
    reverse0 : ∀ {A} → reverse {A} [] ≡ []
    reverse1 : ∀ {A} (x : A) → reverse (x ∷ []) ≡ x ∷ []
    reverse-flip : ∀ {A} (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs


proof : (f : ∀ {A : Set} → List A → List A) → ReverseLike f → {A : Set} (xs : List A) → f xs ≡ List.reverse xs
proof f (rl r0 r1 rf) [] = r0
proof f (rl r0 r1 rf) (x ∷ xs) = trans (rf (x ∷ []) xs) (trans (cong₂ _++_ (proof f (rl r0 r1 rf) xs) (r1 x)) (sym (reverse-++-commute (x ∷ []) xs)))