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

Documentation.SBV.Examples.KnuckleDragger.StrongInduction

Description

Examples of strong induction on integers.

Synopsis

oddSequence1 :: IO Proof
oddSequence2 :: IO Proof
won'tProve :: IO ()

Documentation

oddSequence1 :: IO Proof Source #

Prove that the sequence 1, 3, S_{k-2} + 2 S_{k-1} is always odd.

We have:

>>> oddSequence1
Inductive lemma (strong): oddSequence
  Base: oddSequence.Base                Q.E.D.
  Asms: 1                               Q.E.D.
  Step 1: Case split one way:
    Case [1 of 1]: n[1]                 Q.E.D.
    Completeness:                       Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: oddSequence.Step                Q.E.D.
[Proven] oddSequence

oddSequence2 :: IO Proof Source #

Prove that the sequence 1, 3, 2 S_{k-1} - S_{k-2} generates sequence of odd numbers.

We have:

>>> oddSequence2
Inductive lemma (strong): oddSequence
  Base: oddSequence.Base                Q.E.D.
  Asms: 1                               Q.E.D.
  Step 1: Case split one way:
    Case [1 of 1]: n[1]                 Q.E.D.
    Completeness:                       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: oddSequence.Step                Q.E.D.
[Proven] oddSequence

won'tProve :: IO () Source #

For strong induction to work, We have to instantiate the proof at a "smaller" value. This example demonstrates what happens if we don't. We have:

>>> won'tProve `catch` (\(_ :: SomeException) -> pure ())
Inductive lemma (strong): lengthGood
  Base: lengthGood.Base                 Q.E.D.
  Step: 1
*** Failed to prove lengthGood.1.

*** Solver reported: canceled