sbv
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.KnuckleDragger.MergeSort

Description

Proving merge sort correct.

Synopsis

Merge sort

merge :: SList Integer -> SList Integer -> SList Integer Source #

Merge two already sorted lists into another

mergeSort :: SList Integer -> SList Integer Source #

Merge sort, using merge above to successively sort halved input

Helper functions

nonDecreasing :: SList Integer -> SBool Source #

A predicate testing whether a given list is non-decreasing.

count :: SInteger -> SList Integer -> SInteger Source #

Count the number of occurrences of an element in a list

isPermutation :: SList Integer -> SList Integer -> SBool Source #

Are two lists permutations of each other?

Correctness proof

correctness :: IO Proof Source #

Correctness of merge-sort.

We have:

>>> correctness
Lemma: nonDecrInsert                              Q.E.D.
Inductive lemma (strong): mergeKeepsSort
  Step: 1 (4 way full case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2                                     Q.E.D.
    Step: 1.3                                     Q.E.D.
    Step: 1.4.1                                   Q.E.D.
    Step: 1.4.2 (2 way case split)
      Step: 1.4.2.1.1                             Q.E.D.
      Step: 1.4.2.1.2                             Q.E.D.
      Step: 1.4.2.2.1                             Q.E.D.
      Step: 1.4.2.2.2                             Q.E.D.
      Step: 1.4.2.Completeness                    Q.E.D.
  Result:                                         Q.E.D.
Inductive lemma (strong): sortNonDecreasing
  Step: 1 (2 way full case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2.1                                   Q.E.D.
    Step: 1.2.2                                   Q.E.D.
    Step: 1.2.3                                   Q.E.D.
    Step: 1.2.4                                   Q.E.D.
  Result:                                         Q.E.D.
Inductive lemma (strong): mergeCount
  Step: 1 (4 way full case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2                                     Q.E.D.
    Step: 1.3                                     Q.E.D.
    Step: 1.4.1                                   Q.E.D.
    Step: 1.4.2                                   Q.E.D.
    Step: 1.4.3                                   Q.E.D.
    Step: 1.4.4                                   Q.E.D.
    Step: 1.4.5                                   Q.E.D.
    Step: 1.4.6                                   Q.E.D.
    Step: 1.4.7                                   Q.E.D.
  Result:                                         Q.E.D.
Inductive lemma: countAppend
  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: take_drop                                  Q.E.D.
Lemma: takeDropCount
  Step: 1                                         Q.E.D.
  Step: 2                                         Q.E.D.
  Result:                                         Q.E.D.
Inductive lemma (strong): sortIsPermutation
  Step: 1 (2 way full case split)
    Step: 1.1                                     Q.E.D.
    Step: 1.2.1                                   Q.E.D.
    Step: 1.2.2                                   Q.E.D.
    Step: 1.2.3                                   Q.E.D.
    Step: 1.2.4                                   Q.E.D.
    Step: 1.2.5                                   Q.E.D.
    Step: 1.2.6                                   Q.E.D.
  Result:                                         Q.E.D.
Lemma: mergeSortIsCorrect                         Q.E.D.
[Proven] mergeSortIsCorrect