Idris version of https://gist.github.com/mbrcknl/bfaa72c2ec6ff32a2826

ReverseLike.idr

-- 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