Documentation.SBV.Examples.KnuckleDragger.Induction

Example use of the KnuckleDragger, for some inductive proofs

Documentation

sumConstProof :: IO Proof

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

We have:

>>> sumConstProof
Lemma: sumConst_correct                 Q.E.D.
[Proven] sumConst_correct

sumProof :: IO Proof

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

We have:

>>> sumProof
Lemma: sum_correct                      Q.E.D.
[Proven] sum_correct

sumSquareProof :: IO Proof

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

We have:

>>> sumSquareProof
Lemma: sumSquare_correct                Q.E.D.
[Proven] sumSquare_correct

elevenMinusFour :: IO Proof

Prove that 11^n - 4^n is always divisible by 7. Note that power operator is hard for SMT solvers to deal with due to non-linearity. For this example, we use cvc5 to discharge the final goal, where z3 can't converge on it.

We have:

>>> elevenMinusFour
Lemma: pow0                             Q.E.D.
Lemma: powN                             Q.E.D.
Lemma: elevenMinusFour                  Q.E.D.
[Proven] elevenMinusFour