sbv-12.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.TP.RevAcc

Description

Proves that the accummulating version of reverse is equivalent to the standard definition.

Synopsis

Reversing with an accummulator.

revAcc :: SymVal a => SList a -> SList a -> SList a Source #

Accummulating reverse.

rev :: SymVal a => SList a -> SList a Source #

Given revAcc, we can reverse a list by providing the empty list as the initial accumulator.

Correctness proof

correctness :: SymVal a => IO (Proof (Forall "xs" [a] -> SBool)) Source #

Correctness the function rev. We have:

>>> correctness @Integer
Inductive lemma: revAccCorrect
  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.
  Result:                               Q.E.D.
Lemma: revCorrect                       Q.E.D.
[Proven] revCorrect :: Ɐxs ∷ [Integer] → Bool