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
  Base: sumConst_correct.Base           Q.E.D.
  Asms: 1                               Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: sumConst_correct.Step           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
  Base: sum_correct.Base                Q.E.D.
  Asms: 1                               Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: sum_correct.Step                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
  Base: sumSquare_correct.Base          Q.E.D.
  Asms: 1                               Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: sumSquare_correct.Step          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
  Base: elevenMinusFour.Base            Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Asms: 6                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: 7                               Q.E.D.
  Step: 8                               Q.E.D.
  Step: elevenMinusFour.Step            Q.E.D.
[Proven] elevenMinusFour