# Structural induction proof

I need to prove the following:

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


Where:

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


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?

• In the same way – you use the definitions and everything works out. Mar 7, 2018 at 17:16
• @YuvalFilmus Can you elaborate? I can't see how to do it!
– user85395
Mar 7, 2018 at 17:19
• 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. Mar 7, 2018 at 17:21
• @YuvalFilmus If I start with the inner append I get infinite appends. Can you show me the first steps?
– user85395
Mar 7, 2018 at 17:31
• @YuvalFilmus I can't see how to proceed after I get: $reverse(Cons(y,append(ys,z)))$.
– user85395
Mar 7, 2018 at 17:40