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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.InsertionSort where

import Prelude hiding (null, length, head, tail, elem)

import Data.SBV
import Data.SBV.List
import Data.SBV.TP

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

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

-- * Insertion sort

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

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


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

-- | Are two lists permutations of each other? Note that we diverge from the counting
-- based definition of permutation here, since this variant works better with insertion sort.
isPermutation :: (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation = String
-> (SList a -> SList a -> SBool) -> SList a -> SList a -> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"isPermutation" ((SList a -> SList a -> SBool) -> SList a -> SList a -> SBool)
-> (SList a -> SList a -> SBool) -> SList a -> SList a -> SBool
forall a b. (a -> b) -> a -> b
$ \SList a
l SList a
r -> SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
l)
                                                          (SList a -> SBool
forall a. SymVal a => SList a -> SBool
null SList a
r)
                                                          (let (SBV a
x, SList a
xs) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
l
                                                           in SBV a
x SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList a
r SBool -> SBool -> SBool
.&& SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation SList a
xs (SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
x SList a
r))

-- * Correctness proof

-- | Correctness of insertion-sort. z3 struggles with this, but CVC5 proves it just fine.
--
-- We have:
--
-- >>> correctness @Integer
-- Lemma: nonDecrTail                           Q.E.D.
-- Inductive lemma: insertNonDecreasing
--   Step: Base                                 Q.E.D.
--   Step: 1 (unfold insert)                    Q.E.D.
--   Step: 2 (push nonDecreasing down)          Q.E.D.
--   Step: 3 (unfold simplify)                  Q.E.D.
--   Step: 4                                    Q.E.D.
--   Step: 5                                    Q.E.D.
--   Result:                                    Q.E.D.
-- Inductive lemma: sortNonDecreasing
--   Step: Base                                 Q.E.D.
--   Step: 1 (unfold insertionSort)             Q.E.D.
--   Step: 2                                    Q.E.D.
--   Result:                                    Q.E.D.
-- Inductive lemma: insertIsElem
--   Step: Base                                 Q.E.D.
--   Step: 1                                    Q.E.D.
--   Step: 2                                    Q.E.D.
--   Step: 3                                    Q.E.D.
--   Step: 4                                    Q.E.D.
--   Result:                                    Q.E.D.
-- Inductive lemma: removeAfterInsert
--   Step: Base                                 Q.E.D.
--   Step: 1 (expand insert)                    Q.E.D.
--   Step: 2 (push removeFirst down ite)        Q.E.D.
--   Step: 3 (unfold removeFirst on 'then')     Q.E.D.
--   Step: 4 (unfold removeFirst on 'else')     Q.E.D.
--   Step: 5                                    Q.E.D.
--   Step: 6 (simplify)                         Q.E.D.
--   Result:                                    Q.E.D.
-- Inductive lemma: sortIsPermutation
--   Step: Base                                 Q.E.D.
--   Step: 1                                    Q.E.D.
--   Step: 2                                    Q.E.D.
--   Step: 3                                    Q.E.D.
--   Step: 4                                    Q.E.D.
--   Step: 5                                    Q.E.D.
--   Result:                                    Q.E.D.
-- Lemma: insertionSortIsCorrect                Q.E.D.
-- [Proven] insertionSortIsCorrect :: Ɐxs ∷ [Integer] → Bool
correctness :: forall a. (Ord a, SymVal a) => IO (Proof (Forall "xs" [a] -> SBool))
correctness :: forall a.
(Ord a, SymVal a) =>
IO (Proof (Forall "xs" [a] -> SBool))
correctness = SMTConfig
-> TP (Proof (Forall "xs" [a] -> SBool))
-> IO (Proof (Forall "xs" [a] -> SBool))
forall a. SMTConfig -> TP a -> IO a
runTPWith (Int -> SMTConfig -> SMTConfig
tpRibbon Int
45 SMTConfig
cvc5) (TP (Proof (Forall "xs" [a] -> SBool))
 -> IO (Proof (Forall "xs" [a] -> SBool)))
