-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.QuickSort
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.QuickSort where

import Prelude hiding (null, length, (++), tail, all, fst, snd, elem)
import Control.Monad.Trans (liftIO)

import Data.SBV
import Data.SBV.List hiding (partition)
import Data.SBV.Tuple
import Data.SBV.Tools.KnuckleDragger

-- * Quick sort

-- | Quick-sort, using the first element as pivot.
quickSort :: SList Integer -> SList Integer
quickSort :: SList Integer -> SList Integer
quickSort = String
-> (SList Integer -> SList Integer)
-> SList Integer
-> SList Integer
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"quickSort" ((SList Integer -> SList Integer)
 -> SList Integer -> SList Integer)
-> (SList Integer -> SList Integer)
-> SList Integer
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SList Integer
l -> SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l)
                                                SList Integer
forall a. SymVal a => SList a
nil
                                                (let (SInteger
x,  SList Integer
xs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l
                                                     (SList Integer
lo, SList Integer
hi) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
x SList Integer
xs)
                                                 in  SList Integer -> SList Integer
quickSort SList Integer
lo SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
x SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer -> SList Integer
quickSort SList Integer
hi)

-- | 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.
partition :: SInteger -> SList Integer -> STuple [Integer] [Integer]
partition :: SInteger -> SList Integer -> STuple [Integer] [Integer]
partition = String
-> (SInteger -> SList Integer -> STuple [Integer] [Integer])
-> SInteger
-> SList Integer
-> STuple [Integer] [Integer]
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"partition" ((SInteger -> SList Integer -> STuple [Integer] [Integer])
 -> SInteger -> SList Integer -> STuple [Integer] [Integer])
-> (SInteger -> SList Integer -> STuple [Integer] [Integer])
-> SInteger
-> SList Integer
-> STuple [Integer] [Integer]
forall a b. (a -> b) -> a -> b
$ \SInteger
pivot SList Integer
xs -> SBool
-> STuple [Integer] [Integer]
-> STuple [Integer] [Integer]
-> STuple [Integer] [Integer]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs)
                                                       ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer
forall a. SymVal a => SList a
nil, SList Integer
forall a. SymVal a => SList a
nil))
                                                       (let (SInteger
a,  SList Integer
as) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
xs
                                                            (SList Integer
lo, SList Integer
hi) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)
                                                        in SBool
-> STuple [Integer] [Integer]
-> STuple [Integer] [Integer]
-> STuple [Integer] [Integer]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                                               ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
lo, SList Integer
hi))
                                                               ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer
lo, SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
hi)))

-- * Helper functions

-- | A predicate testing whether a given list is non-decreasing.
nonDecreasing :: SList Integer -> SBool
nonDecreasing :: SList Integer -> SBool
nonDecreasing = String -> (SList Integer -> SBool) -> SList Integer -> SBool
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"nonDecreasing" ((SList Integer -> SBool) -> SList Integer -> SBool)
-> (SList Integer -> SBool) -> SList Integer -> SBool
forall a b. (a -> b) -> a -> b
$ \SList Integer
l ->  SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l SBool -> SBool -> SBool
.|| SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null (SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a
tail SList Integer
l)
                                                 SBool -> SBool -> SBool
.|| let (SInteger
x, SList Integer
l') = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l
                                                         (SInteger
y, SList Integer
_)  = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l'
                                                     in SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y SBool -> SBool -> SBool
.&& SList Integer -> SBool
nonDecreasing SList Integer
l'

-- | Count the number of occurrences of an element in a list
count :: SInteger -> SList Integer -> SInteger
count :: SInteger -> SList Integer -> SInteger
count = String
-> (SInteger -> SList Integer -> SInteger)
-> SInteger
-> SList Integer
-> SInteger
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"count" ((SInteger -> SList Integer -> SInteger)
 -> SInteger -> SList Integer -> SInteger)
-> (SInteger -> SList Integer -> SInteger)
-> SInteger
-> SList Integer
-> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
e SList Integer
l -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l)
                                          SInteger
