I need to prove the following:

reverse(append(zs, z)) = Cons(z, reverse(zs))


sealed abstract class IntList
case object Nil extends IntList
case class Cons(x: Int, xs: IntList) extends IntList

def append(xs: IntList, x: Int): IntList = xs match {
    case Nil => Cons(x, Nil)
    case Cons(y, ys) => Cons(y, append(ys, x))

def reverse(xs: IntList): IntList = xs match {
    case Nil => Nil
    case Cons(x, ys) => append(reverse(ys), x)

I've already made the induction basis:

Assume $zs=Nil$. \begin{align*} reverse(append(zs, z)) &=reverse(append(Nil,z)) \\ &=reverse(Cons(z,Nil)) \\ &=append(reverse(Cons(Nil),z)) \\ &=Cons(z,reverse(Nil)) \end{align*}

How do I make the induction step?

  • $\begingroup$ In the same way – you use the definitions and everything works out. $\endgroup$ Mar 7, 2018 at 17:16
  • $\begingroup$ @YuvalFilmus Can you elaborate? I can't see how to do it! $\endgroup$
    – user85395
    Mar 7, 2018 at 17:19
  • $\begingroup$ Take $zs=Cons(w,ws)$, use the definitions of $append$ and $reverse$, and at some point you will need to use the inductive hypothesis as well. $\endgroup$ Mar 7, 2018 at 17:21
  • $\begingroup$ @YuvalFilmus If I start with the inner append I get infinite appends. Can you show me the first steps? $\endgroup$
    – user85395
    Mar 7, 2018 at 17:31
  • $\begingroup$ @YuvalFilmus I can't see how to proceed after I get: $reverse(Cons(y,append(ys,z)))$. $\endgroup$
    – user85395
    Mar 7, 2018 at 17:40

1 Answer 1


Here is the complete proof:

reverse(append(Cons(w,ws),z)) = reverse(Cons(w,append(ws,z))) = append(reverse(append(ws,z)),w) = append(Cons(z,reverse(ws)),w) = Cons(z,append(reverse(ws),w)) = Cons(z,reverse(Cons(w,ws)))

At one point we used the inductive hypothesis.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.