Skip to content

Instantly share code, notes, and snippets.

@copumpkin
Last active August 29, 2015 13:55
Show Gist options
  • Save copumpkin/8758586 to your computer and use it in GitHub Desktop.
Save copumpkin/8758586 to your computer and use it in GitHub Desktop.
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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment