diff --git a/library/collection/List.scala b/library/collection/List.scala
index 404c53c44596938abd9b4f7576b923f6778e86ff..4462aca308c5f1756ab9ff5b9e9f42b8a8cc6c8f 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -6,6 +6,7 @@ import leon._
import leon.lang._
import leon.annotation._
import leon.math._
+import leon.proof._
@library
sealed abstract class List[T] {
@@ -373,9 +374,9 @@ sealed abstract class List[T] {
res.size == this.size
}
- def isEmpty = this match {
+ def isEmpty = this match {
case Nil() => true
- case _ => false
+ case _ => false
}
// Higher-order API
@@ -393,7 +394,7 @@ sealed abstract class List[T] {
case Nil() => z
case Cons(h, t) => f(h, t.foldRight(z)(f))
}
-
+
def scanLeft[R](z: R)(f: (R,T) => R): List[R] = { this match {
case Nil() => z :: Nil()
case Cons(h,t) => z :: t.scanLeft(f(z,h))(f)
@@ -401,12 +402,12 @@ sealed abstract class List[T] {
def scanRight[R](z: R)(f: (T,R) => R): List[R] = { this match {
case Nil() => z :: Nil[R]()
- case Cons(h, t) =>
+ case Cons(h, t) =>
val rest@Cons(h1,_) = t.scanRight(z)(f)
f(h, h1) :: rest
}} ensuring { !_.isEmpty }
- def flatMap[R](f: T => List[R]): List[R] =
+ def flatMap[R](f: T => List[R]): List[R] =
ListOps.flatten(this map f)
def filter(p: T => Boolean): List[T] = { this match {
@@ -518,20 +519,23 @@ object ListOps {
case Cons(_, t) => isSorted(t)
}
- def sorted(ls: List[BigInt]): List[BigInt] = ls match {
- case Cons(h, t) => insSort(sorted(t), h)
- case Nil() => Nil()
- }
+ def sorted(ls: List[BigInt]): List[BigInt] = { ls match {
+ case Cons(h, t) => sortedIns(sorted(t), h)
+ case Nil() => Nil[BigInt]()
+ }} ensuring { isSorted _ }
- def insSort(ls: List[BigInt], v: BigInt): List[BigInt] = ls match {
- case Nil() => Cons(v, Nil())
- case Cons(h, t) =>
- if (v <= h) {
- Cons(v, t)
- } else {
- Cons(h, insSort(t, v))
- }
- }
+ private def sortedIns(ls: List[BigInt], v: BigInt): List[BigInt] = {
+ require(isSorted(ls))
+ ls match {
+ case Nil() => Cons(v, Nil())
+ case Cons(h, t) =>
+ if (v <= h) {
+ Cons(v, t)
+ } else {
+ Cons(h, sortedIns(t, v))
+ }
+ }
+ } ensuring { isSorted _ }
}
case class Cons[T](h: T, t: List[T]) extends List[T]
@@ -547,20 +551,20 @@ object :: {
}
+import ListOps._
+
@library
object ListSpecs {
- def snocIndex[T](l : List[T], t : T, i : BigInt) : Boolean = {
+ def snocIndex[T](l: List[T], t: T, i: BigInt): Boolean = {
require(0 <= i && i < l.size + 1)
- // proof:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t)) because
(l match {
case Nil() => true
case Cons(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
- }) &&
- // claim:
- ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ })
}.holds
- def reverseIndex[T](l : List[T], i : BigInt) : Boolean = {
+ def reverseIndex[T](l: List[T], i: BigInt): Boolean = {
require(0 <= i && i < l.size)
(l match {
case Nil() => true
@@ -569,68 +573,160 @@ object ListSpecs {
(l.reverse.apply(i) == l.apply(l.size - 1 - i))
}.holds
- def appendIndex[T](l1 : List[T], l2 : List[T], i : BigInt) : Boolean = {
+ def snocLast[T](l: List[T], x: T): Boolean = {
+ ((l :+ x).last == x) because {
+ l match {
+ case Nil() => true
+ case Cons(y, ys) => {
+ ((y :: ys) :+ x).last ==| trivial |
+ (y :: (ys :+ x)).last ==| trivial |
+ (ys :+ x).last ==| snocLast(ys, x) |
+ x
+ }.qed
+ }
+ }
+ }.holds
+
+ def headReverseLast[T](l: List[T]): Boolean = {
+ require (!l.isEmpty)
+ (l.head == l.reverse.last) because {
+ l match {
+ case Cons(x, xs) => {
+ (x :: xs).head ==| trivial |
+ x ==| snocLast(xs.reverse, x) |
+ (xs.reverse :+ x).last ==| trivial |
+ (x :: xs).reverse.last
+ }.qed
+ }
+ }
+ }.holds
+
+ def appendIndex[T](l1: List[T], l2: List[T], i: BigInt): Boolean = {
require(0 <= i && i < l1.size + l2.size)
- (l1 match {
- case Nil() => true
- case Cons(x,xs) => if (i==BigInt(0)) true else appendIndex[T](xs,l2,i-1)
- }) &&
- ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ ( (l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)) ) because {
+ l1 match {
+ case Nil() => true
+ case Cons(x,xs) =>
+ (i != BigInt(0)) ==> appendIndex[T](xs, l2, i - 1)
+ }
+ }
}.holds
- def appendAssoc[T](l1 : List[T], l2 : List[T], l3 : List[T]) : Boolean = {
- (l1 match {
- case Nil() => true
- case Cons(x,xs) => appendAssoc(xs,l2,l3)
- }) &&
- (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ @induct
+ def appendAssoc[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+ (l1 ++ l2) ++ l3 == l1 ++ (l2 ++ l3)
}.holds
- def snocIsAppend[T](l : List[T], t : T) : Boolean = {
- (l match {
- case Nil() => true
- case Cons(x,xs) => snocIsAppend(xs,t)
- }) &&
- ((l :+ t) == l ++ Cons[T](t, Nil()))
+ @induct
+ def rightUnitAppend[T](l1: List[T]): Boolean = {
+ l1 ++ Nil() == l1
}.holds
- def snocAfterAppend[T](l1 : List[T], l2 : List[T], t : T) : Boolean = {
- (l1 match {
- case Nil() => true
- case Cons(x,xs) => snocAfterAppend(xs,l2,t)
- }) &&
- ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ // This follows immediately from the definition of `++` but we
+ // include it here anyway for completeness.
+ def leftUnitAppend[T](l1: List[T]): Boolean = {
+ Nil() ++ l1 == l1
}.holds
- def snocReverse[T](l : List[T], t : T) : Boolean = {
- (l match {
- case Nil() => true
- case Cons(x,xs) => snocReverse(xs,t)
- }) &&
- ((l :+ t).reverse == Cons(t, l.reverse))
+ def snocIsAppend[T](l: List[T], t: T): Boolean = {
+ ( (l :+ t) == l ++ Cons[T](t, Nil()) ) because {
+ l match {
+ case Nil() => true
+ case Cons(x,xs) => snocIsAppend(xs,t)
+ }
+ }
}.holds
- def reverseReverse[T](l : List[T]) : Boolean = {
- (l match {
- case Nil() => true
- case Cons(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
- }) &&
- (l.reverse.reverse == l)
+ def snocAfterAppend[T](l1: List[T], l2: List[T], t: T): Boolean = {
+ ( (l1 ++ l2) :+ t == l1 ++ (l2 :+ t) ) because {
+ l1 match {
+ case Nil() => true
+ case Cons(x,xs) => snocAfterAppend(xs,l2,t)
+ }
+ }
}.holds
- //// my hand calculation shows this should work, but it does not seem to be found
- //def reverseAppend[T](l1 : List[T], l2 : List[T]) : Boolean = {
- // (l1 match {
- // case Nil() => true
- // case Cons(x,xs) => {
- // reverseAppend(xs,l2) &&
- // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
- // l1.reverse == (xs.reverse :+ x)
- // }
- // }) &&
- // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
- //}.holds
+ def snocReverse[T](l: List[T], t: T): Boolean = {
+ ( (l :+ t).reverse == Cons(t, l.reverse) ) because {
+ l match {
+ case Nil() => true
+ case Cons(x,xs) => snocReverse(xs,t)
+ }
+ }
+ }.holds
+ def reverseReverse[T](l: List[T]): Boolean = {
+ l.reverse.reverse == l because {
+ l match {
+ case Nil() => trivial
+ case Cons(x, xs) => {
+ (xs.reverse :+ x).reverse ==| snocReverse[T](xs.reverse, x) |
+ x :: xs.reverse.reverse ==| reverseReverse[T](xs) |
+ (x :: xs)
+ }.qed
+ }
+ }
+ }.holds
+
+ def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
+ ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
+ l1 match {
+ case Nil() => {
+ (Nil() ++ l2).reverse ==| trivial |
+ l2.reverse ==| rightUnitAppend(l2.reverse) |
+ l2.reverse ++ Nil() ==| trivial |
+ l2.reverse ++ Nil().reverse
+ }.qed
+ case Cons(x, xs) => {
+ ((x :: xs) ++ l2).reverse ==| trivial |
+ (x :: (xs ++ l2)).reverse ==| trivial |
+ (xs ++ l2).reverse :+ x ==| reverseAppend(xs, l2) |
+ (l2.reverse ++ xs.reverse) :+ x ==|
+ snocAfterAppend(l2.reverse, xs.reverse, x) |
+ l2.reverse ++ (xs.reverse :+ x) ==| trivial |
+ l2.reverse ++ (x :: xs).reverse
+ }.qed
+ }
+ }
+ }.holds
+
+ def snocFoldRight[A, B](xs: List[A], y: A, z: B, f: (A, B) => B): Boolean = {
+ ( (xs :+ y).foldRight(z)(f) == xs.foldRight(f(y, z))(f) ) because {
+ xs match {
+ case Nil() => true
+ case Cons(x, xs) => snocFoldRight(xs, y, z, f)
+ }
+ }
+ }.holds
+
+ def folds[A, B](xs: List[A], z: B, f: (B, A) => B): Boolean = {
+ val f2 = (x: A, z: B) => f(z, x)
+ ( xs.foldLeft(z)(f) == xs.reverse.foldRight(z)(f2) ) because {
+ xs match {
+ case Nil() => true
+ case Cons(x, xs) => {
+ (x :: xs).foldLeft(z)(f) ==| trivial |
+ xs.foldLeft(f(z, x))(f) ==| folds(xs, f(z, x), f) |
+ xs.reverse.foldRight(f(z, x))(f2) ==| trivial |
+ xs.reverse.foldRight(f2(x, z))(f2) ==|
+ snocFoldRight(xs.reverse, x, z, f2) |
+ (xs.reverse :+ x).foldRight(z)(f2) ==| trivial |
+ (x :: xs).reverse.foldRight(z)(f2)
+ }.qed
+ }
+ }
+ }.holds
+
+ def scanVsFoldLeft[A, B](l: List[A], z: B, f: (B, A) => B): Boolean = {
+ ( l.scanLeft(z)(f).last == l.foldLeft(z)(f) ) because {
+ l match {
+ case Nil() => true
+ case Cons(x, xs) => scanVsFoldLeft(xs, f(z, x), f)
+ }
+ }
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
//def associative[T,U](l1: List[T], l2: List[T], f: List[T] => U, op: (U,U) => U) = {
// f(l1 ++ l2) == op(f(l1), f(l2))
//}
@@ -643,27 +739,32 @@ object ListSpecs {
// associative[T, Boolean](l1, l2, _.exists(p), _ && _ )
//}.holds
- //@induct
- //def folds[T,R](l : List[T], z : R, f : (R,T) => R) = {
- // { l match {
- // case Nil() => true
- // case Cons(h,t) => snocReverse[T](t, h)
- // }} &&
- // l.foldLeft(z)(f) == l.reverse.foldRight((x:T,y:R) => f(y,x))(z)
- //}.holds
- //
-
- //Can't prove this
- //@induct
- //def scanVsFoldLeft[A,B](l : List[A], z: B, f: (B,A) => B): Boolean = {
- // l.scanLeft(z)(f).last == l.foldLeft(z)(f)
- //}.holds
-
@induct
def scanVsFoldRight[A,B](l: List[A], z: B, f: (A,B) => B): Boolean = {
l.scanRight(z)(f).head == l.foldRight(z)(f)
}.holds
+ def appendContent[A](l1: List[A], l2: List[A]) = {
+ l1.content ++ l2.content == (l1 ++ l2).content
+ }.holds
+
+ def flattenPreservesContent[T](ls: List[List[T]]): Boolean = {
+ val f: (List[T], Set[T]) => Set[T] = _.content ++ _
+ ( flatten(ls).content == ls.foldRight(Set[T]())(f) ) because {
+ ls match {
+ case Nil() => true
+ case Cons(h, t) => {
+ flatten(h :: t).content ==| trivial |
+ (h ++ flatten(t)).content ==| appendContent(h, flatten(t)) |
+ h.content ++ flatten(t).content ==| flattenPreservesContent(t) |
+ h.content ++ t.foldRight(Set[T]())(f) ==| trivial |
+ f(h, Set[T]()) ++ t.foldRight(Set[T]())(f) ==| trivial |
+ (h :: t).foldRight(Set[T]())(f)
+ }.qed
+ }
+ }
+ }.holds
+
// A lemma about `append` and `updated`
def appendUpdate[T](l1: List[T], l2: List[T], i: BigInt, y: T): Boolean = {
require(0 <= i && i < l1.size + l2.size)