test.leon.scala

import leon.lang._
import leon.collection._
import leon._
import ListSpecs._

object Test {
  // 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
  
  /*
  // Sieving integral numbers
  def sieve(s: Stream[Int]): Stream[Int] = {
    s.head #:: sieve(s.tail.filter(_ % s.head != 0))
  }

  // All primes as a lazy sequence
  val primes = sieve(Stream.from(2))
  */
  
  def gen(from: BigInt, to: BigInt): List[BigInt] = {
    def recGen(from: BigInt, to: BigInt, acc: List[BigInt]): List[BigInt] = {
      if (from > to) acc
      else recGen(from+1, to, acc :+ from)
    }
    
    recGen(from, to, Nil[BigInt])
  }.ensuring{ res => 
    if (from == to) res == List(from)
    else if (from < to) 
      res.size == (to - from + 1) && 
      res == from :: gen(from + 1, to)
    else res.isEmpty
  }
  
  def gen2(from: BigInt, to: BigInt): List[BigInt] = {
    if (from <= to) from :: gen(from + 1, to)
    else List()
  }.ensuring{ res => 
    if (from == to) res == List(from)
    else if (from < to) 
      res.size == (to - from + 1) && 
      res == from :: gen(from + 1, to)
    else res.isEmpty
  }
  
  def isPrime(x: BigInt): Boolean = {
    require(x >= 2)
    
    if (x == 2) true
    else if (x % 2 == 0) false
    else {
      def recIsPrime(z: BigInt): Boolean = {
        if (z * z > x) true
        else if (x % z == 0) false
        else recIsPrime(z+2)
      }
      recIsPrime(3)
    }
  }
  
  def isPrime2(x: BigInt): Boolean = {
    require(x >= 2)
    
    if (x == 2) true
    else if (x % 2 == 0) false
    else {
      def recIsPrime2(z: BigInt): Boolean = {
        if (z * z > x) true
        else if (x % z == 0) false
        else recIsPrime2(z+2)
      }
      recIsPrime2(3)
    }
  }.ensuring{ res => 
    if (x == 2) res
    else if (x % 2 == 0) !res
    else if (res) {
      // exists y < x s.t. y | x
      true
    } else {
      // forall y < x s.t. not(y | x)
      true
    }
  }
  
  def pow(x: BigInt, exp: BigInt): BigInt = {
    require(exp >= 0)
    
    if (exp == 0) 1
    else x * pow(x, exp - 1)
  }
  
  def lemmaPow(a: BigInt, i: BigInt, j: BigInt): Boolean = {
    require(i >= 0 && j >= 0)
    
    pow(a, i+j) == pow(a, i) * pow(a, j) && {
      if (j == 0) true
      else lemmaPow(a, i, j-1) 
    }
  }.holds
  
  def lemmaFermat1(a: BigInt, p: BigInt): Boolean = {
    require(a >= 0 && p >= 2 && isPrime(p))
    
    //a.modPow(p, p) == a // modPow doesn't exist...
    
    pow(a, p) % p == a % p
  }.holds
  
  def lemmaFermat2(a: BigInt, p: BigInt): Boolean = {
    require(a >= 0 && p >= 2 && isPrime(p) && a % p != 0)
    
    //a.modPow(p, p) == a // modPow doesn't exist...
    
    pow(a, p - 1) % p == 1
  }.holds
  
  def lemmaFermat3(a: BigInt, p: BigInt): Boolean = {
    require(a >= 0 && p >= 2 && isPrime(p) && a % p != 0 && 0 <= a && a < p)
    
    //a.modPow(p, p) == a // modPow doesn't exist...
    
    pow(a, p - 1) % p == 1
  }.holds
  
  // Make sure the impl of isPrime is correct
  def lemma0(): Boolean = {
    List[BigInt](4, 6, 8, 9, 10, 12, 15, 21, 25, 27).forall{!isPrime(_)}
  }.holds
  
  def lemma1(): Boolean = {
    List[BigInt](2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59).forall{isPrime}
  }.holds
  
  def lemma2(): Boolean = {
    List[BigInt](61, 67, 71, 73, 79, 83, 89, 97, 101, 103, 107, 109, 113, 127, 131, 137, 139).forall{isPrime}
  }.holds
  
  def lemma3(): Boolean = {
    List[BigInt](149, 151, 157, 163, 167, 173, 179, 181, 191, 193, 197, 199, 211, 223, 227).forall{isPrime}
  }.holds
  
  def lemma4(): Boolean = {
    List[BigInt](229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283, 293, 307).forall{isPrime}
  }.holds
  
  def lemma5(): Boolean = {
    List[BigInt](311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389).forall{isPrime}
  }.holds
  
  def lemma6(): Boolean = {
    List[BigInt](397, 401, 409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463).forall{isPrime}
  }.holds
  
  def lemma7(): Boolean = {
    List[BigInt](467, 479, 487, 491, 499, 503, 509, 521, 523, 541).forall{isPrime}
  }.holds
}