ListSet implementation.

frontends/library/stainless/collection/List.scala

@@ -5,7 +5,6 @@ package stainless.collection
 import scala.annotation.tailrec
 import scala.language.implicitConversions
 import scala.collection.immutable.{List => ScalaList}
-
 import stainless._
 import stainless.lang._
 import stainless.lang.StaticChecks._
@@ -1007,6 +1006,7 @@ object ListSpecs {
     case _ => false
   }
 
+  @opaque
   def subseqTail[T](l1: List[T], l2: List[T]): Unit = {
     require(!l1.isEmpty && subseq(l1, l2))
 
@@ -1130,6 +1130,11 @@ object ListSpecs {
     l1.forall(l2.contains)
   )
 
+  @opaque
+  def doesNotHaveHeadContainedInTail[T](@induct first: List[T], second: List[T]): Unit = {
+    require(second.nonEmpty && !first.contains(second.head) && first.forall(second.contains))
+  }.ensuring(_ => first.forall(second.tail.contains))
+
   @opaque
   def subsetRefl[T](l: List[T]): Unit = {
     if (!l.isEmpty) {
@@ -1151,4 +1156,183 @@ object ListSpecs {
     l1.content.subsetOf(l2.content)
   )
 
+  @opaque
+  def removingNonContained[T](@induct list: List[T], elem: T): Unit = {
+    require(!list.contains(elem))
+  }.ensuring(_ => list == list - elem)
+
+  @opaque
+  def removingContainment[T](elem: T, @induct first: List[T], second: List[T]): Unit = {
+    require(first.forall(second.contains))
+  }.ensuring(_ => (first - elem).forall((second - elem).contains))
+
+  @opaque
+  def selfContainment[T](list: List[T]): Unit = {
+    list match {
+      case Nil() => ()
+      case Cons(h, t) =>
+        selfContainment(t)
+        prependMaintainsCondition(h, t, list.contains)
+    }
+  }.ensuring(_ => list.forall(list.contains))
+
+  @opaque
+  def prependMaintainsCondition[T](elem: T, @induct list: List[T], p: T => Boolean): Unit = {
+    require(list.forall(p) && p(elem))
+  }.ensuring(_ => (elem :: list).forall(p))
+
+  @opaque
+  def nonContainedElementDoesNotInfluenceDifference[T](elem: T, first: List[T], @induct second: List[T]): Unit = {
+    require(!second.contains(elem))
+  }.ensuring(_ => second -- first == second -- (first - elem))
+
+  @opaque
+  def prependSubset[T](elem: T, @induct list: List[T]): Unit = {
+    ()
+  }.ensuring { _ ⇒
+    selfContainment(list)
+    val appended = elem :: list
+    list.forall((elem :: list).contains)
+  }
+
+  @opaque
+  def restOfSetIsSubset[T](first: List[T], second: List[T]): Unit = {
+    val diff = first -- second
+    first match {
+      case Nil() => assert(diff.isEmpty)
+      case Cons(h, t) if second.contains(h) =>
+        restOfSetIsSubset(t, second)
+      case Cons(h, t) =>
+        restOfSetIsSubset(t, second)
+        prependMaintainsCondition(h, t -- second, first.contains)
+    }
+  }.ensuring(_ => (first -- second).forall(first.contains))
+
+  @pure
+  def listDifference[T](@induct first: List[T], second: List[T]): List[T] = {
+    restOfSetIsSubset(first, second)
+    first -- second
+  }.ensuring(res => (res & second).isEmpty && res.forall(first.contains))
+
+  @opaque
+  def filteringWithoutHead[T](original: List[T], @induct filter: List[T]): Unit = {
+    require(original.nonEmpty && !filter.contains(original.head))
+  }.ensuring(_ =>
+    listDifference(original, filter) == original.head :: listDifference(original.tail, filter))
+
+  @opaque
+  def nonContainedInSuperSetNotContainedInSubset[T](elem: T, @induct first: List[T], second: List[T]): Unit = {
+    require(first.forall(second.contains) && !second.contains(elem))
+  }.ensuring(_ => !first.contains(elem))
+
+  @opaque
+  def removingSubsetInvertsTheRelationship[T](original: List[T], first: List[T], second: List[T]): Unit = {
+    require(first.forall(second.contains))
+    decreases(original.size)
+    original match {
+      case Nil() => ()
+      case Cons(h, t) if first.contains(h) && second.contains(h) =>
+        removingSubsetInvertsTheRelationship(t, first, second)
+
+      case Cons(h, t) if second.contains(h) && !first.contains(h) =>
+        val removedFirst = listDifference(original, first)
+        val removedSecond = listDifference(original, second)
+        removingSubsetInvertsTheRelationship(t, first, second)
+        containedTail(removedSecond, removedFirst)
+
+      case Cons(h, t) =>
+        val removedFirst = listDifference(original, first)
+        val removeTailSecond = listDifference(t, second)
+        removingSubsetInvertsTheRelationship(t, first, second)
+
+        nonContainedInSuperSetNotContainedInSubset(h, first, second)
+        filteringWithoutHead(original, first)
+        filteringWithoutHead(original, second)
+
+        containedTail(removeTailSecond, removedFirst)
+        prependMaintainsCondition(h, removeTailSecond, removedFirst.contains)
+    }
+  }.ensuring(_ => listDifference(original, second).forall(listDifference(original, first).contains))
+
+  @opaque
+  def transitivityLemma[T](first: List[T], second: List[T], third: List[T]): Unit = {
+    require(first.forall(second.contains) && second.forall(third.contains))
+    if (first.nonEmpty) {
+      transitivePredicate(first.head, first.contains, second.contains)
+      transitivePredicate(first.head, second.contains, third.contains)
+      transitivityLemma(first.tail, second, third)
+    }
+  }.ensuring(_ => first.forall(third.contains))
+
+  @opaque
+  def tailSelfContained[T](list: List[T]): Unit = {
+    require(list.nonEmpty)
+    list.tail match {
+      case Nil() => ()
+      case _: Cons[T] =>
+        selfContainment(list.tail)
+        containedTail(list.tail, list)
+    }
+  }.ensuring(_ => list.tail.forall(list.contains))
+
+  @opaque
+  def listIntersectionLemma[T](first: List[T], second: List[T]): Unit = {
+    first match {
+      case Nil() => ()
+      case Cons(h, t) if second.contains(h) =>
+        tailSelfContained(first)
+
+        listIntersectionLemma(t, second)
+
+        val tailIntersection = t & second
+        transitivityLemma(tailIntersection, t, first)
+        prependMaintainsCondition(h, tailIntersection, first.contains)
+
+      case Cons(_, t) =>
+        tailSelfContained(first)
+
+        listIntersectionLemma(t, second)
+
+        transitivityLemma(t & second, t, first)
+    }
+  }.ensuring { _ =>
+    val intersection = first & second
+    intersection.forall(first.contains) &&
+    intersection.forall(second.contains)
+  }
+
+  @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)
+
+    val firstIntersection = original & first
+    val secondIntersection = original & second
+
+    selfContainment(firstIntersection)
+    firstIntersection.forall(secondIntersection.contains)
+  }
+
+  @opaque
+  def containmentRelationship[T](elem: T, @induct first: List[T], second: List[T]): Unit = {
+    require(first.forall(second.contains))
+  }.ensuring(_ ⇒ first.contains(elem) ==> second.contains(elem))
+
+  @opaque
+  def transitivePredicate[T](elem: T, list: T ⇒ Boolean, p: T => Boolean): Unit = {
+    require(list(elem) ==> p(elem) && list(elem))
+  }.ensuring(_ => p(elem))
+
+  @opaque
+  def reflexivity[T](list: List[T]): Unit = {
+    list match {
+      case Nil() => ()
+      case Cons(_, t) =>
+        reflexivity(t)
+        containedTail(t, list)
+    }
+  }.ensuring(_ => list.forall(list.contains))
+
 }