-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.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 CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE OverloadedLists     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.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.TP
import qualified Data.SBV.TP.List as TP

import qualified Documentation.SBV.Examples.TP.SortHelpers as SH

#ifdef DOCTEST
-- $setup
-- >>> :set -XTypeApplications
#endif

-- * Quick sort

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

-- * Correctness proof

-- | Correctness of quick-sort.
--
-- We have:
--
-- >>> correctness @Integer
-- Inductive lemma: countAppend
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2 (unfold count)                                    Q.E.D.
--   Step: 3                                                   Q.E.D.
--   Step: 4 (simplify)                                        Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: countNonNeg
--   Step: Base                                                Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1.1                                             Q.E.D.
--     Step: 1.1.2                                             Q.E.D.
--     Step: 1.2.1                                             Q.E.D.
--     Step: 1.2.2                                             Q.E.D.
--     Step: 1.Completeness                                    Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: countElem
--   Step: Base                                                Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1.1                                             Q.E.D.
--     Step: 1.1.2                                             Q.E.D.
--     Step: 1.2.1                                             Q.E.D.
--     Step: 1.2.2                                             Q.E.D.
--     Step: 1.Completeness                                    Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: elemCount
--   Step: Base                                                Q.E.D.
--   Step: 1 (2 way case split)
--     Step: 1.1                                               Q.E.D.
--     Step: 1.2.1                                             Q.E.D.
--     Step: 1.2.2                                             Q.E.D.
--     Step: 1.Completeness                                    Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: sublistCorrect
--   Step: 1                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: sublistElem
--   Step: 1                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: sublistTail                                          Q.E.D.
-- Lemma: sublistIfPerm                                        Q.E.D.
-- Inductive lemma: lltCorrect
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: lgeCorrect
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: lltSublist
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: lltPermutation
--   Step: 1                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: lgeSublist
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: lgePermutation
--   Step: 1                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: partitionFstLT
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2 (push llt down)                                   Q.E.D.
--   Step: 3                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: partitionSndGE
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2 (push lge down)                                   Q.E.D.
--   Step: 3                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma (strong): partitionNotLongerFst
--   Step: Measure is non-negative                             Q.E.D.
--   Step: 1 (2 way full case split)
--     Step: 1.1                                               Q.E.D.
--     Step: 1.2.1                                             Q.E.D.
--     Step: 1.2.2 (simplify)                                  Q.E.D.
--     Step: 1.2.3                                             Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma (strong): partitionNotLongerSnd
--   Step: Measure is non-negative                             Q.E.D.
--   Step: 1 (2 way full case split)
--     Step: 1.1                                               Q.E.D.
--     Step: 1.2.1                                             Q.E.D.
--     Step: 1.2.2 (simplify)                                  Q.E.D.
--     Step: 1.2.3                                             Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: countPartition
--   Step: Base                                                Q.E.D.
--   Step: 1 (expand partition)                                Q.E.D.
--   Step: 2 (push countTuple down)                            Q.E.D.
--   Step: 3 (2 way case split)
--     Step: 3.1.1                                             Q.E.D.
--     Step: 3.1.2 (simplify)                                  Q.E.D.
--     Step: 3.1.3                                             Q.E.D.
--     Step: 3.2.1                                             Q.E.D.
--     Step: 3.2.2 (simplify)                                  Q.E.D.
--     Step: 3.2.3                                             Q.E.D.
--     Step: 3.Completeness                                    Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma (strong): sortCountsMatch
--   Step: Measure is non-negative                             Q.E.D.
--   Step: 1 (2 way full case split)
--     Step: 1.1                                               Q.E.D.
--     Step: 1.2.1                                             Q.E.D.
--     Step: 1.2.2 (expand quickSort)                          Q.E.D.
--     Step: 1.2.3 (push count down)                           Q.E.D.
--     Step: 1.2.4                                             Q.E.D.
--     Step: 1.2.5                                             Q.E.D.
--     Step: 1.2.6 (IH on lo)                                  Q.E.D.
--     Step: 1.2.7 (IH on hi)                                  Q.E.D.
--     Step: 1.2.8                                             Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: sortIsPermutation                                    Q.E.D.
-- Inductive lemma: nonDecreasingMerge
--   Step: Base                                                Q.E.D.
--   Step: 1 (2 way full case split)
--     Step: 1.1                                               Q.E.D.
--     Step: 1.2.1                                             Q.E.D.
--     Step: 1.2.2                                             Q.E.D.
--     Step: 1.2.3                                             Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma (strong): sortIsNonDecreasing
--   Step: Measure is non-negative                             Q.E.D.
--   Step: 1 (2 way full case split)
--     Step: 1.1                                               Q.E.D.
--     Step: 1.2.1                                             Q.E.D.
--     Step: 1.2.2 (expand quickSort)                          Q.E.D.
--     Step: 1.2.3 (push nonDecreasing down)                   Q.E.D.
--     Step: 1.2.4                                             Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: quickSortIsCorrect                                   Q.E.D.
-- Inductive lemma: partitionSortedLeft
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: partitionSortedRight
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma: unchangedIfNondecreasing
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2                                                   Q.E.D.
--   Step: 3                                                   Q.E.D.
--   Step: 4                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: ifChangedThenUnsorted                                Q.E.D.
-- == Proof tree:
-- quickSortIsCorrect
--  ├╴sortIsPermutation
--  │  └╴sortCountsMatch
--  │     ├╴countAppend (x2)
--  │     ├╴partitionNotLongerFst
--  │     ├╴partitionNotLongerSnd
--  │     └╴countPartition
--  └╴sortIsNonDecreasing
--     ├╴partitionNotLongerFst
--     ├╴partitionNotLongerSnd
--     ├╴partitionFstLT
--     ├╴partitionSndGE
--     ├╴sortIsPermutation (x2)
--     ├╴lltPermutation
--     │  ├╴lltSublist
--     │  │  ├╴sublistElem
--     │  │  │  └╴sublistCorrect
--     │  │  │     ├╴countElem
--     │  │  │     │  └╴countNonNeg
--     │  │  │     └╴elemCount
--     │  │  ├╴lltCorrect
--     │  │  └╴sublistTail
--     │  └╴sublistIfPerm
--     ├╴lgePermutation
--     │  ├╴lgeSublist
--     │  │  ├╴sublistElem
--     │  │  ├╴lgeCorrect
--     │  │  └╴sublistTail
--     │  └╴sublistIfPerm
--     └╴nonDecreasingMerge
-- [Proven] quickSortIsCorrect :: Ɐxs ∷ [Integer] → Bool
correctness :: forall a. (Ord a, SymVal a) => IO (Proof (Forall "xs" [a] -> SBool))
correctness :: forall a.
(Ord a, SymVal a) =>
IO (Proof (Forall "xs" [a] -> SBool))
correctness = SMTConfig
-> TP (Proof (Forall "xs" [a] -> SBool))
-> IO (Proof (Forall "xs" [a] -> SBool))
forall a. SMTConfig -> TP a -> IO a
runTPWith (Int -> SMTConfig -> SMTConfig
tpRibbon Int
60 SMTConfig
z3) (TP (Proof (Forall "xs" [a] -> SBool))
 -> IO (Proof (Forall "xs" [a] -> SBool)))
-> TP (Proof (Forall "xs" [a] -> SBool))
-> IO (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$ do

  --------------------------------------------------------------------------------------------
  -- Part I. Import helper lemmas, definitions
  --------------------------------------------------------------------------------------------
  let count :: SBV a -> SList a -> SInteger
count         = forall a. SymVal a => SBV a -> SList a -> SInteger
TP.count         @a
      isPermutation :: SList a -> SList a -> SBool
isPermutation = forall a. SymVal a => SList a -> SList a -> SBool
SH.isPermutation @a
      nonDecreasing :: SList a -> SBool
nonDecreasing = forall a. (Ord a, SymVal a) => SList a -> SBool
SH.nonDecreasing @a
      sublist :: SList a -> SList a -> SBool
sublist       = forall a. SymVal a => SList a -> SList a -> SBool
SH.sublist       @a

  Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
countAppend   <- forall a.
SymVal a =>
TP
  (Proof
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool))
TP.countAppend   @a
  Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistElem   <- forall a.
(Eq a, SymVal a) =>
TP
  (Proof
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
SH.sublistElem   @a
  Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistTail   <- forall a.
(Eq a, SymVal a) =>
TP
  (Proof
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
SH.sublistTail   @a
  Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistIfPerm <- forall a.
(Eq a, SymVal a) =>
TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
SH.sublistIfPerm @a

  ---------------------------------------------------------------------------------------------------
  -- Part II. 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 :: SBV a -> SList a -> SBool
      llt :: SBV a -> SList a -> SBool
llt = String -> (SBV a -> SList a -> SBool) -> SBV a -> SList a -> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"llt" ((SBV a -> SList a -> SBool) -> SBV a -> SList a -> SBool)
-> (SBV a -> SList a -> SBool) -> SBV a -> SList a -> SBool
forall a b. (a -> b) -> a -> b
$ \SBV a
pivot SList a
l -> SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
l SBool -> SBool -> SBool
.|| let (SBV a
x, SList a
xs) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
l in SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<  SBV a
pivot SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
llt SBV a
pivot SList a
xs
      lge :: SBV a -> SList a -> SBool
lge = String -> (SBV a -> SList a -> SBool) -> SBV a -> SList a -> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"lge" ((SBV a -> SList a -> SBool) -> SBV a -> SList a -> SBool)
-> (SBV a -> SList a -> SBool) -> SBV a -> SList a -> SBool
forall a b. (a -> b) -> a -> b
$ \SBV a
pivot SList a
l -> SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
l SBool -> SBool -> SBool
.|| let (SBV a
x, SList a
xs) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
l in SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV a
pivot SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
lge SBV a
pivot SList a
xs

  -- llt correctness
  Proof
  (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
lltCorrect <-
     String
-> (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
forall t.
(Proposition
   (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool) t)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"lltCorrect"
            (\(Forall SList a
xs) (Forall SBV a
e) (Forall SBV a
pivot) -> SBV a -> SList a -> SBool
llt SBV a
pivot SList a
xs SBool -> SBool -> SBool
.&& SBV a
e SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList a
xs SBool -> SBool -> SBool
.=> SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot) ((Proof
    (IHType
       (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
  -> IHArg
       (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
  -> IStepArgs
       (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)))
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
forall a b. (a -> b) -> a -> b
$
            \Proof
  (IHType
     (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
ih (SBV a
x, SList a
xs) SBV a
e SBV a
pivot -> [SBV a -> SList a -> SBool
llt SBV a
pivot (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs), SBV a
e SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)]
                                [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot
                                SBool
-> Proof (Forall "e" a -> Forall "pivot" a -> SBool)
-> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
Proof (Forall "e" a -> Forall "pivot" a -> SBool)
ih
                                TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed

  -- lge correctness
  Proof
  (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
lgeCorrect <-
     String
-> (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
forall t.
(Proposition
   (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool) t)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"lgeCorrect"
            (\(Forall SList a
xs) (Forall SBV a
e) (Forall SBV a
pivot) -> SBV a -> SList a -> SBool
lge SBV a
pivot SList a
xs SBool -> SBool -> SBool
.&& SBV a
e SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList a
xs SBool -> SBool -> SBool
.=> SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV a
pivot) ((Proof
    (IHType
       (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
  -> IHArg
       (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
  -> IStepArgs
       (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)))
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
forall a b. (a -> b) -> a -> b
$
            \Proof
  (IHType
     (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
ih (SBV a
x, SList a
xs) SBV a
e SBV a
pivot -> [SBV a -> SList a -> SBool
lge SBV a
pivot (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs), SBV a
e SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)]
                                [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV a
pivot
                                SBool
-> Proof (Forall "e" a -> Forall "pivot" a -> SBool)
-> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool))
Proof (Forall "e" a -> Forall "pivot" a -> SBool)
ih
                                TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed

  -- 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
  Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
lltSublist <-
     SMTConfig
-> String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall t.
(Proposition
   (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         t)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith SMTConfig
cvc5 String
"lltSublist"
            (\(Forall SList a
xs) (Forall SBV a
pivot) (Forall SList a
ys) -> SBV a -> SList a -> SBool
llt SBV a
pivot SList a
ys SBool -> SBool -> SBool
.&& SList a
xs SList a -> SList a -> SBool
`sublist` SList a
ys SBool -> SBool -> SBool
.=> SBV a -> SList a -> SBool
llt SBV a
pivot SList a
xs) ((Proof
    (IHType
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
  -> IHArg
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
  -> IStepArgs
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)))
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
            \Proof
  (IHType
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
ih (SBV a
x, SList a
xs) SBV a
pivot SList a
ys -> [SBV a -> SList a -> SBool
llt SBV a
pivot SList a
ys, (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SList a -> SList a -> SBool
`sublist` SList a
ys]
                                 [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a -> SList a -> SBool
llt SBV a
pivot (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
llt SBV a
pivot SList a
xs
                                 -- To establish x .< pivot, observe that x is in ys, and together
                                 -- with llt pivot ys, we get that x is less than pivot
                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistElem Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV a
x,   forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                                 TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
lltCorrect  Proof
  (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e"  SBV a
x,  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
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
                                 Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistTail Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV a
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                                 Hinted (Hinted (TPProofRaw SBool))
-> Proof Bool -> Hinted (Hinted (Hinted (TPProofRaw SBool)))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
Proof (Forall "pivot" a -> Forall "ys" [a] -> SBool)
ih          Proof (Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> IArgs (Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
pivot, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                                 Hinted (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (Hinted (TPProofRaw SBool))))
-> ChainsTo (Hinted (Hinted (Hinted (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed

  -- Variant of the above for the permutation case
  Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
lltPermutation <-
     String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> StepArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
     Bool
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall t.
(Proposition
   (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> StepArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool) t
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"lltPermutation"
           (\(Forall SList a
xs) (Forall SBV a
pivot) (Forall SList a
ys) -> SBV a -> SList a -> SBool
llt SBV a
pivot SList a
ys SBool -> SBool -> SBool
.&& SList a -> SList a -> SBool
isPermutation SList a
xs SList a
ys SBool -> SBool -> SBool
.=> SBV a -> SList a -> SBool
llt SBV a
pivot SList a
xs) (StepArgs
   (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)))
-> StepArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
     Bool
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
           \SList a
xs SBV a
pivot SList a
ys -> [SBV a -> SList a -> SBool
llt SBV a
pivot SList a
ys, SList a -> SList a -> SBool
isPermutation SList a
xs SList a
ys]
                        [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a -> SList a -> SBool
llt SBV a
pivot SList a
xs
                        SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
lltSublist    Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
pivot, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                        TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistIfPerm Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                        Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw 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
  Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
lgeSublist <-
     SMTConfig
-> String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall t.
(Proposition
   (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         t)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith SMTConfig
cvc5 String
"lgeSublist"
            (\(Forall SList a
xs) (Forall SBV a
pivot) (Forall SList a
ys) -> SBV a -> SList a -> SBool
lge SBV a
pivot SList a
ys SBool -> SBool -> SBool
.&& SList a
xs SList a -> SList a -> SBool
`sublist` SList a
ys SBool -> SBool -> SBool
.=> SBV a -> SList a -> SBool
lge SBV a
pivot SList a
xs) ((Proof
    (IHType
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
  -> IHArg
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
  -> IStepArgs
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)))
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
            \Proof
  (IHType
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
ih (SBV a
x, SList a
xs) SBV a
pivot SList a
ys -> [SBV a -> SList a -> SBool
lge SBV a
pivot SList a
ys, (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SList a -> SList a -> SBool
`sublist` SList a
ys]
                                 [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a -> SList a -> SBool
lge SBV a
pivot (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV a
pivot SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
lge SBV a
pivot SList a
xs
                                 -- 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
                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistElem Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV a
x,   forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                                 TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
lgeCorrect  Proof
  (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "e" a -> Forall "pivot" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e"  SBV a
x,  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
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
                                 Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistTail Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV a
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                                 Hinted (Hinted (TPProofRaw SBool))
-> Proof Bool -> Hinted (Hinted (Hinted (TPProofRaw SBool)))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
Proof (Forall "pivot" a -> Forall "ys" [a] -> SBool)
ih          Proof (Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> IArgs (Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
pivot, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                                 Hinted (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (Hinted (TPProofRaw SBool))))
-> ChainsTo (Hinted (Hinted (Hinted (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed

  -- Variant of the above for the permutation case
  Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
lgePermutation <-
     String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> StepArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
     Bool
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall t.
(Proposition
   (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> StepArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool) t
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"lgePermutation"
           (\(Forall SList a
xs) (Forall SBV a
pivot) (Forall SList a
ys) -> SBV a -> SList a -> SBool
lge SBV a
pivot SList a
ys SBool -> SBool -> SBool
.&& SList a -> SList a -> SBool
isPermutation SList a
xs SList a
ys SBool -> SBool -> SBool
.=> SBV a -> SList a -> SBool
lge SBV a
pivot SList a
xs) (StepArgs
   (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)))
-> StepArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
     Bool
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
           \SList a
xs SBV a
pivot SList a
ys -> [SBV a -> SList a -> SBool
lge SBV a
pivot SList a
ys, SList a -> SList a -> SBool
isPermutation SList a
xs SList a
ys]
                        [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a -> SList a -> SBool
lge SBV a
pivot SList a
xs
                        SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
lgeSublist    Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
pivot, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                        TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
sublistIfPerm Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys)
                        Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed

  --------------------------------------------------------------------------------------------
  -- Part III. Helper lemmas for partition
  --------------------------------------------------------------------------------------------

  -- The first element of the partition produces all smaller elements
  Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
partitionFstLT <- SMTConfig
-> String
-> (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> (Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall t.
(Proposition (Forall "l" [a] -> Forall "pivot" a -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> (Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) t)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith SMTConfig
cvc5 String
"partitionFstLT"
     (\(Forall SList a
l) (Forall SBV a
pivot) -> SBV a -> SList a -> SBool
llt SBV a
pivot (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
l))) ((Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
  -> IHArg (Forall "l" [a] -> Forall "pivot" a -> SBool)
  -> IStepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
 -> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)))
-> (Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall a b. (a -> b) -> a -> b
$
     \Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
ih (SBV a
a, SList a
as) SBV a
pivot -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a -> SList a -> SBool
llt SBV a
pivot (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as)))
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a -> SList a -> SBool
llt SBV a
pivot (SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot)
                                               (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as))
                                               (     STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)))
                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push llt down"
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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 (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot)
                                    (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
llt SBV a
pivot (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)))
                                    (               SBV a -> SList a -> SBool
llt SBV a
pivot (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)))
                             SBool -> Proof (Forall "pivot" a -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
Proof (Forall "pivot" a -> SBool)
ih
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed

  -- The second element of the partition produces all greater-than-or-equal to elements
  Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
partitionSndGE <- SMTConfig
-> String
-> (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> (Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall t.
(Proposition (Forall "l" [a] -> Forall "pivot" a -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> (Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) t)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith SMTConfig
cvc5 String
"partitionSndGE"
     (\(Forall SList a
l) (Forall SBV a
pivot) -> SBV a -> SList a -> SBool
lge SBV a
pivot (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
l))) ((Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
  -> IHArg (Forall "l" [a] -> Forall "pivot" a -> SBool)
  -> IStepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
 -> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)))
-> (Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall a b. (a -> b) -> a -> b
$
     \Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
ih (SBV a
a, SList a
as) SBV a
pivot -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a -> SList a -> SBool
lge SBV a
pivot (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as)))
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a -> SList a -> SBool
lge SBV a
pivot (SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot)
                                               (     STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as))
                                               (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)))
                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push lge down"
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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 (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot)
                                    (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
lge SBV a
pivot (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)))
                                    (               SBV a -> SList a -> SBool
lge SBV a
pivot (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)))
                             SBool -> Proof (Forall "pivot" a -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "l" [a] -> Forall "pivot" a -> SBool))
Proof (Forall "pivot" a -> SBool)
ih
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed

  -- The first element of partition does not increase in size
  Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
partitionNotLongerFst <- String
-> (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> MeasureArgs
     (Forall "l" [a] -> Forall "pivot" a -> SBool) Integer
-> (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> StepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "l" [a] -> Forall "pivot" a -> SBool), Zero m,
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> MeasureArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) m
-> (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> StepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) t)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
sInduct String
"partitionNotLongerFst"
     (\(Forall SList a
l) (Forall SBV a
pivot) -> SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition @a SBV a
pivot SList a
l)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l)
     (\SList a
l SBV a
_ -> SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l) ((Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
  -> StepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
 -> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)))
-> (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> StepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall a b. (a -> b) -> a -> b
$
     \Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
ih SList a
l SBV a
pivot -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition @a SBV a
pivot SList a
l)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l
                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a
-> TPProofRaw SBool
-> (SBV a -> SList a -> TPProofRaw SBool)
-> TPProofRaw SBool
forall a r.
SymVal a =>
SList a
-> TPProofRaw r
-> (SBV a -> SList a -> TPProofRaw r)
-> TPProofRaw r
split SList a
l TPProofRaw SBool
forall a. Trivial a => a
trivial
                                (\SBV a
a SList a
as -> let lo :: SList a
lo = STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)
                                       in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot)
                                              (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
lo) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as))
                                              (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length       SList a
lo  SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as))
                                       SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                       TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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 (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot)
                                              (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<=     SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
as)
                                              (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
as)
                                       SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
ih Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> IArgs (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList a
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
pivot)
                                       TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed)

  -- The second element of partition does not increase in size
  Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
partitionNotLongerSnd <- String
-> (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> MeasureArgs
     (Forall "l" [a] -> Forall "pivot" a -> SBool) Integer
-> (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> StepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition (Forall "l" [a] -> Forall "pivot" a -> SBool), Zero m,
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> MeasureArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) m
-> (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> StepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) t)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
sInduct String
"partitionNotLongerSnd"
     (\(Forall SList a
l) (Forall SBV a
pivot) -> SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition @a SBV a
pivot SList a
l)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l)
     (\SList a
l SBV a
_ -> SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l) ((Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
  -> StepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
 -> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)))
-> (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
    -> StepArgs (Forall "l" [a] -> Forall "pivot" a -> SBool) Bool)
-> TP (Proof (Forall "l" [a] -> Forall "pivot" a -> SBool))
forall a b. (a -> b) -> a -> b
$
     \Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
ih SList a
l SBV a
pivot -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition @a SBV a
pivot SList a
l)) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l
                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a
-> TPProofRaw SBool
-> (SBV a -> SList a -> TPProofRaw SBool)
-> TPProofRaw SBool
forall a r.
SymVal a =>
SList a
-> TPProofRaw r
-> (SBV a -> SList a -> TPProofRaw r)
-> TPProofRaw r
split SList a
l TPProofRaw SBool
forall a. Trivial a => a
trivial
                                (\SBV a
a SList a
as -> let hi :: SList a
hi = STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)
                                       in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot)
                                              (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length       SList a
hi  SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as))
                                              (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
hi) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as))
                                       SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                       TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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 (SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
pivot)
                                              (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
hi SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
as)
                                              (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
hi SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<=     SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
as)
                                       SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
ih Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> IArgs (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList a
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
pivot)
                                       TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed)

  --------------------------------------------------------------------------------------------
  -- Part IV. Helper lemmas for count
  --------------------------------------------------------------------------------------------

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

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

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

  Proof (Forall "xs" [a] -> SBool)
sortIsPermutation <- String
-> (Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"sortIsPermutation" (\(Forall SList a
xs) -> SList a -> SList a -> SBool
isPermutation SList a
xs (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
xs)) [Proof (Forall "xs" [a] -> Forall "e" a -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
sortCountsMatch]

  --------------------------------------------------------------------------------------------
  -- Part VI. Helper lemmas for nonDecreasing
  --------------------------------------------------------------------------------------------
  Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
nonDecreasingMerge <-
      SMTConfig
-> String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall t.
(Proposition
   (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "xs" [a]
    -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         t)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith SMTConfig
cvc5 String
"nonDecreasingMerge"
          (\(Forall SList a
xs) (Forall SBV a
pivot) (Forall SList a
ys) ->
                     SList a -> SBool
nonDecreasing SList a
xs SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
llt SBV a
pivot SList a
xs
                 SBool -> SBool -> SBool
.&& SList a -> SBool
nonDecreasing SList a
ys SBool -> SBool -> SBool
.&& SBV a -> SList a -> SBool
lge SBV a
pivot SList a
ys SBool -> SBool -> SBool
.=> SList a -> SBool
nonDecreasing (SList a
xs SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SList a)
SBV a
pivot] SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
ys)) ((Proof
    (IHType
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
  -> IHArg
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
  -> IStepArgs
       (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)))
-> (Proof
      (IHType
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
    -> IHArg
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
    -> IStepArgs
         (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
          \Proof
  (IHType
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
ih (SBV a
x, SList a
xs) SBV a
pivot SList a
ys ->
                [SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs), SBV a -> SList a -> SBool
llt SBV a
pivot SList a
xs, SList a -> SBool
nonDecreasing SList a
ys, SBV a -> SList a -> SBool
lge SBV a
pivot SList a
ys]
             [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SList a)
SBV a
pivot] SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
ys)
             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a
-> TPProofRaw SBool
-> (SBV a -> SList a -> TPProofRaw SBool)
-> TPProofRaw SBool
forall a r.
SymVal a =>
SList a
-> TPProofRaw r
-> (SBV a -> SList a -> TPProofRaw r)
-> TPProofRaw r
split SList a
xs TPProofRaw SBool
forall a. Trivial a => a
trivial
                      (\SBV a
a SList a
as -> SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SList a)
SBV a
pivot] SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
ys)
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
a SBool -> SBool -> SBool
.&& SList a -> SBool
nonDecreasing (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SList a)
SBV a
pivot] SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
ys)
                             SBool
-> Proof (Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (IHType
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool))
Proof (Forall "pivot" a -> Forall "ys" [a] -> SBool)
ih
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed)

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

                                   -- Use the inductive hypothesis twice to deduce quickSort of lo and hi are nonDecreasing
                                   Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
ih Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
lo  -- nonDecreasing (quickSort lo)
                                   Hinted (Hinted (TPProofRaw SBool))
-> Proof Bool -> Hinted (Hinted (Hinted (TPProofRaw SBool)))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
ih Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
hi  -- nonDecreasing (quickSort hi)

                                   -- Deduce that lo is all less than a, and hi is all greater than or equal to a
                                   Hinted (Hinted (Hinted (TPProofRaw SBool)))
-> Proof Bool
-> Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
partitionFstLT Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> IArgs (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList a
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
a)
                                   Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))
-> Proof Bool
-> Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
partitionSndGE Proof (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> IArgs (Forall "l" [a] -> Forall "pivot" a -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"l" SList a
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
a)

                                   -- Deduce that quickSort lo is all less than a
                                   Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))
-> Proof Bool
-> Hinted
     (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
sortIsPermutation Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at`  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
lo
                                   Hinted
  (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))
-> Proof Bool
-> Hinted
     (Hinted
        (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
lltPermutation    Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
lo), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
lo)

                                   -- Deduce that quickSort hi is all greater than or equal to a
                                   Hinted
  (Hinted
     (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))
-> Proof Bool
-> Hinted
     (Hinted
        (Hinted
           (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> SBool)
sortIsPermutation Proof (Forall "xs" [a] -> SBool)
-> IArgs (Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at`  forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList a
hi
                                   Hinted
  (Hinted
     (Hinted
        (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))))
-> Proof Bool
-> Hinted
     (Hinted
        (Hinted
           (Hinted
              (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
lgePermutation    Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
hi), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
hi)

                                   -- Finally conclude that the whole reconstruction is non-decreasing
                                   Hinted
  (Hinted
     (Hinted
        (Hinted
           (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))))
-> Proof Bool
-> Hinted
     (Hinted
        (Hinted
           (Hinted
              (Hinted
                 (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))))))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
nonDecreasingMerge Proof
  (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "pivot" a -> Forall "ys" [a] -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
lo), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"pivot" SBV a
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
hi))
                                   Hinted
  (Hinted
     (Hinted
        (Hinted
           (Hinted
              (Hinted (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool))))))))))
