From 51527856b2f6dc5ecf4e1ff548d7ffd6d90a4a1b Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Sun, 22 Sep 2024 20:16:59 -0700 Subject: [PATCH] playing around with insertion sort --- .../Examples/KnuckleDragger/InsertionSort.hs | 135 ++++++++++++++++++ sbv.cabal | 1 + 2 files changed, 136 insertions(+) create mode 100644 Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs diff --git a/Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs b/Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs new file mode 100644 index 000000000..0f7d791fb --- /dev/null +++ b/Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs @@ -0,0 +1,135 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.KnuckleDragger.InsertionSort +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Proving insertion-sort correct. +----------------------------------------------------------------------------- + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.KnuckleDragger.InsertionSort where + +import Data.SBV +import Data.SBV.Tools.KnuckleDragger + +import Prelude hiding (null, length, head, tail) +import Data.SBV.List + +-- | Insert an element into an already sorted list in the correct place. +insert :: SInteger -> SList Integer -> SList Integer +insert = smtFunction "insert" $ \e l -> ite (null l) (singleton e) + $ let (x, xs) = uncons l + in ite (e .<= x) (e .: x .: xs) (x .: insert e xs) + +-- | Insertion sort, using 'insert' above to successively insert the elements. +insertionSort :: SList Integer -> SList Integer +insertionSort = smtFunction "insertionSort" $ \l -> ite (null l) nil + $ let (x, xs) = uncons l + in insert x (insertionSort xs) + + +-- | A predicate testing whether a given list is non-decreasing. +nonDecreasing :: SList Integer -> SBool +nonDecreasing = smtFunction "nonDecreasing" $ \l -> null l .|| null (tail l) + .|| let (x, l') = uncons l + (y, _) = uncons l' + in x .<= y .&& nonDecreasing l' + +-- | The default settings for z3 have trouble running this proof out-of-the-box. +-- We have to pass auto_config=false to z3! +z3NoAutoConfig :: KDConfig +z3NoAutoConfig = z3KD{kdExtraSolverArgs = ["auto_config=false"]} + +-- | Correctness of insertion-sort. +-- +-- We have: +-- +-- >>> correctness +correctness :: IO Proof +correctness = runKDWith cvc5KD $ do + + -- helper: tail of nonDecreasing is nonDecreasing + tlNonDec <- lemma "tailNonDec" + (\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) -> nonDecreasing (x .: xs) .=> nonDecreasing xs) + [] + + -- helper: inserting into a non-decreasing list leaves it non-decreasing. Insertij + insertIntoNonDecreasing1 <- chainLemma "insertIntoNonDecreasing1" + (\(Forall @"e" e) (Forall @"x" x) (Forall @"xs" xs) -> e .<= x .=> nonDecreasing (x .: xs) .== nonDecreasing (insert e (x .: xs))) + (\e x xs -> [ e .<= x .=> nonDecreasing (insert e (x .: xs)) + , e .<= x .=> nonDecreasing (e .: x .: xs) + ]) + [] + + insertIntoNonDecreasing2 <- chainLemma "insertIntoNonDecreasing2" + (\(Forall @"e" e) (Forall @"x" x) (Forall @"xs" xs) -> e .> x .=> nonDecreasing (x .: xs) .== nonDecreasing (insert e (x .: xs))) + (\e x xs -> [ e .> x .=> nonDecreasing (insert e (x .: xs)) + , e .> x .=> nonDecreasing (x .: insert e xs) + , e .> x .=> nonDecreasing (insert e xs) + , e .> x .=> nonDecreasing xs + ]) + [induct (\e x -> nonDecreasing . insert e . (x .:)), tlNonDec, sorry] + + insertIntoNonDecreasing <- lemma "insertIntoNonDecreasing" + (\(Forall @"e" e) (Forall @"x" x) (Forall @"xs" xs) -> nonDecreasing (x .: xs) .== nonDecreasing (insert e (x .: xs))) + [insertIntoNonDecreasing1, insertIntoNonDecreasing2, sorry] + + nonDecreasingInsert <- lemma "nonDecreasingInsert" + (\(Forall @"e" e) (Forall @"xs" xs) -> nonDecreasing (insert e xs) .== nonDecreasing xs) + [induct nonDecreasing] + + chainLemma "insertionSortCorrect" + (\(Forall @"l" l) -> nonDecreasing (insertionSort l)) + (\x xs -> [ nonDecreasing (insertionSort (x .: xs)) + , nonDecreasing (insert x (insertionSort xs)) + , nonDecreasing (insertionSort xs) + ]) + [induct (nonDecreasing . insertionSort), nonDecreasingInsert, insertIntoNonDecreasing] +{- + -- helper: cons isn't null + consNotNull <- lemma "consNotNull" + (\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) -> sNot (null (x .: xs))) + [] + + -- helper: tail of nonDecreasing is nonDecreasing + tlNonDec <- lemma "tailNonDec" + (\(Forall @"x" (x :: SInteger)) (Forall @"xs" xs) -> nonDecreasing (x .: xs) .=> nonDecreasing xs) + [] + + -- helper: inserting into a non-decreasing list leaves it non-decreasing. Insertij + insertIntoNonDecreasing1 <- chainLemma "insertIntoNonDecreasing1" + (\(Forall @"e" e) (Forall @"x" x) (Forall @"xs" xs) -> e .<= x .=> nonDecreasing (x .: xs) .== nonDecreasing (insert e (x .: xs))) + (\e x xs -> [ e .<= x .=> nonDecreasing (insert e (x .: xs)) + , e .<= x .=> nonDecreasing (e .: x .: xs) + ]) + [] + + insertIntoNonDecreasing2 <- chainLemma "insertIntoNonDecreasing2" + (\(Forall @"e" e) (Forall @"x" x) (Forall @"xs" xs) -> e .> x .=> nonDecreasing (x .: xs) .== nonDecreasing (insert e (x .: xs))) + (\e x xs -> [ e .> x .=> nonDecreasing (insert e (x .: xs)) + , e .> x .=> nonDecreasing (x .: insert e xs) + , e .> x .=> nonDecreasing (insert e xs) + , e .> x .=> nonDecreasing xs + ]) + [induct (\e x -> nonDecreasing . insert e . (x .:)), tlNonDec] + + insertIntoNonDecreasing <- lemma "insertIntoNonDecreasing" + (\(Forall @"e" e) (Forall @"x" x) (Forall @"xs" xs) -> nonDecreasing (x .: xs) .== nonDecreasing (insert e (x .: xs))) + [insertIntoNonDecreasing1, insertIntoNonDecreasing2, sorry] + + chainLemma "insertionSortCorrect" + (\(Forall @"l" l) -> nonDecreasing (insertionSort l)) + (\x xs -> [ nonDecreasing (insertionSort (x .: xs)) + , nonDecreasing (insert x (insertionSort xs)) + , nonDecreasing (insertionSort xs) + ]) + [induct (nonDecreasing . insertionSort), consNotNull, insertIntoNonDecreasing] +-} diff --git a/sbv.cabal b/sbv.cabal index 8fd44d5f8..47531be16 100644 --- a/sbv.cabal +++ b/sbv.cabal @@ -159,6 +159,7 @@ Library , Documentation.SBV.Examples.KnuckleDragger.CaseSplit , Documentation.SBV.Examples.KnuckleDragger.Kleene , Documentation.SBV.Examples.KnuckleDragger.Induction + , Documentation.SBV.Examples.KnuckleDragger.InsertionSort , Documentation.SBV.Examples.KnuckleDragger.ListLen , Documentation.SBV.Examples.KnuckleDragger.RevLen , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational