Instantly share code, notes, and snippets.

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