MiniForall.scala

import stainless.annotation._
import stainless.collection._
import stainless.lang._
import stainless.lang.StaticChecks._
import stainless.proof._

object MiniForall {

  @induct
  def lemmaV1[T](xs: List[T], p1: T => Boolean, p2: T => Boolean): Boolean = {
    require(forall{ (z: T) => p1(z) ==> p2(z) })
    xs.forall(p1) ==> xs.forall(p2)
  }.holds

  def foo[T](xss: List[List[T]], length: BigInt): Unit = {
    require(length > 0 && xss.forall{ _.size == length && length > 0 })
    assert(lemmaV1[List[T]](xss, { _.size == length && length > 0 }, { _.size > 0 })) // fine!

    val p1 = { (xs: List[T]) => xs.size > 0 }
    val p2 = { (xs: List[T]) => xs.size > 0 && (xs.tail.size == xs.size - 1) }

    assert(xss.forall(p1)) // fine!
    assert(forall{ (xs: List[T]) => p1(xs) ==> p2(xs) }) // fine!
    // ADDING
    // assert(forall{ (xs: List[T]) => property(p1, p2, xs) }) 
    // FIX THE TIMEOUT
    assert(lemmaV1(xss, p1, p2)) // FIXME precond. call lemmaV1 times out
  }

  def property[T](p1: T => Boolean, p2: T => Boolean, x: T): Boolean = p1(x) ==> p2(x)

  //@induct // not powerfull enough, doing manual induction instead
  def lemmaV2[T](xs: List[T], p1: T => Boolean, p2: T => Boolean): Boolean = {
    require(forall{ (z: T) => property(p1, p2, z) /* equivalent to p1(z) ==> p2(z) }) */ })
    (xs.forall(p1) ==> xs.forall(p2)) because {
      xs match {
        case Nil() => trivial
        case Cons(h, t) => property(p1, p2, h) && lemmaV2(t, p1, p2)
      }
    }
  }.holds

  def bar[T](xss: List[List[T]], length: BigInt): Unit = {
    require(length > 0 && xss.forall{ _.size == length && length > 0 })
    assert(lemmaV2[List[T]](xss, { _.size == length && length > 0 }, { _.size > 0 })) // fine!

    val p1 = { (xs: List[T]) => xs.size > 0 }
    val p2 = { (xs: List[T]) => xs.size > 0 && (xs.tail.size == xs.size - 1) }

    //assert(xss.forall(p1)) // fine, not required.
    //assert(forall{ (xs: List[T]) => p1(xs) ==> p2(xs) }) // (1)
    assert(forall{ (xs: List[T]) => property(p1, p2, xs) }) // (2)
    // either (1) or (2) is required
    assert(lemmaV2(xss, p1, p2)) // fine!
  }

}