-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.MergeSort
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proving merge sort correct.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.MergeSort where

import Prelude hiding (null, length, head, tail, elem, splitAt, (++), take, drop)

import Data.SBV
import Data.SBV.List
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

-- * Merge sort

-- | Merge two already sorted lists into another
merge :: (Ord a, SymVal a) => SList a -> SList a -> SList a
merge :: forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge = String
-> (SList a -> SList a -> SList a) -> SList a -> SList a -> SList a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"merge" ((SList a -> SList a -> SList a) -> SList a -> 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 SList a
r -> 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
r
                                    (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ 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
r) SList a
l
                                    (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ 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
l
                                          (SBV a
b, SList a
bs) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
r
                                      in 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
b) (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
as SList a
r) (SBV a
b SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
l SList a
bs)

-- | Merge sort, using 'merge' above to successively sort halved input
mergeSort :: (Ord a, SymVal a) => SList a -> SList a
mergeSort :: forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort = String -> (SList a -> SList a) -> SList a -> SList a
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"mergeSort" ((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 -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1) SList a
l
                                              (SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ let (SList a
h1, SList a
h2) = SInteger -> SList a -> (SList a, SList a)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) SList a
l
                                                in SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h1) (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h2)

-- * Correctness proof

-- | Correctness of merge-sort.
--
-- We have:
--
-- >>> correctness @Integer
-- Lemma: nonDecrInsert                                        Q.E.D.
-- Inductive lemma: countAppend
--   Step: Base                                                Q.E.D.
--   Step: 1                                                   Q.E.D.
--   Step: 2 (unfold count)                                    Q.E.D.
--   Step: 3                                                   Q.E.D.
--   Step: 4 (simplify)                                        Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: take_drop                                            Q.E.D.
-- Lemma: takeDropCount
--   Step: 1                                                   Q.E.D.
--   Step: 2                                                   Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma (strong): mergeKeepsSort
--   Step: Measure is non-negative                             Q.E.D.
--   Step: 1 (4 way full case split)
--     Step: 1.1                                               Q.E.D.
--     Step: 1.2                                               Q.E.D.
--     Step: 1.3                                               Q.E.D.
--     Step: 1.4.1 (unfold merge)                              Q.E.D.
--     Step: 1.4.2 (2 way case split)
--       Step: 1.4.2.1.1 (case split)                          Q.E.D.
--       Step: 1.4.2.1.2                                       Q.E.D.
--       Step: 1.4.2.2.1 (case split)                          Q.E.D.
--       Step: 1.4.2.2.2                                       Q.E.D.
--       Step: 1.4.2.Completeness                              Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma (strong): sortNonDecreasing
--   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 (unfold)                                    Q.E.D.
--     Step: 1.2.2 (push nonDecreasing down)                   Q.E.D.
--     Step: 1.2.3                                             Q.E.D.
--     Step: 1.2.4                                             Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma (strong): mergeCount
--   Step: Measure is non-negative                             Q.E.D.
--   Step: 1 (4 way full case split)
--     Step: 1.1                                               Q.E.D.
--     Step: 1.2                                               Q.E.D.
--     Step: 1.3                                               Q.E.D.
--     Step: 1.4.1 (unfold merge)                              Q.E.D.
--     Step: 1.4.2 (push count inside)                         Q.E.D.
--     Step: 1.4.3 (unfold count, twice)                       Q.E.D.
--     Step: 1.4.4                                             Q.E.D.
--     Step: 1.4.5                                             Q.E.D.
--     Step: 1.4.6 (unfold count in reverse, twice)            Q.E.D.
--     Step: 1.4.7 (simplify)                                  Q.E.D.
--   Result:                                                   Q.E.D.
-- Inductive lemma (strong): sortIsPermutation
--   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 (unfold mergeSort)                          Q.E.D.
--     Step: 1.2.2 (push count down, simplify, rearrange)      Q.E.D.
--     Step: 1.2.3                                             Q.E.D.
--     Step: 1.2.4                                             Q.E.D.
--     Step: 1.2.5                                             Q.E.D.
--     Step: 1.2.6                                             Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: mergeSortIsCorrect                                   Q.E.D.
-- [Proven] mergeSortIsCorrect :: Ɐ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 nonDecreasing :: SList a -> SBool
nonDecreasing = forall a. (Ord a, SymVal a) => SList a -> SBool
SH.nonDecreasing @a
        isPermutation :: SList a -> SList a -> SBool
isPermutation = forall a. SymVal a => SList a -> SList a -> SBool
SH.isPermutation @a
        count :: SBV a -> SList a -> SInteger
count         = forall a. SymVal a => SBV a -> SList a -> SInteger
TP.count         @a

    Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
nonDecrIns    <- forall a.
(Ord a, SymVal a) =>
TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
SH.nonDecrIns    @a
    Proof
  (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool)
takeDropCount <- forall a.
SymVal a =>
TP
  (Proof
     (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool))
TP.takeDropCount @a

    --------------------------------------------------------------------------------------------
    -- Part II. Prove that the output of merge sort is non-decreasing.
    --------------------------------------------------------------------------------------------

    Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
mergeKeepsSort <-
        SMTConfig
-> String
-> (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> MeasureArgs
     (Forall "xs" [a] -> Forall "ys" [a] -> SBool) (Integer, Integer)
-> (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
    -> StepArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) Bool)
-> TP (Proof (Forall "xs" [a] -> Forall "ys" [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] -> Forall "ys" [a] -> SBool), Zero m,
 SymVal t, EqSymbolic (SBV t)) =>
SMTConfig
-> String
-> (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
-> MeasureArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) m
-> (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
    -> StepArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sInductWith SMTConfig
cvc5 String
"mergeKeepsSort"
           (\(Forall SList a
xs) (Forall SList a
ys) -> SList a -> SBool
nonDecreasing SList a
xs SBool -> SBool -> SBool
.&& SList a -> SBool
nonDecreasing SList a
ys SBool -> SBool -> SBool
.=> SList a -> SBool
nonDecreasing (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
xs SList a
ys))
           (\SList a
xs SList a
ys -> (SInteger, SInteger) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
xs, SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
ys)) ((Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
  -> StepArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) Bool)
 -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)))
