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

Documentation.SBV.Examples.KnuckleDragger.InsertionSort

Description

Proving insertion sort correct.

Synopsis

Insertion sort

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

Insert an element into an already sorted list in the correct place.

insertionSort :: SList Integer -> SList Integer Source #

Insertion sort, using insert above to successively insert the elements.

Helper functions

nonDecreasing :: SList Integer -> SBool Source #

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

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

Remove the first occurrence of an number from a list, if any.

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

Are two lists permutations of each other?

Correctness proof

correctness :: IO Proof Source #

Correctness of insertion-sort. z3 struggles with this, but CVC5 proves it just fine.

We have:

>>> correctness
Lemma: nonDecTail                            Q.E.D.
Inductive lemma: insertNonDecreasing
  Step: Base                                 Q.E.D.
  Step: 1 (unfold insert)                    Q.E.D.
  Step: 2 (push nonDecreasing down)          Q.E.D.
  Step: 3 (unfold simplify)                  Q.E.D.
  Step: 4                                    Q.E.D.
  Step: 5                                    Q.E.D.
  Result:                                    Q.E.D.
Inductive lemma: sortNonDecreasing
  Step: Base                                 Q.E.D.
  Step: 1 (unfold insertionSort)             Q.E.D.
  Step: 2                                    Q.E.D.
  Result:                                    Q.E.D.
Lemma: elemITE                               Q.E.D.
Inductive lemma: insertIsElem
  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: removeAfterInsert
  Step: Base                                 Q.E.D.
  Step: 1 (expand insert)                    Q.E.D.
  Step: 2 (push removeFirst down ite)        Q.E.D.
  Step: 3 (unfold removeFirst on 'then')     Q.E.D.
  Step: 4 (unfold removeFirst on 'else')     Q.E.D.
  Step: 5                                    Q.E.D.
  Step: 6 (simplify)                         Q.E.D.
  Result:                                    Q.E.D.
Inductive lemma: sortIsPermutation
  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: insertionSortIsCorrect                Q.E.D.
[Proven] insertionSortIsCorrect