Testcases for higher-order functions

testcases/verification/higher-order/invalid/Continuations1.scala

+import leon.lang._
+
+object Continuations1 {
+  def add_cps[T](x: BigInt, y: BigInt)(f: BigInt => T): T = {
+    f(x + y)
+  }
+
+  def square_cps[T](x: BigInt)(f: BigInt => T): T = {
+    f(x * x)
+  }
+
+  def pythagoras_cps[T](a: BigInt, b: BigInt)(f: BigInt => T): T = {
+    val a2 = square_cps(a)(x => x)
+    val b2 = square_cps(b)(x => x)
+    add_cps(a2, b2)(f)
+  }
+
+  def lemma1(a: BigInt, b: BigInt): Boolean = {
+    require(a > 0 && b > 0)
+    pythagoras_cps(a, b)(_ == a*a + b*b)
+  }.holds
+
+  def lemma2(a: BigInt, b: BigInt): Boolean = {
+    require(a > 0 && b > 0)
+    pythagoras_cps(a, b)(_ == a*a)
+  }.holds
+}

testcases/verification/higher-order/invalid/HOInvocations.scala

+import leon.lang._
+
+object HOInvocations {
+  def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g
+
+  def failling_1(f: (Int) => Int) = {
+    switch(-10, (x: Int) => x + 1, f)(2)
+  } ensuring { res => res > 0 }
+
+  def failling_2(x: Int, f: (Int) => Int, g: (Int) => Int) = {
+    require(x > 0)
+    switch(1, switch(x, f, g), g)(1)
+  } ensuring { res => res != f(1) }
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/invalid/Lists1.scala

+import leon.lang._
+
+object Lists1 {
+  abstract class List[T]
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+    case Cons(head, tail) => f(head) && forall(tail, f)
+    case Nil() => true
+  }
+
+  def positive(list: List[Int]): Boolean = list match {
+    case Cons(head, tail) => if (head < 0) false else positive(tail)
+    case Nil() => true
+  }
+
+  def gt(i: Int): Int => Boolean = x => x > i
+
+  def positive_lemma(list: List[Int]): Boolean = {
+    positive(list) == forall(list, gt(0))
+  }
+
+  def failling_1(list: List[Int]): Boolean = {
+    list match {
+      case Nil() => positive_lemma(list)
+      case Cons(head, tail) => positive_lemma(list) && failling_1(tail)
+    }
+  }.holds
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/invalid/Map.scala

+import leon.lang._
+import leon.collection._
+
+object Map {
+  
+  def failure1[T](l: List[T], f: T => T): Boolean = {
+    l.map(f) == l.map(f).map(f)
+  }.holds
+
+  def failure2[T](l: List[T], f: T => T): Boolean = {
+    l.map(f) == (l match {
+      case Cons(head, tail) => Cons(head, tail.map(f))
+      case Nil() => Nil[T]()
+    })
+  }.holds
+
+  def failure3[T](l: List[T], f: T => List[T]): Boolean = {
+    l == l.flatMap(f)
+  }.holds
+}

testcases/verification/higher-order/invalid/ParBalance.scala

+import leon._
+import leon.lang._
+
+object ParBalance {
+
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  sealed abstract class Option
+  case class Some(x: BigInt) extends Option
+  case class None() extends Option
+
+  val openPar : BigInt = BigInt(1)
+  val closePar : BigInt = BigInt(2)
+
+  def balanced(list: List, counter: BigInt): Boolean = {
+    if (counter < 0) false else list match {
+      case Cons(head, tail) =>
+        val c = if (head == openPar) counter + 1
+          else if (head == closePar) counter - 1
+          else counter
+        balanced(tail, c)
+      case Nil() => counter == 0
+    }
+  }
+
+  def balanced_nonEarly(list: List, counter: BigInt): Boolean = {
+    list match {
+      case Cons(head, tail) =>
+        if (counter < 0) balanced_nonEarly(tail, counter) else {
+          val c = if (head == openPar) counter + 1
+            else if (head == closePar) counter - 1
+            else counter
+          balanced_nonEarly(tail, c)
+        }
+      case Nil() => counter == 0
+    }
+  } ensuring { res => res == balanced(list, counter) }
+
+  def balanced_withFailure(list: List, counter: BigInt, failed: Boolean): Boolean = {
+    require(counter >= 0 || failed)
+    list match {
+      case Cons(head, tail) =>
+        val c = if (head == openPar) counter + 1
+          else if (head == closePar) counter - 1
+          else counter
+        balanced_withFailure(tail, c, failed || c < 0)
+      case Nil() => !failed && counter == 0
+    }
+  } ensuring { res =>
+    if (failed) {
+      res == balanced_nonEarly(list, -1)
+    } else {
+      res == balanced_nonEarly(list, counter)
+    }
+  }
+
+  def balanced_withReduce(list: List, p: (BigInt, BigInt)): Boolean = {
+    require(p._1 >= 0 && p._2 >= 0)
+    list match {
+      case Cons(head, tail) =>
+        val p2 = reduce(p, parPair(head))
+        balanced_withReduce(tail, p2)
+      case Nil() =>
+        p._1 == 0 && p._2 == 0
+    }
+  } ensuring { res => res == balanced_withFailure(list, p._1 - p._2, p._2 > 0) }
+
+  def balanced_foldLeft_equivalence(list: List, p: (BigInt, BigInt)): Boolean = {
+    require(p._1 >= 0 && p._2 >= 0)
+    val f = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+    (foldLeft(list, p, f) == (BigInt(0), BigInt(0))) == balanced_withReduce(list, p) && (list match {
+      case Cons(head, tail) =>
+        val p2 = f(p, head)
+        balanced_foldLeft_equivalence(tail, p2)
+      case Nil() => true
+    })
+  }.holds
+
+  def foldRight[A](list: List, state: A, f: (BigInt, A) => A): A = list match {
+    case Cons(head, tail) =>
+      val tailState = foldRight(tail, state, f)
+      f(head, tailState)
+    case Nil() => state
+  }
+
+  def foldLeft[A](list: List, state: A, f: (A, BigInt) => A): A = list match {
+    case Cons(head, tail) =>
+      val nextState = f(state, head)
+      foldLeft(tail, nextState, f)
+    case Nil() => state
+  }
+
+  def reduce(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): (BigInt, BigInt) = {
+    if (p1._1 >= p2._2) {
+      (p1._1 - p2._2 + p2._1, p1._2)
+    } else {
+      (p2._1, p2._2 - p1._1 + p1._2)
+    }
+  }
+
+  def reduce_associative(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+    reduce(p1, reduce(p2, p3)) == reduce(reduce(p1, p2), p3)
+  }.holds
+
+  def swap(p: (BigInt, BigInt)): (BigInt, BigInt) = (p._2, p._1)
+
+  def reduce_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): Boolean = {
+    reduce(p1, p2) == swap(reduce(swap(p2), swap(p1)))
+  }.holds
+
+  def reduce_associative_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+    reduce(p1, reduce(p2, p3)) == swap(reduce(reduce(swap(p3), swap(p2)), swap(p1)))
+  }.holds
+
+  def reduce_associative_inverse2(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+    reduce(reduce(p1, p2), p3) == swap(reduce(swap(p3), reduce(swap(p2), swap(p1))))
+  }.holds
+
+  def parPair(x: BigInt): (BigInt, BigInt) = {
+    if (x == openPar) (1, 0) else if (x == closePar) (0, 1) else (0, 0)
+  }
+
+  def fold_equivalence(list: List): Boolean = {
+    val s = (BigInt(0), BigInt(0))
+    val fl = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+    val fr = (x: BigInt, s: (BigInt, BigInt)) => reduce(swap(parPair(x)), s)
+
+    foldLeft(list, s, fl) == swap(foldRight(list, swap(s), fr))
+  }.holds
+
+}

