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

Documentation.SBV.Examples.TP.Fibonacci

Description

Proving that the naive version of fibonacci and the faster tail-recursive version are equivalent.

Synopsis

correctness :: IO (Proof (Forall "n" Integer -> SBool))

Documentation

correctness :: IO (Proof (Forall "n" Integer -> SBool)) Source #

Proving the tail recursive version of fibonacci is equivalent to the textbook version.

We have:

>>> correctness
Inductive lemma: helper
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2 (unfold fibonacci)            Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
Lemma: fibCorrect
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
[Proven] fibCorrect :: Ɐn ∷ Integer → Bool