Skip to content

Instantly share code, notes, and snippets.

@puffnfresh puffnfresh/ReverseLike.idr
Last active Aug 29, 2015

Embed
What would you like to do?
-- Originally an Idris translation of copumpkin's Agda code:
-- https://gist.github.com/copumpkin/8758586
-- Extended using Matthew Brecknell's proof which only needs two properties:
-- https://gist.github.com/mbrcknl/bfaa72c2ec6ff32a2826
-- Proves that List reverse is completely specified by:
-- 1. f [x] = [x]
-- 2. f (xs ++ ys) = f ys ++ f xs
%default total
reverse' : List a -> List a
reverse' [] = []
reverse' (x :: xs) = reverse' xs ++ [x]
record ReverseLike : (List a -> List a) -> Type where
RL : {reverse : List a -> List a} ->
(reverse1 : (x : a) -> reverse [x] = [x]) ->
(reverseFlip : (xs, ys : List a) -> reverse (xs ++ ys) = reverse ys ++ reverse xs) ->
ReverseLike reverse
consElim : (x : a) -> (xs, ys : List a) -> x :: xs = x :: ys -> xs = ys
consElim x [] [] prf = Refl
consElim x [] (y :: xs) Refl impossible
consElim x (x :: xs) [] Refl impossible
consElim x (x :: xs) (x :: xs) Refl = Refl
appEqNil : (xs, ys : List a) -> xs ++ ys = xs -> ys = []
appEqNil [] ys prf = prf
appEqNil (x :: xs) [] prf = Refl
appEqNil (x :: xs) (y :: ys) prf =
appEqNil xs (y :: ys) (consElim x (xs ++ y :: ys) xs prf)
reverse'Proof : (f : List a -> List a) -> ReverseLike f -> (xs : List a) -> f xs = reverse' xs
reverse'Proof f (RL reverse1 reverseFlip) [] = ?reverse'ProofNilCase
reverse'Proof f (RL reverse1 reverseFlip) (x :: xs) =
let inductiveHypothesis = reverse'Proof f (RL reverse1 reverseFlip) xs
in ?reverse'ProofStepCase
---------- Proofs ----------
reverse'ProofNilCase = proof
intros
rewrite appEqNil (f []) (f []) (sym (reverseFlip [] []))
trivial
reverse'ProofStepCase = proof
intros
rewrite sym (reverseFlip [x] xs)
rewrite sym (reverse1 x)
rewrite inductiveHypothesis
trivial
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.