testcases/verification/higher-order/invalid/PositiveMap.scala

+import leon.lang._
+
+object PositiveMap {
+  
+  abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  def positive(list: List): Boolean = list match {
+    case Cons(head, tail) => if (head < 0) false else positive(tail)
+    case Nil() => true
+  }
+
+  def positiveMap_failling_1(f: (Int) => Int, list: List): List = {
+    list match {
+      case Cons(head, tail) =>
+        val fh = f(head)
+        val nh = if (fh < -1) 0 else fh
+        Cons(nh, positiveMap_failling_1(f, tail))
+      case Nil() => Nil()
+    }
+  } ensuring { res => positive(res) }
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/invalid/Sets1.scala

+import leon.lang._
+
+object Sets1 {
+  def set(i: Int): Int => Boolean = x => x == i
+
+  def complement(s: Int => Boolean): Int => Boolean = x => !s(x)
+
+  def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+  def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+  def failing(s1: Int => Boolean, s2: Int => Boolean): Boolean = {
+    complement(intersection(union(s1, s2), s1)) == s2
+  }.holds
+
+}

testcases/verification/higher-order/valid/Anonymous.scala

+import leon.lang._
+
+object Anonymous {
+  def test(x: BigInt) = {
+    require(x > 0)
+    val i = (a: BigInt) => a + 1
+    i(x) + i(2)
+  } ensuring { res => res > 0 }
+}

testcases/verification/higher-order/valid/Closures.scala

+import leon.lang._
+
+object Closures {
+  def addX(x: Int): Int => Int = {
+    (a: Int) => a + x
+  }
+
+  def test(x: Int): Boolean = {
+    val add1 = addX(1)
+    val add2 = addX(2)
+    add1(add2(1)) == 4
+  }.holds
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/valid/Closures2.scala

+import leon.lang._
+
+object Closures2 {
+  def set(i: Int): Int => Boolean = x => x == i
+
+  def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+  def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+  def diff(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && !s2(x)
+
+  def set123(): Int => Boolean = union(set(1), union(set(2), set(3)))
+
+  def test1(): Boolean = {
+    val s1 = set123()
+    val s2 = union(s1, set(4))
+    s2(1) && s2(2) && s2(3) && s2(4)
+  }.holds
+
+  def test2(): Boolean = {
+    val s1 = set123()
+    val s2 = intersection(s1, union(set(1), set(3)))
+    val s3 = diff(s1, s2)
+    s3(2) && !s3(1) && !s3(3)
+  }.holds
+
+  def test3(): Boolean = {
+    val s1 = set123()
+    val s2 = set123()
+    val s3 = union(s1, s2)
+    s3(1) && s3(2) && s3(3)
+  }.holds
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/valid/FlatMap.scala

+import leon.lang._
+import leon.collection._
+
+object FlatMap {
+
+  def append[T](l1: List[T], l2: List[T]): List[T] = l1 match {
+    case Cons(head, tail) => Cons(head, append(tail, l2))
+    case Nil() => l2
+  }
+
+  def associative_append_lemma[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+    append(append(l1, l2), l3) == append(l1, append(l2, l3))
+  }
+
+  def associative_append_lemma_induct[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+    l1 match {
+      case Nil() => associative_append_lemma(l1, l2, l3)
+      case Cons(head, tail) => associative_append_lemma(l1, l2, l3) && associative_append_lemma_induct(tail, l2, l3)
+    }
+  }.holds
+
+  def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
+    case Cons(head, tail) => append(f(head), flatMap(tail, f))
+    case Nil() => Nil()
+  }
+
+  def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
+    flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
+  }
+
+  def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
+    associative_lemma(list, f, g) &&
+    append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
+    (glist match {
+      case Cons(ghead, gtail) =>
+        associative_lemma_induct(list, flist, gtail, f, g)
+      case Nil() => flist match {
+        case Cons(fhead, ftail) =>
+          associative_lemma_induct(list, ftail, g(fhead), f, g)
+        case Nil() => list match {
+          case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+          case Nil() => true
+        }
+      }
+    })
+  }.holds
+
+}

testcases/verification/higher-order/valid/FoldAssociative.scala

+import leon._
+import leon.lang._
+
+object FoldAssociative {
+
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  sealed abstract class Option
+  case class Some(x: Int) extends Option
+  case class None() extends Option
+
+  def foldRight[A](list: List, state: A, f: (Int, A) => A): A = list match {
+    case Cons(head, tail) =>
+      val tailState = foldRight(tail, state, f)
+      f(head, tailState)
+    case Nil() => state
+  }
+
+  def take(list: List, count: Int): List = {
+    require(count >= 0)
+    list match {
+      case Cons(head, tail) if count > 0 => Cons(head, take(tail, count - 1))
+      case _ => Nil()
+    }
+  }
+
+  def drop(list: List, count: Int): List = {
+    require(count >= 0)
+    list match {
+      case Cons(head, tail) if count > 0 => drop(tail, count - 1)
+      case _ => list
+    }
+  }
+
+  def append(l1: List, l2: List): List = {
+    l1 match {
+      case Cons(head, tail) => Cons(head, append(tail, l2))
+      case Nil() => l2
+    }
+  }
+
+  def lemma_split(list: List, x: Int): Boolean = {
+    require(x >= 0)
+    val f = (x: Int, s: Int) => x + s
+    val l1 = take(list, x)
+    val l2 = drop(list, x)
+    foldRight(list, 0, f) == foldRight(l1, foldRight(l2, 0, f), f)
+  }
+
+  def lemma_split_induct(list: List, x: Int): Boolean = {
+    require(x >= 0)
+    val f = (x: Int, s: Int) => x + s
+    val l1 = take(list, x)
+    val l2 = drop(list, x)
+    lemma_split(list, x) && (list match {
+      case Cons(head, tail) if x > 0 =>
+        lemma_split_induct(tail, x - 1)
+      case _ => true
+    })
+  }.holds
+
+  def lemma_reassociative(list: List, x: Int): Boolean = {
+    require(x >= 0)
+    val f = (x: Int, s: Int) => x + s
+    val l1 = take(list, x)
+    val l2 = drop(list, x)
+
+    foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+  }
+
+  def lemma_reassociative_induct(list: List, x: Int): Boolean = {
+    require(x >= 0)
+    val f = (x: Int, s: Int) => x + s
+    val l1 = take(list, x)
+    val l2 = drop(list, x)
+    lemma_reassociative(list, x) && (list match {
+      case Cons(head, tail) if x > 0 =>
+        lemma_reassociative_induct(tail, x - 1)
+      case _ => true
+    })
+  }.holds
+
+  def lemma_reassociative_presplit(l1: List, l2: List): Boolean = {
+    val f = (x: Int, s: Int) => x + s
+    val list = append(l1, l2)
+    foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+  }
+
+  def lemma_reassociative_presplit_induct(l1: List, l2: List): Boolean = {
+    val f = (x: Int, s: Int) => x + s
+    val list = append(l1, l2)
+    lemma_reassociative_presplit(l1, l2) && (l1 match {
+      case Cons(head, tail) =>
+        lemma_reassociative_presplit_induct(tail, l2)
+      case Nil() => true
+    })
+  }.holds
+
+}

testcases/verification/higher-order/valid/HOInvocations.scala

+import leon.lang._
+
+object HOInvocations {
+  def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g
+
+  def passing_1(f: (Int) => Int) = {
+    switch(10, (x: Int) => x + 1, f)(2)
+  } ensuring { res => res > 0 }
+
+  def passing_2(x: Int, f: (Int) => Int, g: (Int) => Int) = {
+    require(x > 0)
+    switch(1, switch(x, f, g), g)(1)
+  } ensuring { res => res == f(1) }
+
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/valid/Lambdas.scala

+import leon.lang._
+
+object Lambdas {
+  def gen(x: Int): (Int) => Int = {
+    val f = (x: Int) => x + 1
+    val g = (x: Int) => x + 2
+    if (x > 0) g else f
+  }
+
+  def test(x: Int): Boolean = {
+    require(x > 0)
+    val f = gen(x)
+    f(x) == x + 2
+  }.holds
+}

testcases/verification/higher-order/valid/Lists1.scala

+import leon.lang._
+import leon.collection._
+import leon.annotation._
+
+object Lists1 {
+
+  def exists[T](list: List[T], f: T => Boolean): Boolean = list match {
+    case Cons(head, tail) => f(head) || exists(tail, f)
+    case Nil() => false
+  }
+
+  def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+    case Cons(head, tail) => f(head) && forall(tail, f)
+    case Nil() => true
+  }
+
+  def exists_lemma[T](list: List[T], f: T => Boolean): Boolean = {
+    exists(list, f) == !forall(list, (x: T) => !f(x))
+  }
+
+  def exists_lemma_induct[T](list: List[T], f: T => Boolean): Boolean = {
+    list match {
+      case Nil() => exists_lemma(list, f)
+      case Cons(head, tail) => exists_lemma(list, f) && exists_lemma_induct(tail, f)
+    }
+  }.holds 
+
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/valid/Lists2.scala

+import leon.lang._
+
+object Lists2 {
+  abstract class List[T]
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+    case Cons(head, tail) => f(head) && forall(tail, f)
+    case Nil() => true
+  }
+
+  def positive(list: List[Int]): Boolean = list match {
+    case Cons(head, tail) => if (head < 0) false else positive(tail)
+    case Nil() => true
+  }
+
+  def positive_lemma(list: List[Int]): Boolean = {
+    positive(list) == forall(list, (x: Int) => x >= 0)
+  }
+
+  def positive_lemma_induct(list: List[Int]): Boolean = {
+    list match {
+      case Nil() => positive_lemma(list)
+      case Cons(head, tail) => positive_lemma(list) && positive_lemma_induct(tail)
+    }
+  }.holds
+
+  def remove[T](list: List[T], e: T) : List[T] = {
+    list match {
+      case Nil() => Nil()
+      case Cons(x, xs) if x == e => remove(xs, e)
+      case Cons(x, xs)           => Cons(x, remove(xs, e))
+    }
+  } //ensuring { (res: List[T]) => forall(res, (x : T) => x != e) }
+
+  def remove_lemma[T](list: List[T], e: T): Boolean = {
+    forall(remove(list, e), (x : T) => x != e)
+  }
+
+  def remove_lemma_induct[T](list: List[T], e: T): Boolean = {
+    list match {
+      case Nil() => remove_lemma(list, e)
+      case Cons(head, tail) => remove_lemma(list, e) && remove_lemma_induct(tail, e)
+    }
+  }.holds
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/valid/Lists3.scala

+import leon.lang._
+
+object Lists3 {
+  abstract class List[T]
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+    case Cons(head, tail) => f(head) && forall(tail, f)
+    case Nil() => true
+  }
+
+  def positive(list: List[Int]): Boolean = list match {
+    case Cons(head, tail) => if (head < 0) false else positive(tail)
+    case Nil() => true
+  }
+
+  def gt(i: Int): Int => Boolean = x => x > i
+
+  def gte(i: Int): Int => Boolean = x => gt(i)(x) || x == i
+
+  def positive_lemma(list: List[Int]): Boolean = {
+    positive(list) == forall(list, gte(0))
+  }
+
+  def positive_lemma_induct(list: List[Int]): Boolean = {
+    list match {
+      case Nil() => positive_lemma(list)
+      case Cons(head, tail) => positive_lemma(list) && positive_lemma_induct(tail)
+    }
+  }.holds
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/valid/Lists4.scala

+import leon.lang._
+
+object Lists4 {
+  abstract class List[T]
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  def map[F,T](list: List[F], f: F => T): List[T] = list match {
+    case Cons(head, tail) => Cons(f(head), map(tail, f))
+    case Nil() => Nil()
+  }
+
+  def map_lemma[A,B,C](list: List[A], f: A => B, g: B => C): Boolean = {
+    map(list, (x: A) => g(f(x))) == map(map(list, f), g)
+  }
+
+  def map_lemma_induct[D,E,F](list: List[D], f: D => E, g: E => F): Boolean = {
+    list match {
+      case Nil() => map_lemma(list, f, g)
+      case Cons(head, tail) => map_lemma(list, f, g) && map_lemma_induct(tail, f, g)
+    }
+  }.holds
+
+}
+
+// vim: set ts=4 sw=4 et:

testcases/verification/higher-order/valid/Lists5.scala

+import leon.lang._
+import leon.collection._
+
+object Lists5 {
+  abstract class Option[T]
+  case class Some[T](value: T) extends Option[T]
+  case class None[T]() extends Option[T]
+
+  def find[T](f: T => Boolean, list: List[T]): Option[T] = list match {
+    case Cons(head, tail) => if (f(head)) Some(head) else find(f, tail)
+    case Nil() => None()
+  }
+
+  def exists[T](f: T => Boolean, list: List[T]): Boolean = list match {
+    case Cons(head, tail) => f(head) || exists(f, tail)
+    case Nil() => false
+  }
+
+  def equivalence_lemma[T](f: T => Boolean, list: List[T]): Boolean = {
+    find(f, list) match {
+      case Some(e) => exists(f, list)
+      case None() => !exists(f, list)
+    }
+  }
+
+  def equivalence_lemma_induct[T](f: T => Boolean, list: List[T]): Boolean = {
+    list match {
+      case Cons(head, tail) => equivalence_lemma(f, list) && equivalence_lemma_induct(f, tail)
+      case Nil() => equivalence_lemma(f, list)
+    }
+  }.holds
+}

testcases/verification/higher-order/valid/Lists6.scala

+import leon.lang._
+import leon.collection._
+
+object Lists6 {
+  def exists[T](list: List[T], f: T => Boolean): Boolean = {
+    list match {
+      case Cons(head, tail) => f(head) || exists(tail, f)
+      case Nil() => false
+    }
+  }
+
+  def associative_lemma[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
+    exists(list, (x: T) => f(x) || g(x)) == (exists(list, f) || exists(list, g))
+  }
+
+  def associative_lemma_induct[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
+    associative_lemma(list, f, g) && (list match {
+      case Cons(head, tail) => associative_lemma_induct(tail, f, g)
+      case Nil() => true
+    })
+  }.holds
+}