0
                                          (let (SInteger
x, SList Integer
xs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l
                                               cxs :: SInteger
cxs     = SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs
                                           in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x) (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
cxs) SInteger
cxs)

-- | Are two lists permutations of each other?
isPermutation :: SList Integer -> SList Integer -> SBool
isPermutation :: SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs SList Integer
ys = (Forall "x" Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall @"x" SInteger
x) -> SInteger -> SList Integer -> SInteger
count SInteger
x SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList Integer -> SInteger
count SInteger
x SList Integer
ys)

-- * Correctness proof

-- | Correctness of quick-sort.
--
-- We have:
--
-- >>> correctness
-- 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: 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
correctness :: IO Proof
correctness :: IO Proof
correctness = SMTConfig -> KD Proof -> IO Proof
forall a. SMTConfig -> KD a -> IO a
runKDWith SMTConfig
z3{kdOptions = (kdOptions z3) {ribbonLength = 60}} (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do

  ---------------------------------------------------------------------------------------------------
  -- Part I. Formalizing less-than/greater-than-or-equal over lists and relationship to permutations
  ---------------------------------------------------------------------------------------------------
  -- llt: list less-than:     all the elements are <  pivot
  -- lge: list greater-equal: all the elements are >= pivot
  let llt, lge :: SInteger -> SList Integer -> SBool
      llt :: SInteger -> SList Integer -> SBool
llt = String
-> (SInteger -> SList Integer -> SBool)
-> SInteger
-> SList Integer
-> SBool
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"llt" ((SInteger -> SList Integer -> SBool)
 -> SInteger -> SList Integer -> SBool)
-> (SInteger -> SList Integer -> SBool)
-> SInteger
-> SList Integer
-> SBool
forall a b. (a -> b) -> a -> b
$ \SInteger
pivot SList Integer
l -> SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l SBool -> SBool -> SBool
.|| let (SInteger
x, SList Integer
xs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l in SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<  SInteger
pivot SBool -> SBool -> SBool
.&& SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
xs
      lge :: SInteger -> SList Integer -> SBool
lge = String
-> (SInteger -> SList Integer -> SBool)
-> SInteger
-> SList Integer
-> SBool
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"lge" ((SInteger -> SList Integer -> SBool)
 -> SInteger -> SList Integer -> SBool)
-> (SInteger -> SList Integer -> SBool)
-> SInteger
-> SList Integer
-> SBool
forall a b. (a -> b) -> a -> b
$ \SInteger
pivot SList Integer
l -> SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l SBool -> SBool -> SBool
.|| let (SInteger
x, SList Integer
xs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l in SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
pivot SBool -> SBool -> SBool
.&& SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
xs

      -- Sublist relationship
      sublist :: SList Integer -> SList Integer -> SBool
      sublist :: SList Integer -> SList Integer -> SBool
sublist SList Integer
xs SList Integer
ys = (Forall "e" Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
ys SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0)

  -- llt correctness
  lltCorrect <-
     String
-> (Forall "xs" [Integer]
    -> Forall "e" Integer -> Forall "pivot" Integer -> SBool)
-> (Proof
    -> SInteger
    -> SList Integer
    -> SInteger
    -> SInteger
    -> (SBool, KDProofRaw SBool))
-> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
String -> a -> (Proof -> steps) -> KD Proof
induct String
"lltCorrect"
            (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) (Forall @"pivot" SInteger
pivot) -> SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
xs SBool -> SBool -> SBool
.&& SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs SBool -> SBool -> SBool
.=> SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot) ((Proof
  -> SInteger
  -> SList Integer
  -> SInteger
  -> SInteger
  -> (SBool, KDProofRaw SBool))
 -> KD Proof)
-> (Proof
    -> SInteger
    -> SList Integer
    -> SInteger
    -> SInteger
    -> (SBool, KDProofRaw SBool))
-> KD Proof
forall a b. (a -> b) -> a -> b
$
            \Proof
ih SInteger
x SList Integer
xs SInteger
e SInteger
pivot -> [SInteger -> SList Integer -> SBool
llt SInteger
pivot (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs), SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)]
                             [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot
                             SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                             KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- lge correctness
  lgeCorrect <-
     induct "lgeCorrect"
            (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) (Forall @"pivot" SInteger
pivot) -> SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
xs SBool -> SBool -> SBool
.&& SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs SBool -> SBool -> SBool
.=> SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
pivot) $
            \Proof
ih SInteger
x SList Integer
xs SInteger
e SInteger
pivot -> [SInteger -> SList Integer -> SBool
lge SInteger
pivot (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs), SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)]
                             [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
pivot
                             SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                             KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- count is always non-negative
  countNonNegative <- induct "countNonNegative"
                             (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0) $
                             \Proof
ih SInteger
x SList Integer
xs SInteger
e -> [] [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                                                  SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                                                                  KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                                       , SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
x SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
                                                                  SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                                                                  KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                                  SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                                       ]

  -- relationship between count and elem, forward direction
  countElem <- induct "countElem"
                      (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) -> SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs SBool -> SBool -> SBool
.=> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0) $
                      \Proof
