From d55d4ab4854d7251c0dc39a8aa36a2f0de05e172 Mon Sep 17 00:00:00 2001 From: Jad Hamza Date: Thu, 10 Sep 2020 14:08:08 +0200 Subject: [PATCH] Remove forall quantifiers in List library --- .../library/stainless/collection/List.scala | 54 ++----------------- .../stainless/collection/ListSet.scala | 16 +++--- 2 files changed, 12 insertions(+), 58 deletions(-) diff --git a/frontends/library/stainless/collection/List.scala b/frontends/library/stainless/collection/List.scala index d7add435e3..d1e28b7497 100644 --- a/frontends/library/stainless/collection/List.scala +++ b/frontends/library/stainless/collection/List.scala @@ -1006,6 +1006,7 @@ object ListSpecs { case _ => false } + @opaque def subseqTail[T](l1: List[T], l2: List[T]): Unit = { require(!l1.isEmpty && subseq(l1, l2)) @@ -1171,16 +1172,10 @@ object ListSpecs { case Nil() => () case Cons(h, t) => selfContainment(t) - expandPredicate(t, t.contains, list.contains) prependMaintainsCondition(h, t, list.contains) } }.ensuring(_ => list.forall(list.contains)) - @opaque - def expandPredicate[T](@induct list: List[T], p1: T => Boolean, p2: T => Boolean): Unit = { - require(forall((elem: T) => p1(elem) ==> p2(elem)) && list.forall(p1)) - }.ensuring(_ => list.forall(p2)) - @opaque def prependMaintainsCondition[T](elem: T, @induct list: List[T], p: T => Boolean): Unit = { require(list.forall(p) && p(elem)) @@ -1192,10 +1187,11 @@ object ListSpecs { }.ensuring(_ => second -- first == second -- (first - elem)) @opaque - def prependSubset[T](elem: T, @induct list: List[T]): Unit = {}.ensuring { _ ⇒ + def prependSubset[T](elem: T, @induct list: List[T]): Unit = { + () + }.ensuring { _ ⇒ selfContainment(list) val appended = elem :: list - expandPredicate(list, list.contains, appended.contains) list.forall((elem :: list).contains) } @@ -1206,10 +1202,8 @@ object ListSpecs { case Nil() => assert(diff.isEmpty) case Cons(h, t) if second.contains(h) => restOfSetIsSubset(t, second) - expandPredicate(diff, t.contains, first.contains) case Cons(h, t) => restOfSetIsSubset(t, second) - expandPredicate(t -- second, t.contains, first.contains) prependMaintainsCondition(h, t -- second, first.contains) } }.ensuring(_ => (first -- second).forall(first.contains)) @@ -1304,30 +1298,20 @@ object ListSpecs { }.ensuring { _ => val intersection = first & second intersection.forall(first.contains) && - intersection.forall(second.contains) && - forall((elem: T) => intersection.contains(elem) == (first.contains(elem) && second.contains(elem))) + intersection.forall(second.contains) } - @opaque - def listSubsetContainmentLemma[T](original: List[T], @induct first: List[T], second: List[T]): Unit = { - require(first.forall(second.contains)) - }.ensuring(_ => - forall((elem: T) => - (original.contains(elem) && first.contains(elem)) ==> (original.contains(elem) && second.contains(elem)))) - @opaque def listSubsetIntersectionLemma[T](original: List[T], first: List[T], second: List[T]): Unit = { require(first.forall(second.contains)) }.ensuring { _ => listIntersectionLemma(original, first) listIntersectionLemma(original, second) - listSubsetContainmentLemma(original, first, second) val firstIntersection = original & first val secondIntersection = original & second selfContainment(firstIntersection) - expandPredicate(firstIntersection, firstIntersection.contains, secondIntersection.contains) firstIntersection.forall(secondIntersection.contains) } @@ -1351,32 +1335,4 @@ object ListSpecs { } }.ensuring(_ => list.forall(list.contains)) - @opaque - def filteringWithExpandingPredicateCreatesSubsets[T](first: T ⇒ Boolean, second: T ⇒ Boolean, list: List[T]): Unit = { - require(forall((elem: T) ⇒ first(elem) ==> second(elem))) - list match { - case Nil() => - case Cons(h, t) => - filteringWithExpandingPredicateCreatesSubsets(first, second, t) - val secondTailFiltered = t.filter(node => second(node)) - val secondFiltered = list.filter(node => second(node)) - reflexivity(secondFiltered) - assert(secondTailFiltered.forall(secondFiltered.contains)) - - val firstTailFiltered = t.filter(node => first(node)) - assert(firstTailFiltered.forall(secondTailFiltered.contains)) - - if (!first(h)) { - transitivityLemma(firstTailFiltered, secondTailFiltered, secondFiltered) - } else { - transitivePredicate(h, first, second) - transitivityLemma(firstTailFiltered, secondTailFiltered, secondFiltered) - } - } - }.ensuring { _ => - val secondFiltered = list.filter(node => second(node)) - val firstFiltered = list.filter(node => first(node)) - firstFiltered.forall(secondFiltered.contains) - } - } diff --git a/frontends/library/stainless/collection/ListSet.scala b/frontends/library/stainless/collection/ListSet.scala index 13d578e82f..1f68fe3086 100644 --- a/frontends/library/stainless/collection/ListSet.scala +++ b/frontends/library/stainless/collection/ListSet.scala @@ -3,7 +3,7 @@ package stainless.collection import stainless.annotation._ import stainless.lang._ -@library +@ignore case class ListSet[T](toList: List[T]) { require(ListOps.noDuplicate(toList)) @@ -20,7 +20,7 @@ case class ListSet[T](toList: List[T]) { def ++(other: ListSet[T]): ListSet[T] = { val union = ListSetSpec.removeDuplicates(this.toList ++ other.toList) ListSet(union) - }.ensuring(res ⇒ forall((elem: T) ⇒ (this.contains(elem) || other.contains(elem)) == res.contains(elem))) + } def -(elem: T): ListSet[T] = { ListSetSpec.removingFromASetResultsInASet(elem, toList) @@ -32,18 +32,16 @@ case class ListSet[T](toList: List[T]) { ListSpecs.restOfSetIsSubset(toList, other.toList) ListSet(toList -- other.toList) }.ensuring(res ⇒ - forall((elem: T) ⇒ (this.contains(elem) && !other.contains(elem)) == res.contains(elem)) && - (res & other).isEmpty && - res.subsetOf(this)) + (res & other).isEmpty && + res.subsetOf(this)) def &(other: ListSet[T]): ListSet[T] = { ListSetSpec.listSetIntersection(toList, other.toList) ListSpecs.listIntersectionLemma(toList, other.toList) ListSet(toList & other.toList) }.ensuring(res ⇒ - forall((elem: T) ⇒ (this.contains(elem) && other.contains(elem)) == res.contains(elem)) && - res.subsetOf(this) && - res.subsetOf(other)) + res.subsetOf(this) && + res.subsetOf(other)) def filter(predicate: T ⇒ Boolean): ListSet[T] = { ListSetSpec.filteringPreservesPredicate(toList, predicate) @@ -184,7 +182,7 @@ object ListSetSpec { case Cons(h, t) ⇒ if (t.contains(h)) removeDuplicates(t) else h :: removeDuplicates(t) case Nil() ⇒ Nil[T]() } - }.ensuring(res ⇒ ListOps.noDuplicate(res) && forall((elem: T) ⇒ list.contains(elem) == res.contains(elem))) + }.ensuring(res ⇒ ListOps.noDuplicate(res)) @opaque def listSetDiff[T](@induct first: List[T], second: List[T]): Unit = {