-> ChainsTo
     (Hinted
        (Hinted
           (Hinted
              (Hinted
                 (Hinted
                    (Hinted
                       (Hinted (Hinted (Hinted (Hinted (TPProofRaw SBool)))))))))))
-> ChainsTo
     (Hinted
        (Hinted
           (Hinted
              (Hinted
                 (Hinted
                    (Hinted
                       (Hinted (Hinted (Hinted (Hinted (TPProofRaw 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
TPProofRaw SBool
forall a. TPProofRaw a
qed)

  --------------------------------------------------------------------------------------------
  -- Part VIII. Putting it together
  --------------------------------------------------------------------------------------------

  Proof (Forall "xs" [a] -> SBool)
qs <- String
-> (Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"quickSortIsCorrect"
              (\(Forall SList a
xs) -> let out :: SList a
out = SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
xs in SList a -> SList a -> SBool
isPermutation SList a
xs SList a
out SBool -> SBool -> SBool
.&& SList a -> SBool
nonDecreasing SList a
out)
              [Proof (Forall "xs" [a] -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "xs" [a] -> SBool)
sortIsPermutation, Proof (Forall "xs" [a] -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "xs" [a] -> SBool)
sortIsNonDecreasing]

  --------------------------------------------------------------------------------------------
  -- Part IX. Bonus: This property isn't really needed for correctness, but let's also prove
  -- that if a list is sorted, then quick-sort returns it unchanged.
  --------------------------------------------------------------------------------------------
  Proof (Forall "as" [a] -> Forall "pivot" a -> SBool)
partitionSortedLeft <-
     SMTConfig
-> String
-> (Forall "as" [a] -> Forall "pivot" a -> SBool)
-> (Proof (IHType (Forall "as" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "as" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "as" [a] -> Forall "pivot" a -> SBool) [a])
-> TP (Proof (Forall "as" [a] -> Forall "pivot" a -> SBool))
forall t.
(Proposition (Forall "as" [a] -> Forall "pivot" a -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "as" [a] -> Forall "pivot" a -> SBool)
-> (Proof (IHType (Forall "as" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "as" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "as" [a] -> Forall "pivot" a -> SBool) t)
-> TP (Proof (Forall "as" [a] -> Forall "pivot" a -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith SMTConfig
cvc5 String
"partitionSortedLeft"
            (\(Forall @"as" SList a
as) (Forall @"pivot" SBV a
pivot) -> SList a -> SBool
nonDecreasing (SBV a
pivot SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as) SBool -> SBool -> SBool
.=> SList a -> SBool
forall a. SymVal a => SList a -> SBool
null (STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as))) ((Proof (IHType (Forall "as" [a] -> Forall "pivot" a -> SBool))
  -> IHArg (Forall "as" [a] -> Forall "pivot" a -> SBool)
  -> IStepArgs (Forall "as" [a] -> Forall "pivot" a -> SBool) [a])
 -> TP (Proof (Forall "as" [a] -> Forall "pivot" a -> SBool)))
-> (Proof (IHType (Forall "as" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "as" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "as" [a] -> Forall "pivot" a -> SBool) [a])
-> TP (Proof (Forall "as" [a] -> Forall "pivot" a -> SBool))
forall a b. (a -> b) -> a -> b
$
            \Proof (IHType (Forall "as" [a] -> Forall "pivot" a -> SBool))
ih (SBV a
a, SList a
as) SBV a
pivot -> [SList a -> SBool
nonDecreasing (SBV a
pivot SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as)]
                              [SBool] -> TPProofRaw (SList a) -> (SBool, TPProofRaw (SList a))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV a
fst (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as))
                              SList a -> ChainsTo (SList a) -> ChainsTo (SList a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList a
lo, SList a
_) = STuple [a] [a] -> (SList a, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)
                              in SList a
lo
                              SList a -> Proof (Forall "pivot" a -> SBool) -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "as" [a] -> Forall "pivot" a -> SBool))
Proof (Forall "pivot" a -> SBool)
ih
                              TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a
forall a. SymVal a => SList a
nil
                              SList a -> ChainsTo (SList a) -> ChainsTo (SList a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SList a)
TPProofRaw (SList a)
forall a. TPProofRaw a
qed

  Proof (Forall "xs" [a] -> Forall "pivot" a -> SBool)
partitionSortedRight <-
     SMTConfig
-> String
-> (Forall "xs" [a] -> Forall "pivot" a -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "pivot" a -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> Forall "pivot" a -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> Forall "pivot" a -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "xs" [a] -> Forall "pivot" a -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "pivot" a -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> Forall "pivot" a -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
inductWith SMTConfig
cvc5 String
"partitionSortedRight"
           (\(Forall @"xs" SList a
xs) (Forall @"pivot" SBV a
pivot) -> SList a -> SBool
nonDecreasing (SBV a
pivot SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SBool -> SBool -> SBool
.=> SList a
xs SList a -> SList a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
xs)) ((Proof (IHType (Forall "xs" [a] -> Forall "pivot" a -> SBool))
  -> IHArg (Forall "xs" [a] -> Forall "pivot" a -> SBool)
  -> IStepArgs (Forall "xs" [a] -> Forall "pivot" a -> SBool) [a])
 -> TP (Proof (Forall "xs" [a] -> Forall "pivot" a -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> Forall "pivot" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "pivot" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "pivot" a -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> Forall "pivot" a -> SBool))
forall a b. (a -> b) -> a -> b
$
           \Proof (IHType (Forall "xs" [a] -> Forall "pivot" a -> SBool))
ih (SBV a
a, SList a
as) SBV a
pivot -> [SList a -> SBool
nonDecreasing (SBV a
pivot SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as)]
                             [SBool] -> TPProofRaw (SList a) -> (SBool, TPProofRaw (SList a))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- STuple [a] [a] -> SList a
forall a b. (SymVal a, SymVal b) => STuple a b -> SBV b
snd (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as))
                             SList a -> ChainsTo (SList a) -> ChainsTo (SList a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList a
_, SList a
hi) = STuple [a] [a] -> (SList a, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
pivot SList a
as)
                             in SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
hi
                             SList a -> Proof (Forall "pivot" a -> SBool) -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "xs" [a] -> Forall "pivot" a -> SBool))
Proof (Forall "pivot" a -> SBool)
ih
                             TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as
                             SList a -> ChainsTo (SList a) -> ChainsTo (SList a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SList a)
TPProofRaw (SList a)
forall a. TPProofRaw a
qed

  Proof (Forall "xs" [a] -> SBool)
unchangedIfNondecreasing <-
       String
-> (Forall "xs" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"unchangedIfNondecreasing"
              (\(Forall @"xs" SList a
xs) -> SList a -> SBool
nonDecreasing SList a
xs SBool -> SBool -> SBool
.=> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
xs SList a -> SList a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList a
xs) ((Proof (IHType (Forall "xs" [a] -> SBool))
  -> IHArg (Forall "xs" [a] -> SBool)
  -> IStepArgs (Forall "xs" [a] -> SBool) [a])
 -> TP (Proof (Forall "xs" [a] -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
              \Proof (IHType (Forall "xs" [a] -> SBool))
ih (SBV a
x, SList a
xs) -> [SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)]
                          [SBool] -> TPProofRaw (SList a) -> (SBool, TPProofRaw (SList a))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                          SList a -> ChainsTo (SList a) -> ChainsTo (SList a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList a
lo, SList a
hi) = STuple [a] [a] -> (SList a, SList a)
forall tup a. Tuple tup a => SBV tup -> a
untuple (SBV a -> SList a -> STuple [a] [a]
forall a. (Ord a, SymVal a) => SBV a -> SList a -> STuple [a] [a]
partition SBV a
x SList a
xs)
                          in SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
lo SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ [Item (SList a)
SBV a
x] SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
hi
                          SList a
-> Proof (Forall "as" [a] -> Forall "pivot" a -> SBool)
-> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "as" [a] -> Forall "pivot" a -> SBool)
partitionSortedLeft
                          TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [Item (SList a)
SBV a
x] SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
hi
                          SList a
-> Proof (Forall "xs" [a] -> Forall "pivot" a -> SBool)
-> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "pivot" a -> SBool)
partitionSortedRight
                          TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [Item (SList a)
SBV a
x] SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
xs
                          SList a -> Proof SBool -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "xs" [a] -> SBool))
ih
                          TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs
                          SList a -> ChainsTo (SList a) -> ChainsTo (SList a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SList a)
TPProofRaw (SList a)
forall a. TPProofRaw a
qed

  -- A nice corrollary to the above is that if quicksort changes its input, that implies the input was not non-decreasing:
  Proof (Forall "xs" [a] -> SBool)
_ <- String
-> (Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"ifChangedThenUnsorted"
             (\(Forall @"xs" SList a
xs) -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
quickSort SList a
xs SList a -> SList a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SList a
xs SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (SList a -> SBool
nonDecreasing SList a
xs))
             [Proof (Forall "xs" [a] -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "xs" [a] -> SBool)
unchangedIfNondecreasing]

  --------------------------------------------------------------------------------------------
  -- | We can display the dependencies in a proof
  --------------------------------------------------------------------------------------------
  IO () -> TP ()
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TP ()) -> IO () -> TP ()
forall a b. (a -> b) -> a -> b
$ do String -> IO ()
putStrLn String
"== Proof tree:"
              String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> Proof (Forall "xs" [a] -> SBool) -> String
forall a. Bool -> Proof a -> String
showProofTree Bool
True Proof (Forall "xs" [a] -> SBool)
qs

  Proof (Forall "xs" [a] -> SBool)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Proof (Forall "xs" [a] -> SBool)
qs

{- HLint ignore correctness "Use :" -}