ih SInteger
x SList Integer
xs SInteger
e -> [SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)]
                                 [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0
                                                     SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
countNonNegative
                                                     KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                          , SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
x SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0
                                                     SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                                                     KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                          ]

  -- relationship between count and elem, backwards direction
  elemCount <- induct "elemCount"
                      (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs) $
                      \Proof
ih SInteger
x SList Integer
xs SInteger
e -> [SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0]
                                 [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> KDProofRaw SBool
forall a. Trivial a => a
trivial
                                          , SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
x SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs
                                                     SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                                                     KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                          ]

  -- sublist correctness
  sublistCorrect <- calc "sublistCorrect"
                          (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) (Forall @"x" SInteger
x) -> SList Integer
xs SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
ys) $
                          \SList Integer
xs SList Integer
ys SInteger
x -> [SList Integer
xs SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys, SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
xs]
                                   [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
ys
                                   SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
countElem Proof -> (Inst "xs" [Integer], Inst "e" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
x)
                                      , Proof
elemCount Proof -> (Inst "xs" [Integer], Inst "e" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
x)
                                      ]
                                   KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- If one list is a sublist of another, then its head is an elem
  sublistElem <- calc "sublistElem"
                       (\(Forall @"x" SInteger
x) (Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) -> (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys SBool -> SBool -> SBool
.=> SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
ys) $
                       \SInteger
x SList Integer
xs SList Integer
ys -> [(SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys]
                                [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
ys
                                SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
sublistCorrect Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer], Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- If one list is a sublist of another so is its tail
  sublistTail <- lemma "sublistTail"
                       (\(Forall @"x" SInteger
x) (Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) -> (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys SBool -> SBool -> SBool
.=> SList Integer
xs SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys)
                       []

  -- Permutation implies sublist
  permutationImpliesSublist <- lemma "permutationImpliesSublist"
                                    (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) -> SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs SList Integer
ys SBool -> SBool -> SBool
.=> SList Integer
xs SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys)
                                    []

  -- If a value is less than all the elements in a list, then it is also less than all the elements of any sublist of it
  lltSublist <-
     inductWith cvc5 "lltSublist"
            (\(Forall @"xs" SList Integer
xs) (Forall @"pivot" SInteger
pivot) (Forall @"ys" SList Integer
ys) -> SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
ys SBool -> SBool -> SBool
.&& SList Integer
xs SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys SBool -> SBool -> SBool
.=> SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
xs) $
            \Proof
ih SInteger
x SList Integer
xs SInteger
pivot SList Integer
ys -> [SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
ys, (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys]
                              [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SBool
llt SInteger
pivot (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot SBool -> SBool -> SBool
.&& SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
xs
                              SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ -- To establish x .< pivot, observe that x is in ys, and together
                                   -- with llt pivot ys, we get that x is less than pivot
                                   Proof
sublistElem Proof
-> (Inst "x" Integer, Inst "xs" [Integer], Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x,   forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                                 , Proof
lltCorrect Proof
-> (Inst "xs" [Integer], Inst "e" Integer, Inst "pivot" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e"  SInteger
x,  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
pivot)

                                   -- Use induction hypothesis to get rid of the second conjunct. We need to tell
                                   -- the prover that xs is a sublist of ys too so it can satisfy its precondition
                                 , Proof
sublistTail Proof
-> (Inst "x" Integer, Inst "xs" [Integer], Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                                 , Proof
ih         Proof -> (Inst "pivot" Integer, Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
pivot, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                                 ]
                              KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- Variant of the above for the permutation case
  lltPermutation <-
     calc "lltPermutation"
           (\(Forall @"xs" SList Integer
xs) (Forall @"pivot" SInteger
pivot) (Forall @"ys" SList Integer
ys) -> SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
ys SBool -> SBool -> SBool
.&& SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs SList Integer
ys SBool -> SBool -> SBool
.=> SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
xs) $
           \SList Integer
xs SInteger
pivot SList Integer
ys -> [SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
ys, SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs SList Integer
ys]
                        [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
xs
                        SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
lltSublist                Proof
-> (Inst "xs" [Integer], Inst "pivot" Integer, Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
pivot, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                           , Proof
permutationImpliesSublist Proof -> (Inst "xs" [Integer], Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                           ]
                        KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                        SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- If a value is greater than or equal to all the elements in a list, then it is also less than all the elements of any sublist of it
  lgeSublist <-
     inductWith cvc5 "lgeSublist"
            (\(Forall @"xs" SList Integer
xs) (Forall @"pivot" SInteger
pivot) (Forall @"ys" SList Integer
ys) -> SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
ys SBool -> SBool -> SBool
.&& SList Integer
xs SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys SBool -> SBool -> SBool
.=> SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
xs) $
            \Proof
ih SInteger
x SList Integer
xs SInteger
pivot SList Integer
ys -> [SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
ys, (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer -> SList Integer -> SBool
`sublist` SList Integer
ys]
                              [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SBool
lge SInteger
pivot (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
pivot SBool -> SBool -> SBool
.&& SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
xs
                              SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ -- To establish x .>= pivot, observe that x is in ys, and together
                                   -- with lge pivot ys, we get that x is greater than equal to the pivot
                                   Proof
sublistElem Proof
-> (Inst "x" Integer, Inst "xs" [Integer], Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x,   forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                                 , Proof
lgeCorrect  Proof
-> (Inst "xs" [Integer], Inst "e" Integer, Inst "pivot" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e"  SInteger
x,  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
pivot)

                                   -- Use induction hypothesis to get rid of the second conjunct. We need to tell
                                   -- the prover that xs is a sublist of ys too so it can satisfy its precondition
                                 , Proof
sublistTail Proof
-> (Inst "x" Integer, Inst "xs" [Integer], Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                                 , Proof
ih          Proof -> (Inst "pivot" Integer, Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
pivot, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                                 ]
                              KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- Variant of the above for the permutation case
  lgePermutation <-
     calc "lgePermutation"
           (\(Forall @"xs" SList Integer
xs) (Forall @"pivot" SInteger
pivot) (Forall @"ys" SList Integer
ys) -> SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
ys SBool -> SBool -> SBool
.&& SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs SList Integer
ys SBool -> SBool -> SBool
.=> SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
xs) $
           \SList Integer
xs SInteger
pivot SList Integer
ys -> [SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
ys, SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs SList Integer
ys]
                        [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
xs
                        SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
lgeSublist                Proof
-> (Inst "xs" [Integer], Inst "pivot" Integer, Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
pivot, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                           , Proof
permutationImpliesSublist Proof -> (Inst "xs" [Integer], Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys)
                           ]
                        KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                        SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  --------------------------------------------------------------------------------------------
  -- Part II. Helper lemmas for partition
  --------------------------------------------------------------------------------------------

  -- The first element of the partition produces all smaller elements
  partitionFstLT <- inductWith cvc5 "partitionFstLT"
     (\(Forall @"l" SList Integer
l) (Forall @"pivot" SInteger
pivot) -> SInteger -> SList Integer -> SBool
llt SInteger
pivot (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
l))) $
     \Proof
ih SInteger
a SList Integer
as SInteger
pivot -> [] [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SBool
llt SInteger
pivot (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as)))
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SBool
llt SInteger
pivot (SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                            (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as))
                                            (     STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)))
                          SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push llt down"
                          KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                 (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot SBool -> SBool -> SBool
.&& SInteger -> SList Integer -> SBool
llt SInteger
pivot (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)))
                                 (               SInteger -> SList Integer -> SBool
llt SInteger
pivot (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)))
                          SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                          KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- The second element of the partition produces all greater-than-or-equal to elements
  partitionSndGE <- inductWith cvc5 "partitionSndGE"
     (\(Forall @"l" SList Integer
l) (Forall @"pivot" SInteger
pivot) -> SInteger -> SList Integer -> SBool
lge SInteger
pivot (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
l))) $
     \Proof
ih SInteger
a SList Integer
as SInteger
pivot -> [] [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SBool
lge SInteger
pivot (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as)))
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SBool
lge SInteger
pivot (SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                            (     STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as))
                                            (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)))
                          SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push lge down"
                          KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                 (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot SBool -> SBool -> SBool
.&& SInteger -> SList Integer -> SBool
lge SInteger
pivot (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)))
                                 (               SInteger -> SList Integer -> SBool
lge SInteger
pivot (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)))
                          SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                          KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

  -- The first element of partition does not increase in size
  partitionNotLongerFst <- sInduct "partitionNotLongerFst"
     (\(Forall @"l" SList Integer
l) (Forall @"pivot" SInteger
pivot) -> SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
l)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
l)
     (\SList Integer
l (SInteger
_ :: SInteger) -> forall a. SymVal a => SList a -> SInteger
length @Integer SList Integer
l) $
     \Proof
ih SList Integer
l SInteger
pivot -> [] [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
l)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
l
                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> KDProofRaw SBool
-> (SInteger -> SList Integer -> KDProofRaw SBool)
-> KDProofRaw SBool
forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList Integer
l KDProofRaw SBool
forall a. Trivial a => a
trivial
                                (\SInteger
a SList Integer
as -> let lo :: SList Integer
lo = STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)
                                       in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                              (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
lo) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as))
                                              (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length       SList Integer
lo  SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as))
                                       SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                       KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                              (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<=     SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
as)
                                              (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
as)
                                       SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof -> (Inst "l" [Integer], Inst "pivot" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
pivot)
                                       KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed)

  -- The second element of partition does not increase in size
  partitionNotLongerSnd <- sInduct "partitionNotLongerSnd"
     (\(Forall @"l" SList Integer
l) (Forall @"pivot" SInteger
pivot) -> SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
l)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
l)
     (\SList Integer
l (SInteger
_ :: SInteger) -> forall a. SymVal a => SList a -> SInteger
length @Integer SList Integer
l) $
     \Proof
