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)
}
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?
append
I get infiniteappends
. Can you show me the first steps? $\endgroup$