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

Documentation.SBV.Examples.TP.QuickSort

Contents

Quick sort
Correctness proof

Description

Proving quick sort correct. The proof here closely follows the development given by Tobias Nipkow, in his paper "Term Rewriting and Beyond -- Theorem Proving in Isabelle," published in Formal Aspects of Computing 1: 320-338 back in 1989.

Synopsis

quickSort :: (Ord a, SymVal a) => SList a -> SList a
partition :: (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
correctness :: (Ord a, SymVal a) => IO (Proof (Forall "xs" [a] -> SBool))

Quick sort

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

Quick-sort, using the first element as pivot.

partition :: (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a] Source #

We define partition as an explicit function. Unfortunately, we can't just replace this with pivot xs -> Data.List.SBV.partition (.< pivot) xs because that would create a firstified version of partition with a free-variable captured, which isn't supported due to higher-order limitations in SMTLib.

Correctness proof

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

Correctness of quick-sort.

We have:

>>> correctness @Integer
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.
Inductive lemma: countNonNeg
  Step: Base                                                Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1.1                                             Q.E.D.
    Step: 1.1.2                                             Q.E.D.
    Step: 1.2.1                                             Q.E.D.
    Step: 1.2.2                                             Q.E.D.
    Step: 1.Completeness                                    Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: countElem
  Step: Base                                                Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1.1                                             Q.E.D.
    Step: 1.1.2                                             Q.E.D.
    Step: 1.2.1                                             Q.E.D.
    Step: 1.2.2                                             Q.E.D.
    Step: 1.Completeness                                    Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: elemCount
  Step: Base                                                Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                                               Q.E.D.
    Step: 1.2.1                                             Q.E.D.
    Step: 1.2.2                                             Q.E.D.
    Step: 1.Completeness                                    Q.E.D.
  Result:                                                   Q.E.D.
Lemma: sublistCorrect
  Step: 1                                                   Q.E.D.
  Result:                                                   Q.E.D.
Lemma: sublistElem
  Step: 1                                                   Q.E.D.
  Result:                                                   Q.E.D.
Lemma: sublistTail                                          Q.E.D.
Lemma: sublistIfPerm                                        Q.E.D.
Inductive lemma: lltCorrect
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: lgeCorrect
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: lltSublist
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Step: 2                                                   Q.E.D.
  Result:                                                   Q.E.D.
Lemma: lltPermutation
  Step: 1                                                   Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: lgeSublist
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Step: 2                                                   Q.E.D.
  Result:                                                   Q.E.D.
Lemma: lgePermutation
  Step: 1                                                   Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: partitionFstLT
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Step: 2 (push llt down)                                   Q.E.D.
  Step: 3                                                   Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: partitionSndGE
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Step: 2 (push lge down)                                   Q.E.D.
  Step: 3                                                   Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma (strong): partitionNotLongerFst
  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                                             Q.E.D.
    Step: 1.2.2 (simplify)                                  Q.E.D.
    Step: 1.2.3                                             Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma (strong): partitionNotLongerSnd
  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                                             Q.E.D.
    Step: 1.2.2 (simplify)                                  Q.E.D.
    Step: 1.2.3                                             Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: countPartition
  Step: Base                                                Q.E.D.
  Step: 1 (expand partition)                                Q.E.D.
  Step: 2 (push countTuple down)                            Q.E.D.
  Step: 3 (2 way case split)
    Step: 3.1.1                                             Q.E.D.
    Step: 3.1.2 (simplify)                                  Q.E.D.
    Step: 3.1.3                                             Q.E.D.
    Step: 3.2.1                                             Q.E.D.
    Step: 3.2.2 (simplify)                                  Q.E.D.
    Step: 3.2.3                                             Q.E.D.
    Step: 3.Completeness                                    Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma (strong): sortCountsMatch
  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                                             Q.E.D.
    Step: 1.2.2 (expand quickSort)                          Q.E.D.
    Step: 1.2.3 (push count down)                           Q.E.D.
    Step: 1.2.4                                             Q.E.D.
    Step: 1.2.5                                             Q.E.D.
    Step: 1.2.6 (IH on lo)                                  Q.E.D.
    Step: 1.2.7 (IH on hi)                                  Q.E.D.
    Step: 1.2.8                                             Q.E.D.
  Result:                                                   Q.E.D.
Lemma: sortIsPermutation                                    Q.E.D.
Inductive lemma: nonDecreasingMerge
  Step: Base                                                Q.E.D.
  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.
  Result:                                                   Q.E.D.
Inductive lemma (strong): sortIsNonDecreasing
  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                                             Q.E.D.
    Step: 1.2.2 (expand quickSort)                          Q.E.D.
    Step: 1.2.3 (push nonDecreasing down)                   Q.E.D.
    Step: 1.2.4                                             Q.E.D.
  Result:                                                   Q.E.D.
Lemma: quickSortIsCorrect                                   Q.E.D.
Inductive lemma: partitionSortedLeft
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Step: 2                                                   Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: partitionSortedRight
  Step: Base                                                Q.E.D.
  Step: 1                                                   Q.E.D.
  Step: 2                                                   Q.E.D.
  Result:                                                   Q.E.D.
Inductive lemma: unchangedIfNondecreasing
  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: ifChangedThenUnsorted                                Q.E.D.
== Proof tree:
quickSortIsCorrect
 ├╴sortIsPermutation
 │  └╴sortCountsMatch
 │     ├╴countAppend (x2)
 │     ├╴partitionNotLongerFst
 │     ├╴partitionNotLongerSnd
 │     └╴countPartition
 └╴sortIsNonDecreasing
    ├╴partitionNotLongerFst
    ├╴partitionNotLongerSnd
    ├╴partitionFstLT
    ├╴partitionSndGE
    ├╴sortIsPermutation (x2)
    ├╴lltPermutation
    │  ├╴lltSublist
    │  │  ├╴sublistElem
    │  │  │  └╴sublistCorrect
    │  │  │     ├╴countElem
    │  │  │     │  └╴countNonNeg
    │  │  │     └╴elemCount
    │  │  ├╴lltCorrect
    │  │  └╴sublistTail
    │  └╴sublistIfPerm
    ├╴lgePermutation
    │  ├╴lgeSublist
    │  │  ├╴sublistElem
    │  │  ├╴lgeCorrect
    │  │  └╴sublistTail
    │  └╴sublistIfPerm
    └╴nonDecreasingMerge
[Proven] quickSortIsCorrect :: Ɐxs ∷ [Integer] → Bool