ih SList Integer
l SInteger
pivot -> [] [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
l)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
l
                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> KDProofRaw SBool
-> (SInteger -> SList Integer -> KDProofRaw SBool)
-> KDProofRaw SBool
forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList Integer
l KDProofRaw SBool
forall a. Trivial a => a
trivial
                                (\SInteger
a SList Integer
as -> let hi :: SList Integer
hi = STuple [Integer] [Integer] -> SList Integer
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)
                                       in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                              (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length       SList Integer
hi  SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as))
                                              (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
hi) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as))
                                       SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                       KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                              (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
hi SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
as)
                                              (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
hi SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<=     SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
as)
                                       SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof -> (Inst "l" [Integer], Inst "pivot" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
pivot)
                                       KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed)

  --------------------------------------------------------------------------------------------
  -- Part III. Helper lemmas for count
  --------------------------------------------------------------------------------------------

  -- Count distributes over append
  countAppend <-
      induct "countAppend"
             (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) (Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
ys) $
             \Proof
ih SInteger
x SList Integer
xs SList Integer
ys SInteger
e -> [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SInteger
count SInteger
e ((SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: (SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys))
                                 SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold count"
                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (let r :: SInteger
r = SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                 SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof -> (Inst "ys" [Integer], Inst "e" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (let r :: SInteger
r = SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
ys in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                 SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
ys
                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed

  -- Count is preserved over partition
  let countTuple :: SInteger -> STuple [Integer] [Integer] -> SInteger
      countTuple SInteger
e STuple [Integer] [Integer]
xsys = SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
ys
        where (SList Integer
xs, SList Integer
ys) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple STuple [Integer] [Integer]
xsys

  countPartition <-
     induct "countPartition"
            (\(Forall @"xs" SList Integer
xs) (Forall @"pivot" SInteger
pivot) (Forall @"e" SInteger
e) -> SInteger -> STuple [Integer] [Integer] -> SInteger
countTuple SInteger
e (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs) $
            \Proof
ih SInteger
a SList Integer
as SInteger
pivot SInteger
e ->
                [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> STuple [Integer] [Integer] -> SInteger
countTuple SInteger
e (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as))
                   SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"expand partition"
                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> STuple [Integer] [Integer] -> SInteger
countTuple SInteger
e (let (SList Integer
lo, SList Integer
hi) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)
                                    in SBool
-> STuple [Integer] [Integer]
-> STuple [Integer] [Integer]
-> STuple [Integer] [Integer]
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                           ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
lo, SList Integer
hi))
                                           ((SList Integer, SList Integer) -> STuple [Integer] [Integer]
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList Integer
lo, SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
hi)))
                   SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push countTuple down"
                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList Integer
lo, SList Integer
hi) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
pivot SList Integer
as)
                   in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                          (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
lo) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
hi)
                          (SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
hi))
                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SInteger)] -> KDProofRaw SInteger
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
a  SBool -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                              (SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
hi)
                                              (SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
hi)
                                       SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                       KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
