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
badNonNegative :: IO ()

Documentation

>>> -- For doctest purposes only:
>>> :set -XScopedTypeVariables
>>> import Control.Exception

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

badNonNegative :: IO () Source #

A negative example: The regular inductive proof on integers (i.e., proving at 0, assuming at n and proving at n+1 will not allow you to conclude things when n < 0. The following example demonstrates this with the most obvious example:

>>> badNonNegative `catch` (\(_ :: SomeException) -> pure ())
Inductive lemma: badNonNegative
  Step: Base                            Q.E.D.
  Step: 1
*** Failed to prove badNonNegative.1.
Falsifiable. Counter-example:
  n = -2 :: Integer