sbv-11.4: 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.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.

We have:

>>> correctness
Lemma: nonDecTail                       Q.E.D.
Inductive lemma: insertNonDecreasing
  Base: insertNonDecreasing.Base        Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Asms: 4                               Q.E.D.
  Step: 4                               Q.E.D.
  Asms: 5                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: insertNonDecreasing.Step        Q.E.D.
Lemma: insertionSort1                   Q.E.D.
Inductive lemma: sortNonDecreasing
  Base: sortNonDecreasing.Base          Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: sortNonDecreasing.Step          Q.E.D.
Lemma: elemITE                          Q.E.D.
Inductive lemma: insertIsElem
  Base: insertIsElem.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: insertIsElem.Step               Q.E.D.
Inductive lemma: removeAfterInsert
  Base: removeAfterInsert.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.
  Step: 6                               Q.E.D.
  Step: removeAfterInsert.Step          Q.E.D.
Inductive lemma: sortIsPermutation
  Base: sortIsPermutation.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.
  Step: sortIsPermutation.Step          Q.E.D.
Lemma: insertionSortIsCorrect           Q.E.D.
[Proven] insertionSortIsCorrect