hi
                                       SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                                       KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
as
                                       SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed
                            , SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
a SBool -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
pivot)
                                              (SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
hi)
                                              (SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
hi)
                                       SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                       KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
hi
                                       SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                                       KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
as
                                       SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed
                            ]
  --------------------------------------------------------------------------------------------
  -- Part IV. Prove that the output of quick sort is a permutation of its input
  --------------------------------------------------------------------------------------------

  sortCountsMatch <-
     sInduct "sortCountsMatch"
             (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
quickSort SList Integer
xs))
             (\SList Integer
xs (SInteger
_ :: SInteger) -> forall a. SymVal a => SList a -> SInteger
length @Integer SList Integer
xs) $
             \Proof
ih SList Integer
xs SInteger
e ->
                [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
quickSort SList Integer
xs)
                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> KDProofRaw SInteger
-> (SInteger -> SList Integer -> KDProofRaw SInteger)
-> KDProofRaw SInteger
forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList Integer
xs KDProofRaw SInteger
forall a. Trivial a => a
trivial
                            (\SInteger
a SList Integer
as -> SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
quickSort (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as))
                                   SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"expand quickSort"
                                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (let (SList Integer
lo, SList Integer
hi) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
a SList Integer
as)
                                               in SList Integer -> SList Integer
