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 :: (OrdSymbolic (SBV a), SymVal a) => SList a -> SList a
partition :: (OrdSymbolic (SBV a), SymVal a) => SBV a -> SList a -> STuple [a] [a]
partitionFstBound :: (OrdSymbolic (SBV a), SymVal a) => TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
partitionSndBound :: (OrdSymbolic (SBV a), SymVal a) => TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
correctness :: (Eq a, OrdSymbolic (SBV a), SymVal a) => IO (Proof (Forall "xs" [a] -> SBool))

Quick sort

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

Quick-sort, using the first element as pivot.

partition :: (OrdSymbolic (SBV 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.

partitionFstBound :: (OrdSymbolic (SBV a), SymVal a) => TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)) Source #

The first component of partition is no longer than the input.

>>> runTP $ partitionFstBound @Integer
Inductive lemma (strong): partitionNotLongerFst
  Step: Measure is non-negative                    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 (simplify)                         Q.E.D.
    Step: 1.2.3                                    Q.E.D.
    Step: 1.Completeness                           Q.E.D.
  Result:                                          Q.E.D.
Functions proven terminating: partition
[Proven] partitionNotLongerFst :: Ɐl ∷ [Integer] → Ɐpivot ∷ Integer → Bool

partitionSndBound :: (OrdSymbolic (SBV a), SymVal a) => TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)) Source #

The second component of partition is no longer than the input.

>>> runTP $ partitionSndBound @Integer
Inductive lemma (strong): partitionNotLongerSnd
  Step: Measure is non-negative                    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 (simplify)                         Q.E.D.
    Step: 1.2.3                                    Q.E.D.
    Step: 1.Completeness                           Q.E.D.
  Result:                                          Q.E.D.
Functions proven terminating: partition
[Proven] partitionNotLongerSnd :: Ɐl ∷ [Integer] → Ɐpivot ∷ Integer → Bool

Correctness proof

correctness :: (Eq a, OrdSymbolic (SBV 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 (unroll partition)                       Q.E.D.
  Step: 2 (push fst down, simplify)                Q.E.D.
  Step: 3 (push llt down)                          Q.E.D.
  Step: 4                                          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.
Lemma: partitionNotLongerFst                       Q.E.D.
Lemma: partitionNotLongerSnd                       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 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.
    Step: 1.Completeness                           Q.E.D.
  Result:                                          Q.E.D.
Lemma: sortIsPermutation                           Q.E.D.
Inductive lemma: nonDecreasingMerge
  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.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.
    Step: 1.2.7                                    Q.E.D.
    Step: 1.Completeness                           Q.E.D.
  Result:                                          Q.E.D.
Inductive lemma (strong): sortIsNonDecreasing
  Step: Measure is non-negative                    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 (expand quickSort)                 Q.E.D.
    Step: 1.2.3                                    Q.E.D.
    Step: 1.Completeness                           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
Functions proven terminating: count, lge, llt, nonDecreasing, partition, quickSort
[Proven] quickSortIsCorrect :: Ɐxs ∷ [Integer] → Bool