Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.KnuckleDragger.Numeric

Description

Example use of inductive KnuckleDragger proofs, over integers.

Synopsis

sumConstProof :: IO Proof
sumProof :: IO Proof
sumSquareProof :: IO Proof
elevenMinusFour :: IO Proof

Documentation

sumConstProof :: IO Proof Source #

Prove that sum of constants c from 0 to n is n*c.

We have:

>>> sumConstProof
Inductive lemma: sumConst_correct
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Result:                               Q.E.D.
[Proven] sumConst_correct

sumProof :: IO Proof Source #

Prove that sum of numbers from 0 to n is n*(n-1)/2.

>>> sumProof
Inductive lemma: sum_correct
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
[Proven] sum_correct

sumSquareProof :: IO Proof Source #

Prove that sum of square of numbers from 0 to n is n*(n+1)*(2n+1)/6.

>>> sumSquareProof
Inductive lemma: sumSquare_correct
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
[Proven] sumSquare_correct

elevenMinusFour :: IO Proof Source #

Prove that 11^n - 4^n is always divisible by 7.

NB. As of Feb 2025, z3 struggles with the inductive step in this proof, but cvc5 performs just fine.

We have:

>>> elevenMinusFour
Lemma: powN                             Q.E.D.
Inductive lemma: elevenMinusFour
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: 7                               Q.E.D.
  Step: 8                               Q.E.D.
  Result:                               Q.E.D.
[Proven] elevenMinusFour