quickSort SList Integer
lo SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer -> SList Integer
quickSort SList Integer
hi)
                                   SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push count down"
                                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList Integer
lo, SList Integer
hi) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
a SList Integer
as)
                                   in SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
quickSort SList Integer
lo SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer -> SList Integer
quickSort SList Integer
hi)
                                   SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
countAppend Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer], Inst "e" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList Integer -> SList Integer
quickSort SList Integer
lo), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer -> SList Integer
quickSort SList Integer
hi), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
quickSort SList Integer
lo) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer -> SList Integer
quickSort SList Integer
hi)
                                   SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
countAppend Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer], Inst "e" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SList Integer -> SList Integer
quickSort SList Integer
hi), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
quickSort SList Integer
lo) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
quickSort SList Integer
hi)
                                   SInteger -> [Helper] -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof -> Helper
hprf  (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
ih                    Proof -> (Inst "xs" [Integer], Inst "e" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
lo, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                      , Proof -> Helper
hprf  (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
partitionNotLongerFst Proof -> (Inst "l" [Integer], Inst "pivot" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l"  SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a)
                                      , SBool -> Helper
hasm  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer
xs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as
                                      , String -> Helper
hcmnt String
"IH on lo"
                                      ]
                                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
quickSort SList Integer
hi)
                                   SInteger -> [Helper] -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof -> Helper
hprf  (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
ih                    Proof -> (Inst "xs" [Integer], Inst "e" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
hi, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                      , Proof -> Helper
hprf  (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
partitionNotLongerSnd Proof -> (Inst "l" [Integer], Inst "pivot" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l"  SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a)
                                      , SBool -> Helper
hasm  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer
xs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as
                                      , String -> Helper
hcmnt String
"IH on hi"
                                      ]
                                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
hi
                                   SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
countPartition Proof
-> (Inst "xs" [Integer], Inst "pivot" Integer, Inst "e" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                   KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs
                                   SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed)

  sortIsPermutation <- lemma "sortIsPermutation" (\(Forall @"xs" SList Integer
xs) -> SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs (SList Integer -> SList Integer
quickSort SList Integer
xs)) [sortCountsMatch]

  --------------------------------------------------------------------------------------------
  -- Part V. Helper lemmas for nonDecreasing
  --------------------------------------------------------------------------------------------
  nonDecreasingMerge <-
      inductWith cvc5 "nonDecreasingMerge"
          (\(Forall @"xs" SList Integer
xs) (Forall @"pivot" SInteger
pivot) (Forall @"ys" SList Integer
ys) ->
                     SList Integer -> SBool
nonDecreasing SList Integer
xs SBool -> SBool -> SBool
.&& SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
xs
                 SBool -> SBool -> SBool
.&& SList Integer -> SBool
nonDecreasing SList Integer
ys SBool -> SBool -> SBool
.&& SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
ys SBool -> SBool -> SBool
.=> SList Integer -> SBool
nonDecreasing (SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
pivot SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)) $
          \Proof
ih SInteger
x SList Integer
xs SInteger
pivot SList Integer
ys ->
               [SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs), SInteger -> SList Integer -> SBool
llt SInteger
pivot SList Integer
xs, SList Integer -> SBool
nonDecreasing SList Integer
ys, SInteger -> SList Integer -> SBool
lge SInteger
pivot SList Integer
ys]
            [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
pivot SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> KDProofRaw SBool
-> (SInteger -> SList Integer -> KDProofRaw SBool)
-> KDProofRaw SBool
forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList Integer
xs KDProofRaw SBool
forall a. Trivial a => a
trivial
                     (\SInteger
a SList Integer
as -> SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
pivot SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
a SBool -> SBool -> SBool
.&& SList Integer -> SBool
nonDecreasing (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
pivot SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys)
                            SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih
                            KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                            SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed)

  --------------------------------------------------------------------------------------------
  -- Part VI. Prove that the output of quick sort is non-decreasing
  --------------------------------------------------------------------------------------------
  sortIsNonDecreasing <-
     sInductWith cvc5 "sortIsNonDecreasing"
             (\(Forall @"xs" SList Integer
xs) -> SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer
quickSort SList Integer
xs))
             (length @Integer) $
             \Proof
ih SList Integer
xs ->
                [] [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer
quickSort SList Integer
xs)
                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer
-> KDProofRaw SBool
-> (SInteger -> SList Integer -> KDProofRaw SBool)
-> KDProofRaw SBool
forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList Integer
xs KDProofRaw SBool
forall a. Trivial a => a
trivial
                            (\SInteger
a SList Integer
as -> SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer
quickSort (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as))
                                   SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"expand quickSort"
                                   KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SBool
nonDecreasing (let (SList Integer
lo, SList Integer
hi) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
a SList Integer
as)
                                                     in SList Integer -> SList Integer
quickSort SList Integer
lo SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer -> SList Integer
quickSort SList Integer
hi)
                                   SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push nonDecreasing down"
                                   KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList Integer
lo, SList Integer
hi) = STuple [Integer] [Integer] -> (SList Integer, SList Integer)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SInteger -> SList Integer -> STuple [Integer] [Integer]
partition SInteger
a SList Integer
as)
                                   in SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer
quickSort SList Integer
lo SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
a SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer -> SList Integer
quickSort SList Integer
hi)
                                   SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ -- Deduce that lo/hi is not longer than as, and hence, shorter than xs
                                        Proof
