proofs of list reverse properties in Idris

rev.idr

module Rev

rev : List a -> List a
rev [] = []
rev (x::xs) = rev xs ++ [x]

revUnit : rev [a] = [a]
revUnit = Refl


revApp : (xs, ys : List a) -> rev (xs ++ ys) = rev ys ++ rev xs
revApp = ?proof_revApp

proof_revApp = proof
  intros
  induction xs
  compute
  rewrite (appendNilRightNeutral (rev ys))
  trivial
  intros
  compute
  rewrite ihl__0
  rewrite sym ihl__0
  rewrite (appendAssociative (rev ys) (rev l__0) [t__0])
  trivial


revApp' : (xs, ys : List a) -> rev (xs ++ ys) = rev ys ++ rev xs
revApp' [] ys = ?proof_revAppNil
revApp' (x::xs) ys = let iH = revApp' xs ys in ?proof_revAppInd

proof_revAppNil = proof
  intros
  rewrite (appendNilRightNeutral (rev ys))
  trivial

proof_revAppInd = proof
  intros
  rewrite sym iH
  rewrite (appendAssociative (rev ys) (rev xs) [x])
  trivial