-> TP (Proof (Forall "xs" [a] -> SBool))
-> IO (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$ do

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

    Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
nonDecrTail <- forall a.
(Ord a, SymVal a) =>
TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
SH.nonDecrTail @a

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

    Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
insertNonDecreasing <-
        String
-> (Forall "xs" [a] -> Forall "e" a -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "e" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "e" a -> SBool) Bool)
-> TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> Forall "e" a -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> Forall "e" a -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "e" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "e" a -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"insertNonDecreasing"
               (\(Forall SList a
xs) (Forall SBV a
e) -> SList a -> SBool
nonDecreasing SList a
xs SBool -> SBool -> SBool
.=> SList a -> SBool
nonDecreasing (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs)) ((Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
  -> IHArg (Forall "xs" [a] -> Forall "e" a -> SBool)
  -> IStepArgs (Forall "xs" [a] -> Forall "e" a -> SBool) Bool)
 -> TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "e" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "e" a -> SBool) Bool)
-> TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
forall a b. (a -> b) -> a -> b
$
               \Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
ih (SBV a
x, SList a
xs) SBV a
e -> [SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)]
                             [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SBool
nonDecreasing (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs))
                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold insert"
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBool
nonDecreasing (SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
x) (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push nonDecreasing down"
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
x) (SList a -> SBool
nonDecreasing (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs))
                                              (SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                             SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold simplify"
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
x)
                                    (SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs))
                                    (SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                             SBool -> SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                             TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV a
x SBool -> SBool -> SBool
.=> SList a -> SBool
nonDecreasing (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                             SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
nonDecrTail Proof (Forall "x" a -> Forall "xs" [a] -> SBool)
-> IArgs (Forall "x" a -> Forall "xs" [a] -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SBV a
x, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                             TPProofRaw SBool
-> Proof (Forall "e" a -> SBool) -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
Proof (Forall "e" a -> SBool)
ih
                             Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                             SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed

    Proof (Forall "xs" [a] -> SBool)
sortNonDecreasing <-
        String
-> (Forall "xs" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) Bool)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sortNonDecreasing"
               (\(Forall @"xs" SList a
xs) -> SList a -> SBool
nonDecreasing (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs)) ((Proof (IHType (Forall "xs" [a] -> SBool))
  -> IHArg (Forall "xs" [a] -> SBool)
  -> IStepArgs (Forall "xs" [a] -> SBool) Bool)
 -> TP (Proof (Forall "xs" [a] -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) Bool)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
               \Proof (IHType (Forall "xs" [a] -> SBool))
ih (SBV a
x, SList a
xs) -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SBool
nonDecreasing (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs))
                                 SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold insertionSort"
                                 TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SBool
nonDecreasing (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
x (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs))
                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
insertNonDecreasing Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
-> IArgs (Forall "xs" [a] -> Forall "e" a -> SBool) -> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"xs" (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs), forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"e" SBV a
x)
                                 TPProofRaw SBool -> Proof SBool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "xs" [a] -> SBool))
ih
                                 Hinted (TPProofRaw SBool)
-> ChainsTo (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (TPProofRaw SBool))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed

    --------------------------------------------------------------------------------------------
    -- Part III. Prove that the output of insertion sort is a permuation of its input
    --------------------------------------------------------------------------------------------

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

    Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
removeAfterInsert <-
        String
