Skip to content

Instantly share code, notes, and snippets.

@FlorianCassayre
Last active September 21, 2019 12:11
Show Gist options
  • Save FlorianCassayre/cb36f76c8d713b79f2bb188c201775d6 to your computer and use it in GitHub Desktop.
Save FlorianCassayre/cb36f76c8d713b79f2bb188c201775d6 to your computer and use it in GitHub Desktop.
Proof that 1+2+...+n == n(n+1)/2 using Scala Stainless.
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
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment