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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.MergeSort where

import Data.SBV
import Data.SBV.Tools.KnuckleDragger

import Prelude hiding (null, length, head, tail, elem, splitAt, (++), take, drop)
import Data.SBV.List

-- * Merge sort

-- | Merge two already sorted lists into another
merge :: SList Integer -> SList Integer -> SList Integer
merge :: SList Integer -> SList Integer -> SList Integer
merge = String
-> (SList Integer -> SList Integer -> SList Integer)
-> SList Integer
-> SList Integer
-> SList Integer
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"merge" ((SList Integer -> SList Integer -> SList Integer)
 -> SList Integer -> SList Integer -> SList Integer)
-> (SList Integer -> SList Integer -> SList Integer)
-> SList Integer
-> SList Integer
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SList Integer
l SList Integer
r -> SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l) SList Integer
r
                                    (SList Integer -> SList Integer) -> SList Integer -> SList Integer
forall a b. (a -> b) -> a -> b
$ SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
r) SList Integer
l
                                    (SList Integer -> SList Integer) -> SList Integer -> SList Integer
forall a b. (a -> b) -> a -> b
$ let (SInteger
a, SList Integer
as) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l
                                          (SInteger
b, SList Integer
bs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
r
                                      in SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
b) (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge SList Integer
as SList Integer
r) (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge SList Integer
l SList Integer
bs)

-- | Merge sort, using 'merge' above to successively sort halved input
mergeSort :: SList Integer -> SList Integer
mergeSort :: SList Integer -> SList Integer
mergeSort = String
-> (SList Integer -> SList Integer)
-> SList Integer
-> SList Integer
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"mergeSort" ((SList Integer -> SList Integer)
 -> SList Integer -> SList Integer)
-> (SList Integer -> SList Integer)
-> SList Integer
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SList Integer
l -> SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
l SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1) SList Integer
l
                                              (SList Integer -> SList Integer) -> SList Integer -> SList Integer
forall a b. (a -> b) -> a -> b
$ let (SList Integer
h1, SList Integer
h2) = SInteger -> SList Integer -> (SList Integer, SList Integer)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
l SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) SList Integer
l
                                                in SList Integer -> SList Integer -> SList Integer
merge (SList Integer -> SList Integer
mergeSort SList Integer
h1) (SList Integer -> SList Integer
mergeSort SList Integer
h2)
-- * Helper functions

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

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

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

-- * Correctness proof

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

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

    nonDecrIns <- String
-> (Forall "x" Integer -> Forall "ys" [Integer] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"nonDecrInsert"
                        (\(Forall @"x" SInteger
x) (Forall @"ys" SList Integer
ys) -> SList Integer -> SBool
nonDecreasing SList Integer
ys SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
ys) SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList Integer -> SInteger
forall a. SymVal a => SList a -> SBV a
head SList Integer
ys
                                                           SBool -> SBool -> SBool
.=> SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys))
                        []

    mergeKeepsSort <-
        sInductWith cvc5 "mergeKeepsSort"
           (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) -> SList Integer -> SBool
nonDecreasing SList Integer
xs SBool -> SBool -> SBool
.&& SList Integer -> SBool
nonDecreasing SList Integer
ys SBool -> SBool -> SBool
.=> SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer -> SList Integer
merge SList Integer
xs SList Integer
ys))
           (\(SList Integer
xs :: SList Integer) (SList Integer
ys :: SList Integer) -> (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs, SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
ys)) $
           \Proof
ih SList Integer
xs SList Integer
ys -> [SList Integer -> SBool
nonDecreasing SList Integer
xs, SList Integer -> SBool
nonDecreasing SList Integer
ys]
                     [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- (SList Integer, SList Integer)
-> KDProofRaw SBool
-> ((SInteger, SList Integer) -> KDProofRaw SBool)
-> ((SInteger, SList Integer) -> KDProofRaw SBool)
-> ((SInteger, SList Integer)
    -> (SInteger, SList Integer) -> KDProofRaw SBool)
-> KDProofRaw SBool
forall a b r.
(SymVal a, SymVal b) =>
(SList a, SList b)
-> KDProofRaw r
-> ((SBV b, SList b) -> KDProofRaw r)
-> ((SBV a, SList a) -> KDProofRaw r)
-> ((SBV a, SList a) -> (SBV b, SList b) -> KDProofRaw r)
-> KDProofRaw r
split2 (SList Integer
xs, SList Integer
ys)
                               KDProofRaw SBool
forall a. Trivial a => a
trivial           -- when both xs and ys are empty.  Trivial.
                               (SInteger, SList Integer) -> KDProofRaw SBool
forall a. Trivial a => a
trivial           -- when xs is empty, but ys isn't. Trivial.
                               (SInteger, SList Integer) -> KDProofRaw SBool
forall a. Trivial a => a
trivial           -- when ys is empty, but xs isn't. Trivial.
                               (\(SInteger
a, SList Integer
as) (SInteger
b, SList Integer
bs) ->
                                     SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer -> SList Integer
merge (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as) (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs))
                                  SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold merge"
                                  KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SBool
nonDecreasing (SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
b)
                                                        (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge SList Integer
as (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs))
                                                        (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as) SList Integer
bs))
                                  SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"case split"
                                  KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
b SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SList Integer -> SBool
nonDecreasing (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge SList Integer
as (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs))
                                                      SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
ih         Proof -> (Inst "xs" [Integer], Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
as, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs))
                                                         , Proof
nonDecrIns Proof -> (Inst "x" Integer, Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
a, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SList Integer -> SList Integer -> SList Integer
merge SList Integer
as (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
bs)))
                                                         ]
                                                      KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                      SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                           , SInteger
a SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
b  SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SList Integer -> SBool
nonDecreasing (SInteger
b SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as) SList Integer
bs)
                                                      SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
ih         Proof -> (Inst "xs" [Integer], Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
bs)
                                                         , Proof
nonDecrIns Proof -> (Inst "x" Integer, Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
b, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SList Integer -> SList Integer -> SList Integer
merge (SInteger
a SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
as) SList Integer
bs))
                                                         ]
                                                      KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                      SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                           ])

    sortNonDecreasing <-
        sInduct "sortNonDecreasing"
                (\(Forall @"xs" SList Integer
xs) -> SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer
mergeSort SList Integer
xs))
                (length @Integer) $
                \Proof
ih SList Integer
xs -> [] [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer
-> KDProofRaw SBool
-> (SInteger -> SList Integer -> KDProofRaw SBool)
-> KDProofRaw SBool
forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList Integer
xs
                                      KDProofRaw SBool
forall a. KDProofRaw a
qed
                                      (\SInteger
e SList Integer
es -> SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer
mergeSort (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es))
                                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold"
                                             KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList Integer
h1, SList Integer
h2) = SInteger -> SList Integer -> (SList Integer, SList Integer)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es)
                                                in SList Integer -> SBool
nonDecreasing (SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1)
                                                                      (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es)
                                                                      (SList Integer -> SList Integer -> SList Integer
merge (SList Integer -> SList Integer
mergeSort SList Integer
h1) (SList Integer -> SList Integer
mergeSort SList Integer
h2)))
                                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push nonDecreasing down"
                                             KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1)
                                                    (SList Integer -> SBool
nonDecreasing (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es))
                                                    (SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer -> SList Integer
merge (SList Integer -> SList Integer
mergeSort SList Integer
h1) (SList Integer -> SList Integer
mergeSort SList Integer
h2)))
                                             SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
es
                                             KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
es) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1)
                                                    SBool
sTrue
                                                    (SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer -> SList Integer
merge (SList Integer -> SList Integer
mergeSort SList Integer
h1) (SList Integer -> SList Integer
mergeSort SList Integer
h2)))
                                             SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
ih Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
h1
                                                , Proof
ih Proof -> Inst "xs" [Integer] -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
h2
                                                , Proof
mergeKeepsSort Proof -> (Inst "xs" [Integer], Inst "ys" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList Integer -> SList Integer
mergeSort SList Integer
h1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SList Integer -> SList Integer
mergeSort SList Integer
h2))
                                                ]
                                             KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed)

    --------------------------------------------------------------------------------------------
    -- Part II. Prove that the output of merge sort is a permuation of its input
    --------------------------------------------------------------------------------------------
    mergeCount <-
        sInduct "mergeCount"
                (\(Forall @"xs" SList Integer
xs) (Forall @"ys" SList Integer
ys) (Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer -> SList Integer
merge SList Integer
xs SList Integer
ys) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
ys)
                (\(SList Integer
xs :: SList Integer) (SList Integer
ys :: SList Integer) (SInteger
_e :: SInteger) -> (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs, SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
ys)) $
                \Proof
