0
$\begingroup$

I need to prove:

reverse(push(as,bs)) = push(reverse(bs), reverse(as))

where:

def push[T](as: List[T], bs: List[T]): 
  List [T] = as match {
      case Nil => bs
      case x::xs => x::push(xs, bs)
  }

def reverse[T](ls: List[T]): 
  List[T] = ls match {
     case Nil => Nil
     case x::xs => push(reverse(xs), x::Nil)
  }

I am already stuck in the base case, since i cant figure out a lemma. The only thing I have this far is:

reverse(push(Nil,bs)) = reverse(bs)

and I'm stuck here since it felt eternity.

Does anyone have an idea for a lemma?

$\endgroup$
1
  • $\begingroup$ Have you tried proving push(xs, Nil) = xs? Have you tried proving the equality when as is a list of single item? $\endgroup$
    – John L.
    May 4, 2022 at 23:38

1 Answer 1

1
$\begingroup$

I think what would help a lot is proving first that push(push(a, b), c) = push(a, push(b, c)).

Once you have that result, you can make an induction on as only in the equality reverse(push(as,bs)) = push(reverse(bs), reverse(as)).

I will add some details if necessary.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.