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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.InsertionSort where

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

import Prelude hiding (null, length, head, tail, elem)
import Data.SBV.List

-- * Insertion sort

-- | Insert an element into an already sorted list in the correct place.
insert :: SInteger -> SList Integer -> SList Integer
insert :: SInteger -> SList Integer -> SList Integer
insert = String
-> (SInteger -> SList Integer -> SList Integer)
-> SInteger
-> SList Integer
-> SList Integer
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"insert" ((SInteger -> SList Integer -> SList Integer)
 -> SInteger -> SList Integer -> SList Integer)
-> (SInteger -> SList Integer -> SList Integer)
-> SInteger
-> SList Integer
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SInteger
e SList Integer
l -> SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l) (SInteger -> SList Integer
forall a. SymVal a => SBV a -> SList a
singleton SInteger
e)
                                      (SList Integer -> SList Integer) -> SList Integer -> SList Integer
forall a b. (a -> b) -> a -> b
$ let (SInteger
x, SList Integer
xs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l
                                        in SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs)

-- | Insertion sort, using 'insert' above to successively insert the elements.
insertionSort :: SList Integer -> SList Integer
insertionSort :: SList Integer -> SList Integer
insertionSort = String
-> (SList Integer -> SList Integer)
-> SList Integer
-> SList Integer
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"insertionSort" ((SList Integer -> SList Integer)
 -> SList Integer -> SList Integer)
-> (SList Integer -> SList Integer)
-> SList Integer
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SList Integer
l -> SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l) SList Integer
forall a. SymVal a => SList a
nil
                                                  (SList Integer -> SList Integer) -> SList Integer -> SList Integer
forall a b. (a -> b) -> a -> b
$ let (SInteger
x, SList Integer
xs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l
                                                    in SInteger -> SList Integer -> SList Integer
insert SInteger
x (SList Integer -> SList Integer
insertionSort SList Integer
xs)


-- * 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'

-- | Remove the first occurrence of an number from a list, if any.
removeFirst :: SInteger -> SList Integer -> SList Integer
removeFirst :: SInteger -> SList Integer -> SList Integer
removeFirst = String
-> (SInteger -> SList Integer -> SList Integer)
-> SInteger
-> SList Integer
-> SList Integer
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"removeFirst" ((SInteger -> SList Integer -> SList Integer)
 -> SInteger -> SList Integer -> SList Integer)
-> (SInteger -> SList Integer -> SList Integer)
-> SInteger
-> SList Integer
-> SList Integer
forall a b. (a -> b) -> a -> b
$ \SInteger
e SList Integer
l -> SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
l)
                                                      SList Integer
forall a. SymVal a => SList a
nil
                                                      (let (SInteger
x, SList Integer
xs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l
                                                       in SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x) SList Integer
xs (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
removeFirst SInteger
e SList Integer
xs))

-- | Are two lists permutations of each other?
isPermutation :: SList Integer -> SList Integer -> SBool
isPermutation :: SList Integer -> SList Integer -> SBool
isPermutation = String
-> (SList Integer -> SList Integer -> SBool)
-> SList Integer
-> SList Integer
-> SBool
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"isPermutation" ((SList Integer -> SList Integer -> SBool)
 -> SList Integer -> SList Integer -> SBool)
-> (SList Integer -> SList Integer -> SBool)
-> SList Integer
-> SList Integer
-> SBool
forall a b. (a -> b) -> a -> b
$ \SList Integer
l SList Integer
r -> SBool -> SBool -> SBool -> SBool
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 -> SBool
forall a. SymVal a => SList a -> SBool
null SList Integer
r)
                                                          (let (SInteger
x, SList Integer
xs) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList Integer
l
                                                           in SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
r SBool -> SBool -> SBool
.&& SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs (SInteger -> SList Integer -> SList Integer
removeFirst SInteger
x SList Integer
r))

-- * Correctness proof

-- | Correctness of insertion-sort.
--
-- We have:
--
-- >>> correctness
-- Lemma: nonDecTail                       Q.E.D.
-- Inductive lemma: insertNonDecreasing
--   Base: insertNonDecreasing.Base        Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               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.
--   Step: insertNonDecreasing.Step        Q.E.D.
-- Lemma: insertionSort1                   Q.E.D.
-- Inductive lemma: sortNonDecreasing
--   Base: sortNonDecreasing.Base          Q.E.D.
--   Step: 1                               Q.E.D.
--   Step: 2                               Q.E.D.
--   Step: sortNonDecreasing.Step          Q.E.D.
-- Lemma: elemITE                          Q.E.D.
-- Inductive lemma: insertIsElem
--   Base: insertIsElem.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: insertIsElem.Step               Q.E.D.
-- Inductive lemma: removeAfterInsert
--   Base: removeAfterInsert.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: removeAfterInsert.Step          Q.E.D.
-- Inductive lemma: 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: sortIsPermutation.Step          Q.E.D.
-- Lemma: insertionSortIsCorrect           Q.E.D.
-- [Proven] insertionSortIsCorrect
correctness :: IO Proof
correctness :: IO Proof
correctness = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do

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

    nonDecrTail <- String
-> (Forall "x" Integer -> Forall "xs" [Integer] -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"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)
                         []

    insertNonDecreasing <-
        induct "insertNonDecreasing"
               (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) -> SList Integer -> SBool
nonDecreasing SList Integer
xs SBool -> SBool -> SBool
.=> SList Integer -> SBool
nonDecreasing (SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs)) $
               \Proof
ih SInteger
x SList Integer
xs SInteger
e -> [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] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SList Integer -> SBool
nonDecreasing (SInteger -> SList Integer -> SList Integer
insert SInteger
e (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 insert"
                          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
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                          SBool -> String -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"push nonDecreasing over the ite"
                          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
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SList Integer -> SBool
nonDecreasing (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: 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
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                          SBool -> String -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? String
"unfold nonDecreasing, simplify"
                          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
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x)
                                 (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
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                          SBool -> SBool -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
??  SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                          ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
x SBool -> SBool -> SBool
.=> SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                          SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [ SBool -> Helper
hyp  (SList Integer -> SBool
nonDecreasing (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs))
                             , Proof -> Helper
hprf (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" (SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs)))
                             , Proof -> Helper
hprf Proof
ih
                             ]
                          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


    -- Unfolding insertion sort just once. This helps z3, which otherwise gets stuck in the following proof.
    is1 <- lemma "insertionSort1" (\(Forall @"x" SInteger
x) (Forall @"xs" SList Integer
xs) -> SList Integer -> SList Integer
insertionSort (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SList Integer -> SList Integer
insert SInteger
x (SList Integer -> SList Integer
insertionSort SList Integer
xs)) []

    sortNonDecreasing <-
        induct "sortNonDecreasing"
               (\(Forall @"xs" SList Integer
xs) -> SList Integer -> SBool
nonDecreasing (SList Integer -> SList Integer
insertionSort 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
insertionSort (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs))
                              -- Surprisingly, z3 really needs to be told how to instantiate is1 below so it doesn't get stuck.
                              SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
is1 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)
                              ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SBool
nonDecreasing (SInteger -> SList Integer -> SList Integer
insert SInteger
x (SList Integer -> SList Integer
insertionSort SList Integer
xs))
                              SBool -> [Helper] -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? [ Proof -> Helper
hprf (Proof
insertNonDecreasing 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 -> SList Integer
insertionSort SList Integer
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SInteger
x))
                                , Proof -> Helper
hprf Proof
ih
                                ]
                              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 insertion sort is a permuation of its input
    --------------------------------------------------------------------------------------------

    -- For whatever reason z3 can't figure this out in the below proof. This helper isn't needed for CVC5.
    -- Note that z3 is able to prove this out-of-the box without any helpers, but needs it in the next as a helper.
    elemITE <- lemma "elemITE" (\(Forall @"x" (SInteger
x :: SInteger)) (Forall @"c" SBool
c) (Forall @"t" SList Integer
t) (Forall @"e" SList Integer
e)
                                        -> SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
c SList Integer
t SList Integer
e SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
c (SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
t) (SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList Integer
e))
                     []

    insertIsElem <-
        induct "insertIsElem"
               (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) -> SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs) $
               \Proof
ih SInteger
x SList Integer
xs SInteger
e -> [] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SInteger -> SList Integer -> SList Integer
insert SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs)
                                -- z3 has hard time making the following step (though cvc5 is OK with it)
                                SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
elemITE Proof
-> (Inst "x" Integer, Inst "c" Bool, Inst "t" [Integer],
    Inst "e" [Integer])
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
e, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"c" (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"t" (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: 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 @"e" (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e 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
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)) (SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                                SBool -> ChainsTo SBool -> ChainsTo 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
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) SBool
sTrue (SInteger
e SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs) SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                                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

    removeAfterInsert <-
        induct "removeAfterInsert"
               (\(Forall @"xs" SList Integer
xs) (Forall @"e" SInteger
e) -> SInteger -> SList Integer -> SList Integer
removeFirst SInteger
e (SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs) SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
xs) $
               \Proof
ih SInteger
x SList Integer
xs SInteger
e -> [] [SBool]
-> [ProofStep (SList Integer)]
-> (SBool, [ProofStep (SList Integer)])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- SInteger -> SList Integer -> SList Integer
removeFirst SInteger
e (SInteger -> SList Integer -> SList Integer
insert SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs))
                                SList Integer -> String -> ProofStep (SList Integer)
forall a b. ProofHint a b => a -> b -> ProofStep a
??  String
"expand insert"
                                ProofStep (SList Integer)
-> ChainsTo (ProofStep (SList Integer))
-> ChainsTo (ProofStep (SList Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger -> SList Integer -> SList Integer
removeFirst SInteger
e (SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                                SList Integer -> String -> ProofStep (SList Integer)
forall a b. ProofHint a b => a -> b -> ProofStep a
??  String
"push removeFirst down the if-then-else"
                                ProofStep (SList Integer)
-> ChainsTo (ProofStep (SList Integer))
-> ChainsTo (ProofStep (SList Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger -> SList Integer -> SList Integer
removeFirst SInteger
e (SInteger
e SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)) (SInteger -> SList Integer -> SList Integer
removeFirst SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                                SList Integer -> String -> ProofStep (SList Integer)
forall a b. ProofHint a b => a -> b -> ProofStep a
??  String
"unfold removeFirst, then branch"
                                ProofStep (SList Integer)
-> ChainsTo (ProofStep (SList Integer))
-> ChainsTo (ProofStep (SList Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger -> SList Integer -> SList Integer
removeFirst SInteger
e (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                                SList Integer -> String -> ProofStep (SList Integer)
forall a b. ProofHint a b => a -> b -> ProofStep a
??  String
"unfold removeFirst,  else branch. Note that e .== x is False, due to the pre-condition"
                                ProofStep (SList Integer)
-> ChainsTo (ProofStep (SList Integer))
-> ChainsTo (ProofStep (SList Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SInteger -> SList Integer -> SList Integer
removeFirst SInteger
e (SInteger -> SList Integer -> SList Integer
insert SInteger
e SList Integer
xs))
                                SList Integer -> Proof -> ProofStep (SList Integer)
forall a b. ProofHint a b => a -> b -> ProofStep a
??  Proof
ih
                                ProofStep (SList Integer)
-> ChainsTo (ProofStep (SList Integer))
-> ChainsTo (ProofStep (SList Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList Integer -> SList Integer -> SList Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
e SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
x) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs)
                                SList Integer -> String -> ProofStep (SList Integer)
forall a b. ProofHint a b => a -> b -> ProofStep a
??  String
"simplify"
                                ProofStep (SList Integer)
-> ChainsTo (ProofStep (SList Integer))
-> ChainsTo (ProofStep (SList Integer))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs
                                SList Integer
-> ChainsTo (SList Integer) -> ChainsTo (SList Integer)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [ProofStep (SList Integer)]
ChainsTo (SList Integer)
forall a. [ProofStep a]
qed

    sortIsPermutation <-
        induct "sortIsPermutation"
               (\(Forall @"xs" SList Integer
xs) -> SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs (SList Integer -> SList Integer
insertionSort 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 -> SList Integer -> SBool
isPermutation (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SList Integer -> SList Integer
insertionSort (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs))
                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SList Integer -> SBool
isPermutation (SInteger
x SInteger -> SList Integer -> SList Integer
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList Integer
xs) (SInteger -> SList Integer -> SList Integer
insert SInteger
x (SList Integer -> SList Integer
insertionSort SList Integer
xs))
                              SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
x SInteger -> SList Integer -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SInteger -> SList Integer -> SList Integer
insert SInteger
x (SList Integer -> SList Integer
insertionSort SList Integer
xs) SBool -> SBool -> SBool
.&& SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs (SInteger -> SList Integer -> SList Integer
removeFirst SInteger
x (SInteger -> SList Integer -> SList Integer
insert SInteger
x (SList Integer -> SList Integer
insertionSort SList Integer
xs)))
                              SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
insertIsElem
                              ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs (SInteger -> SList Integer -> SList Integer
removeFirst SInteger
x (SInteger -> SList Integer -> SList Integer
insert SInteger
x (SList Integer -> SList Integer
insertionSort SList Integer
xs)))
                              SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
removeAfterInsert
                              ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList Integer -> SList Integer -> SBool
isPermutation SList Integer
xs (SList Integer -> SList Integer
insertionSort SList Integer
xs)
                              SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
?? Proof
ih
                              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

    --------------------------------------------------------------------------------------------
    -- Put the two parts together for the final proof
    --------------------------------------------------------------------------------------------
    lemma "insertionSortIsCorrect"
          (\(Forall @"xs" SList Integer
xs) -> let out :: SList Integer
out = SList Integer -> SList Integer
insertionSort 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]