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

Documentation.SBV.Examples.TP.InsertionSort

Contents

Insertion sort
Correctness proof

Description

Proving insertion sort correct.

Synopsis

insert :: (Ord a, SymVal a) => SBV a -> SList a -> SList a
insertionSort :: (Ord a, SymVal a) => SList a -> SList a
removeFirst :: (Eq a, SymVal a) => SBV a -> SList a -> SList a
isPermutation :: (Eq a, SymVal a) => SList a -> SList a -> SBool
correctness :: (Ord a, SymVal a) => IO (Proof (Forall "xs" [a] -> SBool))

Insertion sort

insert :: (Ord a, SymVal a) => SBV a -> SList a -> SList a Source #

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

insertionSort :: (Ord a, SymVal a) => SList a -> SList a Source #

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

removeFirst :: (Eq a, SymVal a) => SBV a -> SList a -> SList a Source #

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

isPermutation :: (Eq a, SymVal a) => SList a -> SList a -> SBool Source #

Are two lists permutations of each other? Note that we diverge from the counting based definition of permutation here, since this variant works better with insertion sort.

Correctness proof

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

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

We have:

>>> correctness @Integer
Lemma: nonDecrTail                           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.
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 :: Ɐxs ∷ [Integer] → Bool