Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
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
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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.