| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.KnuckleDragger.QuickSort
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.
Quick sort
partition :: SInteger -> SList Integer -> STuple [Integer] [Integer] 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.
Helper functions
nonDecreasing :: SList Integer -> SBool Source #
A predicate testing whether a given list is non-decreasing.
count :: SInteger -> SList Integer -> SInteger Source #
Count the number of occurrences of an element in a list
isPermutation :: SList Integer -> SList Integer -> SBool Source #
Are two lists permutations of each other?
Correctness proof
correctness :: IO Proof Source #
Correctness of quick-sort.
We have:
>>>correctnessInductive 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: countNonNegative 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: permutationImpliesSublist 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: 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: 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. == Dependencies: quickSortIsCorrect ├╴sortIsPermutation │ └╴sortCountsMatch │ ├╴countAppend (x2) │ ├╴partitionNotLongerFst │ ├╴partitionNotLongerSnd │ └╴countPartition └╴sortIsNonDecreasing ├╴partitionNotLongerFst ├╴partitionNotLongerSnd ├╴partitionFstLT ├╴partitionSndGE ├╴sortIsPermutation (x2) ├╴lltPermutation │ ├╴lltSublist │ │ ├╴sublistElem │ │ │ └╴sublistCorrect │ │ │ ├╴countElem │ │ │ │ └╴countNonNegative │ │ │ └╴elemCount │ │ ├╴lltCorrect │ │ └╴sublistTail │ └╴permutationImpliesSublist ├╴lgePermutation │ ├╴lgeSublist │ │ ├╴sublistElem │ │ ├╴lgeCorrect │ │ └╴sublistTail │ └╴permutationImpliesSublist └╴nonDecreasingMerge [Proven] quickSortIsCorrect