Idris version of https://gist.github.com/copumpkin/8758586

ReverseLike.idr

-- Idris translation of copumpkin's Agda code:
-- https://gist.github.com/copumpkin/8758586

-- Proves that List reverse is completely specified by:
-- 1. f [] = []
-- 2. f [x] = [x]
-- 3. f (xs ++ ys) = f ys ++ f xs

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} ->
       (reverse0 : reverse [] = []) ->
       (reverse1 : (x : a) -> reverse [x] = [x]) ->
       (reverseFlip : (xs, ys : List a) -> reverse (xs ++ ys) = reverse ys ++ reverse xs) ->
       ReverseLike reverse

reverse'Proof : (f : List a -> List a) -> ReverseLike f -> (xs : List a) -> f xs = reverse' xs
reverse'Proof f (RL reverse0 reverse1 reverseFlip) [] = reverse0
reverse'Proof f (RL reverse0 reverse1 reverseFlip) (x :: xs) =
  let inductiveHypothesis = reverse'Proof f (RL reverse0 reverse1 reverseFlip) xs
  in ?reverse'ProofStepCase

---------- Proofs ----------

reverse'ProofStepCase = proof
  intros
  rewrite sym (reverseFlip [x] xs)
  rewrite sym (reverse1 x)
  rewrite inductiveHypothesis
  trivial