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

Documentation.SBV.Examples.TP.Reverse

Contents

Reversing with no auxiliaries
Correctness proof

Description

Can we define the reverse function using no auxiliary functions, i.e., only in terms of cons, head, tail, and itself (recursively)? This example shows such a definition and proves that it is correct.

See Zohar Manna's 1974 "Mathematical Theory of Computation" book, where this definition and its proof is presented as Example 5.36.

Synopsis

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

Reversing with no auxiliaries

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

This definition of reverse uses no helper functions, other than the usual head, tail, cons, and uncons to reverse a given list. Note that efficiency is not our concern here, we call rev itself three times in the body.

Correctness proof

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

Correctness the function rev. We have:

>>> correctness @Integer
Inductive lemma: revLen
  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.
Inductive lemma: revApp
  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.
Inductive lemma: revApp
  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.
Lemma: revSnoc                          Q.E.D.
Inductive lemma: revApp
  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.
Inductive lemma: revRev
  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.
Inductive lemma (strong): revCorrect
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way full case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2 (2 way full case split)
      Step: 1.2.1                       Q.E.D.
      Step: 1.2.2.1                     Q.E.D.
      Step: 1.2.2.2                     Q.E.D.
      Step: 1.2.2.3                     Q.E.D.
      Step: 1.2.2.4                     Q.E.D.
      Step: 1.2.2.5 (simplify head)     Q.E.D.
      Step: 1.2.2.6                     Q.E.D.
      Step: 1.2.2.7 (simplify tail)     Q.E.D.
      Step: 1.2.2.8                     Q.E.D.
      Step: 1.2.2.9                     Q.E.D.
      Step: 1.2.2.10                    Q.E.D.
      Step: 1.2.2.11 (substitute)       Q.E.D.
      Step: 1.2.2.12                    Q.E.D.
      Step: 1.2.2.13                    Q.E.D.
      Step: 1.2.2.14                    Q.E.D.
  Result:                               Q.E.D.
[Proven] revCorrect :: Ɐxs ∷ [Integer] → Bool