Instantly share code, notes, and snippets.

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

 -- 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
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.