diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index e9ac6bbec60776925a3ac5c1f91455511ccfeecc..c1adbf3f1230b2b7afb8553b28be87dc53613a99 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -193,20 +193,6 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(typeInsts, partialInsts, lambdaInsts)
}
- def toto: (Map[TypeTree, Matchers], Map[T, Matchers], Map[Lambda, Matchers]) = {
- var typeInsts: Map[TypeTree, Matchers] = Map.empty
- var partialInsts: Map[T, Matchers] = Map.empty
- var lambdaInsts: Map[Lambda, Matchers] = Map.empty
-
- for ((key, matchers) <- ignored.instantiations) key match {
- case TypeKey(tpe) => typeInsts += tpe -> matchers
- case CallerKey(caller, _) => partialInsts += caller -> matchers
- case LambdaKey(lambda, _) => lambdaInsts += lambda -> matchers
- }
-
- (typeInsts, partialInsts, lambdaInsts)
- }
-
override def registerFree(ids: Seq[(Identifier, T)]): Unit = {
super.registerFree(ids)
known ++= ids.map(_._2)
@@ -342,6 +328,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
private trait MatcherQuantification {
+ val start: T
val quantified: Set[T]
val matchers: Set[Matcher[T]]
val allMatchers: Map[T, Set[Matcher[T]]]
@@ -409,6 +396,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private def extractSubst(mapping: Set[(Set[T], Matcher[T], Matcher[T])]): (Set[T], Map[T,Either[T, Matcher[T]]], Boolean) = {
var constraints: Set[T] = Set.empty
+ var eqConstraints: Set[(T, T)] = Set.empty
var matcherEqs: List[(T, T)] = Nil
var subst: Map[T, Either[T, Matcher[T]]] = Map.empty
@@ -419,17 +407,20 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(qarg, arg) <- (qargs zip args)
} qarg match {
case Left(quant) if subst.isDefinedAt(quant) =>
- constraints += encoder.mkEquals(quant, Matcher.argValue(arg))
+ eqConstraints += (quant -> Matcher.argValue(arg))
case Left(quant) if quantified(quant) =>
subst += quant -> arg
case Right(qam) =>
val argVal = Matcher.argValue(arg)
- constraints += encoder.mkEquals(qam.encoded, argVal)
+ eqConstraints += (qam.encoded -> argVal)
matcherEqs :+= qam.encoded -> argVal
}
val substituter = encoder.substitute(subst.mapValues(Matcher.argValue))
- val enablers = constraints.filter(_ != trueT).map(substituter)
+ val substConstraints = constraints.filter(_ != trueT).map(substituter)
+ val substEqs = eqConstraints.map(p => substituter(p._1) -> p._2)
+ .filter(p => p._1 != p._2).map(p => encoder.mkEquals(p._1, p._2))
+ val enablers = substConstraints ++ substEqs
val isStrict = matcherEqs.forall(p => substituter(p._1) == p._2)
(enablers, subst, isStrict)
@@ -458,7 +449,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val substituter = encoder.substitute(substMap)
for ((b,ms) <- allMatchers; m <- ms) {
- val sb = enablers + substituter(b)
+ val sb = enablers ++ (if (b == start) Set.empty else Set(substituter(b)))
val sm = m.substitute(substituter, matcherSubst = msubst)
if (matchers(m)) {
@@ -478,6 +469,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
private class Quantification (
+ val start: T,
val qs: (Identifier, T),
val q2s: (Identifier, T),
val insts: (Identifier, T),
@@ -675,7 +667,9 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val subst = substMap + (template.qs._2 -> newQ)
val substituter = encoder.substitute(subst)
- val quantification = new Quantification(template.qs._1 -> newQ,
+ val quantification = new Quantification(
+ substituter(template.start),
+ template.qs._1 -> newQ,
template.q2s, template.insts, template.guardVar,
quantified,
matchers map (_.substitute(substituter)),
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index ab026ba3a2694ab311904627007f43c5912b44bd..6d4789421edf9f6ee3d6572251f0880e051de41e 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -221,7 +221,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
def requireDecomposition(e: Expr) = {
exists{
- case (_: Choose) | (_: Forall) => true
+ case (_: Choose) | (_: Forall) | (_: Lambda) => true
case (_: Assert) | (_: Ensuring) => true
case (_: FunctionInvocation) | (_: Application) => true
case _ => false
@@ -247,6 +247,17 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
res
}
+ def liftToIfExpr(parts: Seq[Expr], join: Seq[Expr] => Expr, recons: (Expr, Expr) => Expr): Expr = {
+ val partitions = groupWhile(parts)(!requireDecomposition(_))
+ partitions.map(join) match {
+ case Seq(e) => e
+ case s @ Seq(e1, e2) if !requireDecomposition(e1) =>
+ join(Seq(e1, rec(pathVar, e2)))
+ case seq =>
+ rec(pathVar, seq.reduceRight(recons))
+ }
+ }
+
def rec(pathVar: Identifier, expr: Expr): Expr = {
expr match {
case a @ Assert(cond, err, body) =>
@@ -290,25 +301,17 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
case p : Passes => sys.error("'Passes's should have been eliminated before generating templates.")
case i @ Implies(lhs, rhs) =>
- implies(rec(pathVar, lhs), rec(pathVar, rhs))
-
- case a @ And(parts) =>
- if (requireDecomposition(a)) {
- val partitions = groupWhile(parts)(!requireDecomposition(_))
- val ifExpr = partitions.map(andJoin).reduceRight((a,b) => IfExpr(a, b, BooleanLiteral(false)))
- rec(pathVar, ifExpr)
+ if (requireDecomposition(i)) {
+ rec(pathVar, Or(Not(lhs), rhs))
} else {
- a
+ implies(rec(pathVar, lhs), rec(pathVar, rhs))
}
+ case a @ And(parts) =>
+ liftToIfExpr(parts, andJoin, (a,b) => IfExpr(a, b, BooleanLiteral(false)))
+
case o @ Or(parts) =>
- if (requireDecomposition(o)) {
- val partitions = groupWhile(parts)(!requireDecomposition(_))
- val ifExpr = partitions.map(orJoin).reduceRight((a,b) => IfExpr(a, BooleanLiteral(true), b))
- rec(pathVar, ifExpr)
- } else {
- o
- }
+ liftToIfExpr(parts, orJoin, (a,b) => IfExpr(a, BooleanLiteral(true), b))
case i @ IfExpr(cond, thenn, elze) => {
if(!requireDecomposition(i)) {
diff --git a/src/test/resources/regression/verification/purescala/valid/FlatMap.scala b/src/test/resources/regression/verification/purescala/valid/FlatMap.scala
index 3f1dd39ffd79dd10d1300a9aa0ac60f2b29d46a0..878b61456b6658b13f05d0e5f1b05dc25d959676 100644
--- a/src/test/resources/regression/verification/purescala/valid/FlatMap.scala
+++ b/src/test/resources/regression/verification/purescala/valid/FlatMap.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
object FlatMap {
@@ -17,7 +18,7 @@ object FlatMap {
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)
+ case Cons(head, tail) => associative_append_lemma(l1, l2, l3) because associative_append_lemma_induct(tail, l2, l3)
}
}.holds
@@ -31,20 +32,21 @@ object FlatMap {
}
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
+ associative_lemma(list, f, g) because {
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) because
+ (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
}
diff --git a/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala b/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala
index ff0444f269dd6f9b2a2b7f2b54e13f54c6755ab2..6920231115fea93a1b7c7cefc27691a0ee2471bb 100644
--- a/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala
+++ b/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala
@@ -2,6 +2,7 @@
import leon._
import leon.lang._
+import leon.proof._
object FoldAssociative {
@@ -56,7 +57,7 @@ object FoldAssociative {
val f = (x: Int, s: Int) => x + s
val l1 = take(list, x)
val l2 = drop(list, x)
- lemma_split(list, x) && (list match {
+ lemma_split(list, x) because (list match {
case Cons(head, tail) if x > 0 =>
lemma_split_induct(tail, x - 1)
case _ => true
@@ -77,7 +78,7 @@ object FoldAssociative {
val f = (x: Int, s: Int) => x + s
val l1 = take(list, x)
val l2 = drop(list, x)
- lemma_reassociative(list, x) && (list match {
+ lemma_reassociative(list, x) because (list match {
case Cons(head, tail) if x > 0 =>
lemma_reassociative_induct(tail, x - 1)
case _ => true
@@ -93,7 +94,7 @@ object FoldAssociative {
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 {
+ lemma_reassociative_presplit(l1, l2) because (l1 match {
case Cons(head, tail) =>
lemma_reassociative_presplit_induct(tail, l2)
case Nil() => true
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists1.scala b/src/test/resources/regression/verification/purescala/valid/Lists1.scala
index 4dbee2b7137c8a427cf7bd302e3849050f0b2bc7..0b10f27d05354ef02fab45cc935f7f3695bee378 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists1.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
import leon.annotation._
@@ -21,10 +22,10 @@ object Lists1 {
}
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)
- }
+ exists_lemma(list, f) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => exists_lemma_induct(tail, f)
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists2.scala b/src/test/resources/regression/verification/purescala/valid/Lists2.scala
index 57d86819bf5cb17a77e451aead68393f7c30ed17..79126cb2226b55c811313c1c82375b977265ffc2 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists2.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
object Lists2 {
abstract class List[T]
@@ -22,10 +23,10 @@ object Lists2 {
}
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)
- }
+ positive_lemma(list) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => positive_lemma_induct(tail)
+ })
}.holds
def remove[T](list: List[T], e: T) : List[T] = {
@@ -41,10 +42,10 @@ object Lists2 {
}
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)
- }
+ remove_lemma(list, e) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => remove_lemma_induct(tail, e)
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists3.scala b/src/test/resources/regression/verification/purescala/valid/Lists3.scala
index 1dae4a5c6f5ecf649bc78d2b19151007cc57a47d..dedab2a4e32aee2bf02e816ad8677e02a0a669a2 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists3.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists3.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
object Lists3 {
abstract class List[T]
@@ -26,10 +27,10 @@ object Lists3 {
}
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)
- }
+ positive_lemma(list) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => positive_lemma_induct(tail)
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists4.scala b/src/test/resources/regression/verification/purescala/valid/Lists4.scala
index d4e212aff31bd011ce143901efa34a5a428f0d94..124d944da9e0769e74d43c4b3612f5a79657d9fa 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists4.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists4.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
object Lists4 {
abstract class List[T]
@@ -17,10 +18,10 @@ object Lists4 {
}
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)
- }
+ map_lemma(list, f, g) because (list match {
+ case Nil() => true
+ case Cons(head, tail) => map_lemma_induct(tail, f, g)
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists5.scala b/src/test/resources/regression/verification/purescala/valid/Lists5.scala
index f8fd9491fee2ad4a27ed9a4230ba1b30afec3093..9826dc372a2a79ae733696126de8565394148ff8 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists5.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists5.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
object Lists5 {
@@ -26,9 +27,9 @@ object Lists5 {
}
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)
- }
+ equivalence_lemma(f, list) because (list match {
+ case Cons(head, tail) => equivalence_lemma_induct(f, tail)
+ case Nil() => true
+ })
}.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists6.scala b/src/test/resources/regression/verification/purescala/valid/Lists6.scala
index 8257249830949d07dc36c0c74633d166bebbe561..763fabdaddab6a7d4732dcd2c102beb897b27d0e 100644
--- a/src/test/resources/regression/verification/purescala/valid/Lists6.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Lists6.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
+import leon.proof._
import leon.collection._
object Lists6 {
@@ -16,7 +17,7 @@ object Lists6 {
}
def associative_lemma_induct[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
- associative_lemma(list, f, g) && (list match {
+ associative_lemma(list, f, g) because (list match {
case Cons(head, tail) => associative_lemma_induct(tail, f, g)
case Nil() => true
})
diff --git a/src/test/resources/regression/verification/purescala/valid/Monads3.scala b/src/test/resources/regression/verification/purescala/valid/Monads3.scala
index 05b46ceb0f02a96811b7ca8a4606b4b4b30de3e3..8fac4a7e076510389bc999a271506d2f89c6a9cd 100644
--- a/src/test/resources/regression/verification/purescala/valid/Monads3.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Monads3.scala
@@ -22,20 +22,21 @@ object Monads3 {
}
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
+ associative_lemma(list, f, g) because {
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) because
+ (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
def left_unit_law[T,U](x: T, f: T => List[U]): Boolean = {
@@ -47,7 +48,7 @@ object Monads3 {
}
def right_unit_induct[T,U](list: List[T]): Boolean = {
- right_unit_law(list) && (list match {
+ right_unit_law(list) because (list match {
case Cons(head, tail) => right_unit_induct(tail)
case Nil() => true
})
@@ -62,7 +63,7 @@ object Monads3 {
}
def flatMap_to_zero_induct[T,U](list: List[T]): Boolean = {
- flatMap_to_zero_law(list) && (list match {
+ flatMap_to_zero_law(list) because (list match {
case Cons(head, tail) => flatMap_to_zero_induct(tail)
case Nil() => true
})
diff --git a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
index 29133762e6da8118e1e380b6fabb4fb3880d482b..dd8e16f43b2a9073764ff319fcc91d733e5f1489 100644
--- a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
@@ -72,7 +72,7 @@ object ParBalance {
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 {
+ (foldLeft(list, p, f) == (BigInt(0), BigInt(0))) == balanced_withReduce(list, p) because (list match {
case Cons(head, tail) =>
val p2 = f(p, head)
balanced_foldLeft_equivalence(tail, p2)
@@ -178,14 +178,14 @@ object ParBalance {
}.holds
def reverse_init_equivalence(list: List): Boolean = {
- reverse(init(list)) == tail(reverse(list)) && (list match {
+ reverse(init(list)) == tail(reverse(list)) because (list match {
case Cons(head, tail) => reverse_init_equivalence(tail)
case Nil() => true
})
}.holds
def reverse_equality_equivalence(l1: List, l2: List): Boolean = {
- (l1 == l2) == (reverse(l1) == reverse(l2)) && ((l1, l2) match {
+ (l1 == l2) == (reverse(l1) == reverse(l2)) because ((l1, l2) match {
case (Cons(h1, t1), Cons(h2, t2)) => reverse_equality_equivalence(t1, t2)
case _ => true
})
@@ -198,7 +198,7 @@ object ParBalance {
// always decreasing, so that the termination checker can prove termination.
def reverse_reverse_equivalence(s: BigInt, list: List): Boolean = {
require(size(list) == s)
- reverse(reverse(list)) == list && ((list, reverse(list)) match {
+ reverse(reverse(list)) == list because ((list, reverse(list)) match {
case (Cons(h1, t1), Cons(h2, t2)) =>
reverse_reverse_equivalence(size(t1), t1) && reverse_reverse_equivalence(size(t2), t2)
case _ => true
diff --git a/testcases/verification/higher-order/valid/FlatMap.scala b/testcases/verification/higher-order/valid/FlatMap.scala
index 56f8c47e86d835055e6c3a9ea44cb7b886e464fb..aa4baa08baf2e7fe4c454536da2f5853a3f8b09c 100644
--- a/testcases/verification/higher-order/valid/FlatMap.scala
+++ b/testcases/verification/higher-order/valid/FlatMap.scala
@@ -13,10 +13,10 @@ object FlatMap {
}
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)
- }
+ associative_append_lemma(l1, l2, l3) because (l1 match {
+ case Nil() => true
+ case Cons(head, tail) => associative_append_lemma_induct(tail, l2, l3)
+ })
}.holds
def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
@@ -29,20 +29,21 @@ object FlatMap {
}
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
+ associative_lemma(list, f, g) because {
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) because
+ (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
}
diff --git a/testcases/web/verification/10_FoldAssociative.scala b/testcases/web/verification/10_FoldAssociative.scala
index ff0444f269dd6f9b2a2b7f2b54e13f54c6755ab2..63354e13ab862c8d60c0af922af5fbac250c8332 100644
--- a/testcases/web/verification/10_FoldAssociative.scala
+++ b/testcases/web/verification/10_FoldAssociative.scala
@@ -56,7 +56,7 @@ object FoldAssociative {
val f = (x: Int, s: Int) => x + s
val l1 = take(list, x)
val l2 = drop(list, x)
- lemma_split(list, x) && (list match {
+ lemma_split(list, x) because (list match {
case Cons(head, tail) if x > 0 =>
lemma_split_induct(tail, x - 1)
case _ => true
@@ -77,7 +77,7 @@ object FoldAssociative {
val f = (x: Int, s: Int) => x + s
val l1 = take(list, x)
val l2 = drop(list, x)
- lemma_reassociative(list, x) && (list match {
+ lemma_reassociative(list, x) because (list match {
case Cons(head, tail) if x > 0 =>
lemma_reassociative_induct(tail, x - 1)
case _ => true
@@ -93,7 +93,7 @@ object FoldAssociative {
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 {
+ lemma_reassociative_presplit(l1, l2) because (l1 match {
case Cons(head, tail) =>
lemma_reassociative_presplit_induct(tail, l2)
case Nil() => true