Proof that 1+2+...+n == n(n+1)/2 using Scala Stainless.

SumFirstIntegers.scala

import stainless.annotation.induct

object SumFirstIntegers {

  // n(n+1)/2
  def sumFirstIntegersClosedForm(n: BigInt): BigInt = {
    require(n >= 0)

    n * (n + 1) / 2
  }

  // 1+2+...+n
  def sumFirstIntegersSeries(n: BigInt): BigInt = {
    require(n >= 0)

    if(n > 0) {
      sumFirstIntegersSeries(n - 1) + n
    } else {
      0
    }
  }

  // Proof by induction
  def lemmaEquality(@induct n: BigInt): Unit = {
    require(n >= 0)

  } ensuring(sumFirstIntegersClosedForm(n) == sumFirstIntegersSeries(n)) // <= The property

}