Remove forall, first part.

epfl-lara · Aug 20, 2020 · 6acedb1 · 6acedb1
1 parent 2e8b521
commit 6acedb1
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/frontends/library/stainless/collection/ListSet.scala b/frontends/library/stainless/collection/ListSet.scala
@@ -20,7 +20,10 @@ case class ListSet[T](toList: List[T]) {
   def ++(other: ListSet[T]): ListSet[T] = {
     val union = ListSetSpecs.removeDuplicates(this.toList ++ other.toList)
     ListSet(union)
-  }.ensuring(res ⇒ forall((elem: T) ⇒ (this.contains(elem) || other.contains(elem)) == res.contains(elem)))
+  }.ensuring(res ⇒
+    this.toList.forall(res.contains) &&
+      other.toList.forall(res.contains) &&
+      res.toList.forall(value => contains(value) || other.contains(value)))
 
   def -(elem: T): ListSet[T] = {
     ListSetSpecs.removingFromASetResultsInASet(elem, toList)
@@ -32,7 +35,6 @@ 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))
 
@@ -41,7 +43,7 @@ case class ListSet[T](toList: List[T]) {
     ListSpecs.listIntersectionLemma(toList, other.toList)
     ListSet(toList & other.toList)
   }.ensuring(res ⇒
-    forall((elem: T) ⇒ (this.contains(elem) && other.contains(elem)) == res.contains(elem)) &&
+    res.toList.forall(value => this.contains(value) && other.contains(value)) &&
       res.subsetOf(this) &&
       res.subsetOf(other))
 
@@ -184,7 +186,7 @@ object ListSetSpecs {
       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) && list.forall(res.contains) && res.forall(list.contains))
 
   @opaque
   def listSetDiff[T](@induct first: List[T], second: List[T]): Unit = {