Adding more methods and lemmas to list library

ravimad · May 12, 2015 · 73289a8 · 73289a8
1 parent b0373d9
commit 73289a8
Showing 1 changed file with 70 additions and 1 deletion.
diff --git a/library/collection/List.scala b/library/collection/List.scala
@@ -31,7 +31,8 @@ sealed abstract class List[T] {
     case Cons(x, xs) => Cons(x, xs ++ that)
   }) ensuring { res =>
     (res.content == this.content ++ that.content) && 
-    (res.size == this.size + that.size)
+    (res.size == this.size + that.size) && 
+    (that != Nil[T]() || res == this)
   }
 
   def head: T = {
@@ -447,6 +448,28 @@ sealed abstract class List[T] {
     _ == this.filter(p).size
   }
 
+  def updated(i: BigInt, y: T): List[T] = {
+    require(0 <= i && i < this.size)
+    this match {
+      case Cons(x, tail) if i == 0 =>
+        Cons[T](y, tail)
+      case Cons(x, tail) =>
+        Cons[T](x, tail.updated(i - 1, y))
+    }
+  }
+
+  def insertAtIndex(i: BigInt, y: T): List[T] = {
+    require(0 <= i && i <= this.size)
+    this match {
+      case Nil() =>
+        Cons[T](y, Nil())
+      case _ if i == 0 =>
+        Cons[T](y, this)
+      case Cons(x, tail) =>
+        Cons[T](x, tail.insertAtIndex(i - 1, y))
+    }
+  }
+
 }
 
 @ignore
@@ -604,4 +627,50 @@ object ListSpecs {
     l.scanRight(z)(f).head == l.foldRight(z)(f)
   }.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)
+    // induction scheme
+    (l1 match {
+      case Nil() => true
+      case Cons(x, xs) => if (i == 0) true else appendUpdate[T](xs, l2, i - 1, y)
+    }) &&
+      // lemma
+      ((l1 ++ l2).updated(i, y) == (
+        if (i < l1.size)
+          l1.updated(i, y) ++ l2
+        else
+          l1 ++ l2.updated(i - l1.size, y)))
+  }.holds
+
+  // a lemma about `append`, `take` and `drop`
+  def appendTakeDrop[T](l1: List[T], l2: List[T], n: BigInt): Boolean = {
+    //induction scheme
+    (l1 match {
+      case Nil() => true
+      case Cons(x, xs) => if (n <= 0) true else appendTakeDrop[T](xs, l2, n - 1)
+    }) &&
+      // lemma
+      ((l1 ++ l2).take(n) == (
+        if (n < l1.size) l1.take(n)
+        else if (n > l1.size) l1 ++ l2.take(n - l1.size)
+        else l1)) &&
+        ((l1 ++ l2).drop(n) == (
+          if (n < l1.size) l1.drop(n) ++ l2
+          else if (n > l1.size) l2.drop(n - l1.size)
+          else l2))
+  }.holds
+
+  // A lemma about `append` and `insertAtIndex`
+  def appendInsert[T](l1: List[T], l2: List[T], i: BigInt, y: T): Boolean = {
+    require(0 <= i && i <= l1.size + l2.size)
+    (l1 match {
+      case Nil() => true
+      case Cons(x, xs) => if (i == 0) true else appendInsert[T](xs, l2, i - 1, y)
+    }) &&
+      // lemma
+      ((l1 ++ l2).insertAtIndex(i, y) == (
+        if (i < l1.size) l1.insertAtIndex(i, y) ++ l2
+        else l1 ++ l2.insertAtIndex((i - l1.size), y)))
+  }.holds
 }