ih SList Integer
as SList Integer
bs SInteger
e -> [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|-
                        (SList Integer, SList Integer)
-> KDProofRaw SInteger
-> ((SInteger, SList Integer) -> KDProofRaw SInteger)
-> ((SInteger, SList Integer) -> KDProofRaw SInteger)
-> ((SInteger, SList Integer)
    -> (SInteger, SList Integer) -> KDProofRaw SInteger)
-> KDProofRaw SInteger
forall a b r.
(SymVal a, SymVal b) =>
(SList a, SList b)
-> KDProofRaw r
-> ((SBV b, SList b) -> KDProofRaw r)
-> ((SBV a, SList a) -> KDProofRaw r)
-> ((SBV a, SList a) -> (SBV b, SList b) -> KDProofRaw r)
-> KDProofRaw r
split2 (SList Integer
as, SList Integer
bs)
                               KDProofRaw SInteger
forall a. Trivial a => a
trivial
                               (SInteger, SList Integer) -> KDProofRaw SInteger
forall a. Trivial a => a
trivial
                               (SInteger, SList Integer) -> KDProofRaw SInteger
forall a. Trivial a => a
trivial
                               (\(SInteger
x, SList Integer
xs) (SInteger
y, SList Integer
ys) -> SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer -> SList Integer
merge (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys))
                                                 SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold merge"
                                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                                                 (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge SList Integer
xs (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys))
                                                                 (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer
ys))
                                                 SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push count inside"
                                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw 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 (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                                        (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge SList Integer
xs (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys)))
                                                        (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer -> SList Integer -> SList Integer
merge (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer
ys))
                                                 SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold count, twice"
                                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw 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 (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                                        (let r :: SInteger
r = SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer -> SList Integer
merge SList Integer
xs (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys)) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                        (let r :: SInteger
r = SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer -> SList Integer
merge (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
y) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                 SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer], Inst "e" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                                        (let r :: SInteger
r = SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                        (let r :: SInteger
r = SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer -> SList Integer
merge (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
y) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                 SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer], Inst "e" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" SList Integer
ys, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw 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 (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                                        (let r :: SInteger
r = SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys) in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x) (SInteger
1SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
r) SInteger
r)
                                                        (let r :: SInteger
r = SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
ys in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
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"
                                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw 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 (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                                        (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys))
                                                        (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys))
                                                 SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                                 KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys)
                                                 SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed)

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

    takeDropCount <- do

       takeDrop <- lemma "take_drop"
                         (\(Forall @"n" SInteger
n) (Forall @"xs" (SList Integer
xs :: SList Integer)) -> SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList Integer
xs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
xs)
                         []

       calc "takeDropCount"
            (\(Forall @"xs" SList Integer
xs) (Forall @"n" SInteger
n) (Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList Integer
xs) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs) $
            \SList Integer
xs SInteger
n SInteger
e -> [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList Integer
xs) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList Integer
xs)
                          SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
countAppend Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer], Inst "e" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList Integer
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList Integer
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                          KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList Integer
xs)
                          SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
takeDrop
                          KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs
                          SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed

    sortIsPermutation <-
        sInductWith cvc5 "sortIsPermutation"
                (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
mergeSort SList Integer
xs))
                (\(SList Integer
xs :: SList Integer) (SInteger
_e :: SInteger) -> SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList Integer
xs) $
                \Proof
ih SList Integer
as SInteger
e -> [] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SList Integer
-> KDProofRaw SInteger
-> (SInteger -> SList Integer -> KDProofRaw SInteger)
-> KDProofRaw SInteger
forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList Integer
as
                                        KDProofRaw SInteger
forall a. KDProofRaw a
qed
                                        (\SInteger
x SList Integer
xs -> SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
mergeSort (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs))
                                               SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold mergeSort"
                                               KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SInteger
count SInteger
e (SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
1)
                                                               (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                                               (let (SList Integer
h1, SList Integer
h2) = SInteger -> SList Integer -> (SList Integer, SList Integer)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                                                in SList Integer -> SList Integer -> SList Integer
merge (SList Integer -> SList Integer
mergeSort SList Integer
h1) (SList Integer -> SList Integer
mergeSort SList Integer
h2)))
                                               SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push count down, simplify, rearrange"
                                               KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let (SList Integer
h1, SList Integer
h2) = SInteger -> SList Integer -> (SList Integer, SList Integer)
forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                               in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs)
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
x))
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer -> SList Integer
merge (SList Integer -> SList Integer
mergeSort SList Integer
h1) (SList Integer -> SList Integer
mergeSort SList Integer
h2)))
                                               SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
mergeCount Proof
-> (Inst "xs" [Integer], Inst "ys" [Integer], Inst "e" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList Integer -> SList Integer
mergeSort SList Integer
h1), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (SList Integer -> SList Integer
mergeSort SList Integer
h2), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                               KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs)
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
x))
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
mergeSort SList Integer
h1) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
mergeSort SList Integer
h2))
                                               SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof -> (Inst "xs" [Integer], Inst "e" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
h1, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                               KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs)
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
x))
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
h1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e (SList Integer -> SList Integer
mergeSort SList Integer
h2))
                                               SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
ih Proof -> (Inst "xs" [Integer], Inst "e" Integer) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
h2, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                               KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs)
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
x))
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
h1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger -> SList Integer -> SInteger
count SInteger
e SList Integer
h2)
                                               SInteger -> Proof -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
takeDropCount Proof
-> (Inst "xs" [Integer], Inst "n" Integer, Inst "e" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"n" (SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
length (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
e)
                                               KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
xs)
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
x))
                                                      (SInteger -> SList Integer -> SInteger
count SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs))
                                               SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed)

    --------------------------------------------------------------------------------------------
    -- Put the two parts together for the final proof
    --------------------------------------------------------------------------------------------
    lemma "mergeSortIsCorrect"
          (\(Forall @"xs" SList Integer
xs) -> let out :: SList Integer
out = SList Integer -> SList Integer
mergeSort SList Integer
xs in SList Integer -> SBool
nonDecreasing SList Integer
out SBool -> SBool -> SBool
.&& SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs SList Integer
out)
          [sortNonDecreasing, sortIsPermutation]