MapProver.scala

import leon.lang._
import leon.annotation._
import leon.collection._
import leon.proof._

object MapProover {
  def app[A, B](x: A)(f: A => B): B = f(x)

  def foo[A, B](xs: List[A])(f: A => B): Boolean = {
    // This verifies.
    // app(xs)(x => x) == app(xs)(x => x) &&
    // This too
    // id(xs) == id2(xs) &&
    // So does this.
    // xs.map(f) == xs.map(f) &&
    // This works too
    // xs.map(id) == xs.map(id) because mapId(xs) &&
    // This works as well
    // mapEquality(xs)(x => x) &&
    // But this doesn't.
    // xs.map(x => x) == xs.map(x => x) because mapEquality(xs)(x => x) &&
    // Nor this
    // xs.map(x => x) == xs.map(x => x) &&
    // Nor that
    xs.map(id) == xs.map(id2) &&
    // xs.map(id) == xs.map(id) &&
    true
  }.holds

  def id[A](x: A) = x
  def id2[A](x: A) = x

  @induct
  def mapId[A](xs: List[A]): Boolean = {
    xs.map(id) == xs because {
      xs match {
        case Nil() => true
        case Cons(x, xs) =>
          mapId(xs) &&
          id(x) :: xs.map(id) == x :: xs &&
          true
      }
    }
  }.holds

  def mapEquality1[A, B](xs: List[A])(f: A => B): Boolean = {
    xs.map(f) == xs.map(f)
  }.holds

  def mapEquality2[A, B](xs: List[A])(f: A => B): Boolean = {
    xs.map(id) == xs.map(id)
  }.holds

  def mapEquality3[A, B](xs: List[A]): Boolean = {
    xs.map(id) == xs.map(id) because mapId(xs)
  }.holds

  def mapEquality4[A, B](xs: List[A])(f: A => B): Boolean = {
    xs.map(id) == xs.map(id) because mapId(xs)
  }.holds

  // @induct
  // def mapEquality[A, B](xs: List[A])(f: A => B): Boolean = {
  //   // xs.map(f) == xs.map(f) &&
  //   xs.map(id) == xs.map(id) &&
  //    true because {
  //     xs match {
  //       case Nil() => true
  //       case Cons(y, ys) =>
  //         mapEquality(ys)(f) &&
  //         f(y) :: ys.map(f) == xs.map(f) &&
  //         true
  //     }
  //   } &&
  //   true
  // }.holds

}