-> (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
    -> StepArgs (Forall "xs" [a] -> Forall "ys" [a] -> SBool) Bool)
-> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
           \Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
ih SList a
xs SList a
ys -> [SList a -> SBool
nonDecreasing SList a
xs, SList a -> SBool
nonDecreasing SList a
ys]
                     [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SList a, SList a)
-> TPProofRaw SBool
-> ((SBV a, SList a) -> TPProofRaw SBool)
-> ((SBV a, SList a) -> TPProofRaw SBool)
-> ((SBV a, SList a) -> (SBV a, SList a) -> TPProofRaw SBool)
-> TPProofRaw SBool
forall a b r.
(SymVal a, SymVal b) =>
(SList a, SList b)
-> TPProofRaw r
-> ((SBV b, SList b) -> TPProofRaw r)
-> ((SBV a, SList a) -> TPProofRaw r)
-> ((SBV a, SList a) -> (SBV b, SList b) -> TPProofRaw r)
-> TPProofRaw r
split2 (SList a
xs, SList a
ys)
                               TPProofRaw SBool
forall a. Trivial a => a
trivial           -- when both xs and ys are empty.  Trivial.
                               (SBV a, SList a) -> TPProofRaw SBool
forall a. Trivial a => a
trivial           -- when xs is empty, but ys isn't. Trivial.
                               (SBV a, SList a) -> TPProofRaw SBool
forall a. Trivial a => a
trivial           -- when ys is empty, but xs isn't. Trivial.
                               (\(SBV a
a, SList a
as) (SBV a
b, SList a
bs) ->
                                     SList a -> SBool
nonDecreasing (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as) (SBV a
b SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
bs))
                                  SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold merge"
                                  TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBool
nonDecreasing (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
b)
                                                        (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
as (SBV a
b SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
bs))
                                                        (SBV a
b SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as) SList a
bs))
                                  SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case split"
                                  TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
b SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> 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 -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
as (SBV a
b SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
bs))
                                                      SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
ih         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
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SBV a
b SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
bs))
                                                      TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
nonDecrIns Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
-> IArgs (Forall "x" a -> 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 @"x" SBV a
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
as (SBV a
b SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
bs)))
                                                      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
                                           , SBV a
a SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV a
b  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SList a -> SBool
nonDecreasing (SBV a
b SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as) SList a
bs)
                                                      SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
ih         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" (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
bs)
                                                      TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
nonDecrIns Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
-> IArgs (Forall "x" a -> 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 @"x" SBV a
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
a SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as) SList a
bs))
                                                      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
                                           ])

    Proof (Forall "xs" [a] -> SBool)
sortNonDecreasing <-
        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)) =>
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)) =>
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))
sInduct String
"sortNonDecreasing"
                (\(Forall SList a
xs) -> SList a -> SBool
nonDecreasing (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
xs))
                MeasureArgs (Forall "xs" [a] -> SBool) Integer
SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length ((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
-> 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. TPProofRaw a
qed
                                      (\SBV a
e SList a
es -> SList a -> SBool
nonDecreasing (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es))
                                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold"
                                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList a
h1, SList a
h2) = SInteger -> SList a -> (SList a, SList a)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es)
                                                in SList a -> SBool
nonDecreasing (SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1)
                                                                      (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es)
                                                                      (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h1) (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h2)))
                                             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
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1)
                                                    (SList a -> SBool
nonDecreasing (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es))
                                                    (SList a -> SBool
nonDecreasing (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h1) (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h2)))
                                             SBool -> Proof Bool -> Hinted 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
es
                                             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 (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
es) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1)
                                                    SBool
sTrue
                                                    (SList a -> SBool
nonDecreasing (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h1) (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h2)))
                                             SBool -> Proof Bool -> Hinted 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
h1
                                             TPProofRaw SBool -> Proof Bool -> 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
h2
                                             Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)
mergeKeepsSort 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 -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h1), 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
mergeSort SList a
h2))
                                             Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (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 III. Prove that the output of merge sort is a permuation of its input
    --------------------------------------------------------------------------------------------
    Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
mergeCount <-
        String
-> (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
-> MeasureArgs
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
     (Integer, Integer)
-> (Proof
      (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
    -> StepArgs
         (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "ys" [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 "ys" [a] -> Forall "e" a -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
-> MeasureArgs
     (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool) m
-> (Proof
      (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
    -> StepArgs
         (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool) t)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool))
sInduct String
"mergeCount"
                (\(Forall SList a
xs) (Forall SList a
ys) (Forall SBV a
e) -> SBV a -> SList a -> SInteger
count SBV a
e (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
xs SList a
ys) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 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)
                (\SList a
xs SList a
ys SBV a
_e -> (SInteger, SInteger) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
xs, SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
ys)) ((Proof
    (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
  -> StepArgs
       (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
       Integer)
 -> TP
      (Proof
         (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)))
-> (Proof
      (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
    -> StepArgs
         (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
         Integer)
-> TP
     (Proof
        (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool))
forall a b. (a -> b) -> a -> b
$
                \Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool)
ih SList a
as SList a
bs SBV a
e -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- (SList a, SList a)
-> TPProofRaw SInteger
-> ((SBV a, SList a) -> TPProofRaw SInteger)
-> ((SBV a, SList a) -> TPProofRaw SInteger)
-> ((SBV a, SList a) -> (SBV a, SList a) -> TPProofRaw SInteger)
-> TPProofRaw SInteger
forall a b r.
(SymVal a, SymVal b) =>
(SList a, SList b)
-> TPProofRaw r
-> ((SBV b, SList b) -> TPProofRaw r)
-> ((SBV a, SList a) -> TPProofRaw r)
-> ((SBV a, SList a) -> (SBV b, SList b) -> TPProofRaw r)
-> TPProofRaw r
split2 (SList a
as, SList a
bs)
                                            TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                            (SBV a, SList a) -> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                            (SBV a, SList a) -> TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                            (\(SBV a
x, SList a
xs) (SBV a
y, SList a
ys) -> SBV a -> SList a -> SInteger
count SBV a
e (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys))
                                                              SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold merge"
                                                              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 (SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
y)
                                                                              (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
xs (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys))
                                                                              (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SList a
ys))
                                                              SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push count inside"
                                                              TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
y)
                                                                     (SBV a -> SList a -> SInteger
count SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
xs (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys)))
                                                                     (SBV a -> SList a -> SInteger
count SBV a
e (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SList a
ys))
                                                              SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold count, twice"
                                                              TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
y)
                                                                     (let r :: SInteger
r = SBV a -> SList a -> SInteger
count SBV a
e (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge SList a
xs (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys)) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
x) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                                     (let r :: SInteger
r = SBV a -> SList a -> SInteger
count SBV a
e (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SList a
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
y) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                              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)
ih 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
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys), 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
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
y)
                                                                     (let r :: SInteger
r = 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 (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
x) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                                     (let r :: SInteger
r = SBV a -> SList a -> SInteger
count SBV a
e (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SList a
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
y) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                              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)
ih 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" (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList a
ys, 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
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
y)
                                                                     (let r :: SInteger
r = 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 (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
x) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                                     (let r :: SInteger
r = SBV a -> SList a -> SInteger
count SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: 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 in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
y) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                              SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold count in reverse, twice"
                                                              TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
x SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
y)
                                                                     (SBV a -> SList a -> SInteger
count SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV a -> SList a -> SInteger
count SBV a
e (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys))
                                                                     (SBV a -> SList a -> SInteger
count SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV a -> SList a -> SInteger
count SBV a
e (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys))
                                                              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 (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV a -> SList a -> SInteger
count SBV a
e (SBV a
y SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
ys)
                                                              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] -> Forall "e" a -> SBool)
sortIsPermutation <-
        SMTConfig
-> 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)) =>
SMTConfig
-> 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)) =>
SMTConfig
-> 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))
sInductWith SMTConfig
cvc5 String
"sortIsPermutation"
                (\(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
mergeSort SList a
xs))
                (\SList a
xs SBV a
_e -> 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
as SBV a
e -> [] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw 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
as
                                        TPProofRaw SInteger
forall a. Trivial a => a
trivial
                                        (\SBV a
x SList a
xs -> SBV a -> SList a -> SInteger
count SBV a
e (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs))
                                               SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold mergeSort"
                                               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 (SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1)
                                                               (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                                                               (let (SList a
h1, SList a
h2) = SInteger -> SList a -> (SList a, SList a)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                                                                in SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h1) (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h2)))
                                               SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push count down, simplify, rearrange"
                                               TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList a
h1, SList a
h2) = SInteger -> SList a -> (SList a, SList a)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                                               in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                      (SBV a -> SList a -> SInteger
count SBV a
e [Item (SList a)
SBV a
x])
                                                      (SBV a -> SList a -> SInteger
count SBV a
e (SList a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a -> SList a
merge (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h1) (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h2)))
                                               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)
mergeCount 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
mergeSort SList a
h1), 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
mergeSort SList a
h2), 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
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                      (SBV a -> SList a -> SInteger
count SBV a
e [Item (SList a)
SBV a
x])
                                                      (SBV a -> SList a -> SInteger
count SBV a
e (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
h1) 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
mergeSort SList a
h2))
                                               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
h1, 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
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                      (SBV a -> SList a -> SInteger
count SBV a
e [Item (SList a)
SBV a
x])
                                                      (SBV a -> SList a -> SInteger
count SBV a
e SList a
h1 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
mergeSort SList a
h2))
                                               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
h2, 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
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                      (SBV a -> SList a -> SInteger
count SBV a
e [Item (SList a)
SBV a
x])
                                                      (SBV a -> SList a -> SInteger
count SBV a
e SList a
h1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SBV a -> SList a -> SInteger
count SBV a
e SList a
h2)
                                               SInteger -> Proof Bool -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool)
takeDropCount Proof
  (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool)
-> IArgs
     (Forall "xs" [a] -> Forall "n" Integer -> 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" (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2), 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
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
xs)
                                                      (SBV a -> SList a -> SInteger
count SBV a
e [Item (SList a)
SBV a
x])
                                                      (SBV a -> SList a -> SInteger
count SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: 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)

    --------------------------------------------------------------------------------------------
    -- Put the two parts together for the final proof
    --------------------------------------------------------------------------------------------
    String
-> (Forall "xs" [a] -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"mergeSortIsCorrect"
          (\(Forall SList a
xs) -> let out :: SList a
out = SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
mergeSort SList a
xs in SList a -> SBool
nonDecreasing SList a
out SBool -> SBool -> SBool
.&& SList a -> SList a -> SBool
isPermutation SList a
xs SList a
out)
          [Proof (Forall "xs" [a] -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "xs" [a] -> SBool)
sortNonDecreasing, Proof (Forall "xs" [a] -> Forall "e" a -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
sortIsPermutation]