partitionNotLongerFst Proof -> (Inst "l" [Integer], Inst "pivot" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a)
                                      , Proof
partitionNotLongerSnd Proof -> (Inst "l" [Integer], Inst "pivot" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a)

                                        -- Use the inductive hypothesis twice to deduce quickSort of lo and hi are nonDecreasing
                                      , Proof
ih Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
lo  -- nonDecreasing (quickSort lo)
                                      , Proof
ih Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
hi  -- nonDecreasing (quickSort hi)

                                      -- Deduce that lo is all less than a, and hi is all greater than or equal to a
                                      , Proof
partitionFstLT Proof -> (Inst "l" [Integer], Inst "pivot" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a)
                                      , Proof
partitionSndGE Proof -> (Inst "l" [Integer], Inst "pivot" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a)

                                      -- Deduce that quickSort lo is all less than a
                                      , Proof
sortIsPermutation Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at`  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
lo
                                      , Proof
lltPermutation    Proof
-> (Inst "xs" [Integer], Inst "pivot" Integer, Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList Integer -> SList Integer
quickSort SList Integer
lo), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
lo)

                                      -- Deduce that quickSort hi is all greater than or equal to a
                                      , Proof
sortIsPermutation Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at`  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
hi
                                      , Proof
lgePermutation    Proof
-> (Inst "xs" [Integer], Inst "pivot" Integer, Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList Integer -> SList Integer
quickSort SList Integer
hi), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
hi)

                                      -- Finally conclude that the whole reconstruction is non-decreasing
                                      , Proof
nonDecreasingMerge Proof
-> (Inst "xs" [Integer], Inst "pivot" Integer, Inst "ys" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList Integer -> SList Integer
quickSort SList Integer
lo), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SList Integer -> SList Integer
quickSort SList Integer
hi))
                                      ]
                                   KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed)

  --------------------------------------------------------------------------------------------
  -- Part VII. Putting it together
  --------------------------------------------------------------------------------------------

  qs <- lemma "quickSortIsCorrect"
           (\(Forall @"xs" SList Integer
xs) -> let out :: SList Integer
out = SList Integer -> SList Integer
quickSort SList Integer
xs in SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs SList Integer
out SBool -> SBool -> SBool
.&& SList Integer -> SBool
nonDecreasing SList Integer
out)
           [sortIsPermutation, sortIsNonDecreasing]

  -- | We can display the dependencies in a proof
  liftIO $ do putStrLn "== Dependencies:"
              putStr $ show $ getProofTree qs

  pure qs