-> (Forall "xs" [a] -> Forall "e" a -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "e" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "e" a -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> Forall "e" a -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> Forall "e" a -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "e" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "e" a -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"removeAfterInsert"
               (\(Forall @"xs" SList a
xs) (Forall @"e" (SBV a
e :: SBV a)) -> SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
e (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs) SList a -> SList a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList a
xs) ((Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
  -> IHArg (Forall "xs" [a] -> Forall "e" a -> SBool)
  -> IStepArgs (Forall "xs" [a] -> Forall "e" a -> SBool) [a])
 -> TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
    -> IHArg (Forall "xs" [a] -> Forall "e" a -> SBool)
    -> IStepArgs (Forall "xs" [a] -> Forall "e" a -> SBool) [a])
-> TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
forall a b. (a -> b) -> a -> b
$
               \Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
ih (SBV a
x, SList a
xs) SBV a
e ->
                   [] [SBool] -> TPProofRaw (SList a) -> (SBool, TPProofRaw (SList a))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
e (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs))
                      SList a -> String -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"expand insert"
                      TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
e (SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
x) (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                      SList a -> String -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push removeFirst down ite"
                      TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
x) (SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
e (SBV a
e SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)) (SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                      SList a -> String -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold removeFirst on 'then'"
                      TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
x) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) (SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
e (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                      SList a -> String -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold removeFirst on 'else'"
                      TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
x) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
e (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
e SList a
xs))
                      SList a -> Proof (Forall "e" a -> SBool) -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (IHType (Forall "xs" [a] -> Forall "e" a -> SBool))
Proof (Forall "e" a -> SBool)
ih
                      TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
e SBV a -> SBV a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV a
x) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs)
                      SList a -> String -> Hinted (SList a)
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                      TPProofRaw (SList a)
-> ChainsTo (TPProofRaw (SList a))
-> ChainsTo (TPProofRaw (SList a))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs
                      SList a -> ChainsTo (SList a) -> ChainsTo (SList a)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo (SList a)
TPProofRaw (SList a)
forall a. TPProofRaw a
qed

    Proof (Forall "xs" [a] -> SBool)
sortIsPermutation <-
        String
-> (Forall "xs" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) Bool)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall t.
(Proposition (Forall "xs" [a] -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "xs" [a] -> SBool)
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) t)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a t.
(Inductive a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String
-> a
-> (Proof (IHType a) -> IHArg a -> IStepArgs a t)
-> TP (Proof a)
induct String
"sortIsPermutation"
               (\(Forall @"xs" (SList a
xs :: SList a)) -> SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation SList a
xs (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs)) ((Proof (IHType (Forall "xs" [a] -> SBool))
  -> IHArg (Forall "xs" [a] -> SBool)
  -> IStepArgs (Forall "xs" [a] -> SBool) Bool)
 -> TP (Proof (Forall "xs" [a] -> SBool)))
-> (Proof (IHType (Forall "xs" [a] -> SBool))
    -> IHArg (Forall "xs" [a] -> SBool)
    -> IStepArgs (Forall "xs" [a] -> SBool) Bool)
-> TP (Proof (Forall "xs" [a] -> SBool))
forall a b. (a -> b) -> a -> b
$
               \Proof (IHType (Forall "xs" [a] -> SBool))
ih (SBV a
x, SList a
xs) ->
                   [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs))
                      SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation (SBV a
x SBV a -> SList a -> SList a
forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
xs) (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
x (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs))
                      SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=:     SBV a
x SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
x (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs)
                         SBool -> SBool -> SBool
.&& SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation SList a
xs (SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
x (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
x (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs)))
                      SBool
-> Proof (Forall "xs" [a] -> Forall "e" a -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
insertIsElem
                      TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation SList a
xs (SBV a -> SList a -> SList a
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SList a
removeFirst SBV a
x (SBV a -> SList a -> SList a
forall a. (Ord a, SymVal a) => SBV a -> SList a -> SList a
insert SBV a
x (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs)))
                      SBool
-> Proof (Forall "xs" [a] -> Forall "e" a -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof (Forall "xs" [a] -> Forall "e" a -> SBool)
removeAfterInsert
                      TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
isPermutation SList a
xs (SList a -> SList a
forall a. (Ord a, SymVal a) => SList a -> SList a
insertionSort SList a
xs)
                      SBool -> Proof SBool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof SBool
Proof (IHType (Forall "xs" [a] -> SBool))
ih
                      TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                      SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed

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