1
$\begingroup$

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?

$\endgroup$
5
  • $\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

1
$\begingroup$

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.

$\endgroup$

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.