-----------------------------------------------------------------------------
-- |
-- 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 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.
-- Lemma: nonDecTail                                 Q.E.D.
-- Inductive lemma (strong): mergeKeepsSort
--   Base: mergeKeepsSort.Base                       Q.E.D.
--   Step: 1                                         Q.E.D.
--   Step: 2                                         Q.E.D.
--   Asms: 3                                         Q.E.D.
--   Step: 3                                         Q.E.D.
--   Asms: 4                                         Q.E.D.
--   Step: 4                                         Q.E.D.
--   Asms: 5                                         Q.E.D.
--   Step: 5                                         Q.E.D.
--   Asms: 6                                         Q.E.D.
--   Step: 6                                         Q.E.D.
--   Step: 7                                         Q.E.D.
--   Step: mergeKeepsSort.Step                       Q.E.D.
-- Inductive lemma (strong): sortNonDecreasing
--   Base: sortNonDecreasing.Base                    Q.E.D.
--   Step: 1                                         Q.E.D.
--   Step: 2                                         Q.E.D.
--   Step: 3                                         Q.E.D.
--   Step: 4                                         Q.E.D.
--   Step: sortNonDecreasing.Step                    Q.E.D.
-- Inductive lemma (strong): mergeCount
--   Base: mergeCount.Base                           Q.E.D.
--   Step: 1                                         Q.E.D.
--   Step: 2                                         Q.E.D.
--   Step: 3                                         Q.E.D.
--   Step: 4                                         Q.E.D.
--   Step: 5                                         Q.E.D.
--   Step: 6                                         Q.E.D.
--   Step: 7                                         Q.E.D.
--   Step: mergeCount.Step                           Q.E.D.
-- Inductive lemma: countAppend
--   Base: countAppend.Base                          Q.E.D.
--   Step: 1                                         Q.E.D.
--   Step: 2                                         Q.E.D.
--   Step: 3                                         Q.E.D.
--   Step: 4                                         Q.E.D.
--   Step: countAppend.Step                          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
--   Base: sortIsPermutation.Base                    Q.E.D.
--   Step: 1                                         Q.E.D.
--   Step: 2                                         Q.E.D.
--   Step: 3                                         Q.E.D.
--   Step: 4                                         Q.E.D.
--   Step: 5                                         Q.E.D.
--   Step: 6                                         Q.E.D.
--   Step: sortIsPermutation.Step                    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 = 50}} (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))
                         []

    nonDecrTail <- lemma "nonDecTail"
                         (\(Forall @"x" SInteger
x) (Forall @"xs" SList Integer
xs) -> SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SBool -> SBool -> SBool
.=> SList Integer -> SBool
nonDecreasing SList Integer
xs)
                         []

    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)) $
               \Proof
ih SInteger
x SList Integer
xs SInteger
y SList Integer
ys -> [SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs), SList Integer -> SBool
nonDecreasing (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys)]
                             [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList Integer -> SBool
nonDecreasing (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))
                             SBool -> String -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"unfold merge"
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep 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
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))
                             SBool -> String -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"push nonDecreasing down"
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                    (SList Integer -> SBool
nonDecreasing (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)))
                                    (SList Integer -> SBool
nonDecreasing (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))
                             SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [ Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ 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
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (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)))
                                , SBool -> Helper
hyp  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                , SBool -> Helper
hyp  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer -> SBool
nonDecreasing (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys)
                                ]
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                    (SList Integer -> SBool
nonDecreasing (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)))
                                    (SList Integer -> SBool
nonDecreasing (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))
                             SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [ Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ 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
y, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"ys" (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))
                                , SBool -> Helper
hyp  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                , SBool -> Helper
hyp  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer -> SBool
nonDecreasing (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys)
                                ]
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                    (SList Integer -> SBool
nonDecreasing (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)))
                                    (SList Integer -> SBool
nonDecreasing (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))
                             SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [ Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ 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
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))
                                , Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
nonDecrTail Proof -> (Inst "x" Integer, Inst "xs" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x,   forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
xs)
                                , SBool -> Helper
hyp  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer -> SBool
nonDecreasing (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys)
                                , SBool -> Helper
hyp  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                ]
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y)
                                    SBool
sTrue
                                    (SList Integer -> SBool
nonDecreasing (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))
                             SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [ Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ 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
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)
                                , Proof -> Helper
hprf (Proof -> Helper) -> Proof -> Helper
forall a b. (a -> b) -> a -> b
$ Proof
nonDecrTail Proof -> (Inst "x" Integer, Inst "xs" [Integer]) -> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x"  SInteger
y,         forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" SList Integer
ys)
                                , SBool -> Helper
hyp  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer -> SBool
nonDecreasing (SInteger
y SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
ys)
                                , SBool -> Helper
hyp  (SBool -> Helper) -> SBool -> Helper
forall a b. (a -> b) -> a -> b
$ SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                ]
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
y) SBool
sTrue SBool
sTrue
                             SBool -> String -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"simplify"
                             ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep 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
=: [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep a]
qed

    sortNonDecreasing <-
        sInduct "sortNonDecreasing"
                (\(Forall @"xs" SList Integer
xs) -> SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer
mergeSort SList Integer
xs)) $
                \Proof
ih SInteger
x SList Integer
xs -> [] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList Integer -> SBool
nonDecreasing (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))
                               SBool -> String -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"unfold"
                               ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep 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
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 -> 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
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)
                                                     (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 -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"push nonDecreasing down"
                               ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep 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
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)
                                      (SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs))
                                      (SList Integer -> 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 -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep 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
xs
                               ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep 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
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)
                                      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] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep 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))
                                  ]
                               ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep 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
=: [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep 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) $
                \Proof
ih SInteger
x SList Integer
xs SInteger
y SList Integer
ys SInteger
e -> [] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"unfold merge"
                                      ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"push count inside"
                                      ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"unfold count, twice"
                                      ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep 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)
                                      ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep 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)
                                      ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"unfold count in reverse, twice"
                                      ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"simplify"
                                      ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep 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] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"unfold count"
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep 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)
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"simplify"
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep 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] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep 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)
                          ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
takeDrop
                          ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep a]
qed

    sortIsPermutation <-
        sInduct "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)) $
                \Proof
ih SInteger
x SList Integer
xs SInteger
e -> [] [SBool] -> [ProofStep SInteger] -> (SBool, [ProofStep SInteger])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"unfold mergeSort"
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"push count down, simplify, rearrange"
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep 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)
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep 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)
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep 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)
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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 -> ProofStep SInteger
forall a b. ProofHint a b => a -> b -> ProofStep 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)
                                 ProofStep SInteger
-> ChainsTo (ProofStep SInteger) -> ChainsTo (ProofStep 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
=: [ProofStep SInteger]
ChainsTo SInteger
forall a. [ProofStep 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]