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: Measure is non-negative                             Q.E.D.
  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 (unfold merge)                              Q.E.D.
    Step: 1.4.2 (2 way case split)
      Step: 1.4.2.1.1 (case split)                          Q.E.D.
      Step: 1.4.2.1.2                                       Q.E.D.
      Step: 1.4.2.2.1 (case split)                          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: Measure is non-negative                             Q.E.D.
  Step: 1 (2 way full case split)
    Step: 1.1                                               Q.E.D.
    Step: 1.2.1 (unfold)                                    Q.E.D.
    Step: 1.2.2 (push nonDecreasing down)                   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: Measure is non-negative                             Q.E.D.
  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 (unfold merge)                              Q.E.D.
    Step: 1.4.2 (push count inside)                         Q.E.D.
    Step: 1.4.3 (unfold count, twice)                       Q.E.D.
    Step: 1.4.4                                             Q.E.D.
    Step: 1.4.5                                             Q.E.D.
    Step: 1.4.6 (unfold count in reverse, twice)            Q.E.D.
    Step: 1.4.7 (simplify)                                  Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: countAppend
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Step: 2 (unfold count)                                    Q.E.D.
  Step: 3                                                   Q.E.D.
  Step: 4 (simplify)                                        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: Measure is non-negative                             Q.E.D.
  Step: 1 (2 way full case split)
    Step: 1.1                                               Q.E.D.
    Step: 1.2.1 (unfold mergeSort)                          Q.E.D.
    Step: 1.2.2 (push count down, simplify, rearrange)      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