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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.BinarySearch where

import Prelude hiding (null, length, (!!), drop, take, tail, elem, notElem)

import Data.SBV
import Data.SBV.Maybe
import Data.SBV.TP

-- * Binary search

-- | We will work with arrays containing integers, indexed by integers. Note that since SMTLib arrays
-- are indexed by their entire domain, we explicitly take a lower/upper bounds as parameters, which fits well
-- with the binary search algorithm.
type Arr = SArray Integer Integer

-- | Bounds: This is the focus into the array; both indexes are inclusive.
type Idx = (SInteger, SInteger)

-- | Encode binary search in a functional style.
bsearch :: Arr -> Idx -> SInteger -> SMaybe Integer
bsearch :: Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
array (SInteger
low, SInteger
high) = Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer
f Arr
array SInteger
low SInteger
high
  where f :: Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer
f = String
-> (Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer)
-> Arr
-> SInteger
-> SInteger
-> SInteger
-> SMaybe Integer
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"bsearch" ((Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer)
 -> Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer)
-> (Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer)
-> Arr
-> SInteger
-> SInteger
-> SInteger
-> SMaybe Integer
forall a b. (a -> b) -> a -> b
$ \Arr
arr SInteger
lo SInteger
hi SInteger
x ->
               let mid :: SInteger
mid  = (SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
hi) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                   xmid :: SInteger
xmid = Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid
               in SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                      SMaybe Integer
forall a. SymVal a => SMaybe a
sNothing
                      (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                           (SInteger -> SMaybe Integer
forall a. SymVal a => SBV a -> SMaybe a
sJust SInteger
mid)
                           (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x)
                                (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)))

-- * Correctness proof

-- | A predicate testing whether a given array is non-decreasing in the given range
nonDecreasing :: Arr -> Idx -> SBool
nonDecreasing :: Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
low, SInteger
high) = (Forall Any Integer -> Forall Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall Any Integer -> Forall Any Integer -> SBool) -> SBool)
-> (Forall Any Integer -> Forall Any Integer -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$
    \(Forall SInteger
i) (Forall SInteger
j) -> SInteger
low SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
i SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
j SBool -> SBool -> SBool
.&& SInteger
j SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
high SBool -> SBool -> SBool
.=> Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
j

-- | A predicate testing whether an element is in the array within the given bounds
inArray :: Arr -> Idx -> SInteger -> SBool
inArray :: Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
low, SInteger
high) SInteger
elt = (Exists Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Exists Any Integer -> SBool) -> SBool)
-> (Exists Any Integer -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Exists SInteger
i) -> SInteger
low SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
i SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
high SBool -> SBool -> SBool
.&& Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
elt

-- | Correctness of binary search.
--
-- We have:
--
-- >>> correctness
-- Lemma: notInRange                                 Q.E.D.
-- Lemma: inRangeHigh                                Q.E.D.
-- Lemma: inRangeLow                                 Q.E.D.
-- Lemma: nonDecreasing                              Q.E.D.
-- Inductive lemma (strong): bsearchAbsent
--   Step: Measure is non-negative                   Q.E.D.
--   Step: 1 (unfold bsearch)                        Q.E.D.
--   Step: 2 (push isNothing down, simplify)         Q.E.D.
--   Step: 3 (2 way case split)
--     Step: 3.1                                     Q.E.D.
--     Step: 3.2.1                                   Q.E.D.
--     Step: 3.2.2                                   Q.E.D.
--     Step: 3.2.3                                   Q.E.D.
--     Step: 3.2.4                                   Q.E.D.
--     Step: 3.2.5 (simplify)                        Q.E.D.
--     Step: 3.Completeness                          Q.E.D.
--   Result:                                         Q.E.D.
-- Inductive lemma (strong): bsearchPresent
--   Step: Measure is non-negative                   Q.E.D.
--   Step: 1 (unfold bsearch)                        Q.E.D.
--   Step: 2 (simplify)                              Q.E.D.
--   Step: 3 (3 way case split)
--     Step: 3.1                                     Q.E.D.
--     Step: 3.2                                     Q.E.D.
--     Step: 3.3.1                                   Q.E.D.
--     Step: 3.3.2 (3 way case split)
--       Step: 3.3.2.1                               Q.E.D.
--       Step: 3.3.2.2.1                             Q.E.D.
--       Step: 3.3.2.2.2                             Q.E.D.
--       Step: 3.3.2.3.1                             Q.E.D.
--       Step: 3.3.2.3.2                             Q.E.D.
--       Step: 3.3.2.Completeness                    Q.E.D.
--     Step: 3.Completeness                          Q.E.D.
--   Result:                                         Q.E.D.
-- Lemma: bsearchCorrect
--   Step: 1 (2 way case split)
--     Step: 1.1.1                                   Q.E.D.
--     Step: 1.1.2                                   Q.E.D.
--     Step: 1.2.1                                   Q.E.D.
--     Step: 1.2.2                                   Q.E.D.
--     Step: 1.Completeness                          Q.E.D.
--   Result:                                         Q.E.D.
-- [Proven] bsearchCorrect :: Ɐarr ∷ (ArrayModel Integer Integer) → Ɐlo ∷ Integer → Ɐhi ∷ Integer → Ɐx ∷ Integer → Bool
correctness :: IO (Proof (Forall "arr" (ArrayModel Integer Integer) -> Forall "lo" Integer -> Forall "hi" Integer -> Forall "x" Integer -> SBool))
correctness :: IO
  (Proof
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool))
correctness = SMTConfig
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
-> IO
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall a. SMTConfig -> TP a -> IO a
runTPWith (Int -> SMTConfig -> SMTConfig
tpRibbon Int
50 SMTConfig
cvc5) (TP
   (Proof
      (Forall "arr" (ArrayModel Integer Integer)
       -> Forall "lo" Integer
       -> Forall "hi" Integer
       -> Forall "x" Integer
       -> SBool))
 -> IO
      (Proof
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)))
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
-> IO
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall a b. (a -> b) -> a -> b
$ do

  -- Helper: if a value is not in a range, then it isn't in any subrange of it:
  Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
notInRange <- String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "m" Integer
    -> Forall "x" Integer
    -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "m" Integer
         -> Forall "x" Integer
         -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"notInRange"
                           (\(Forall Arr
arr) (Forall SInteger
lo) (Forall SInteger
hi) (Forall SInteger
md) (Forall SInteger
x)
                               ->  SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x) SBool -> SBool -> SBool
.&& SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
md SBool -> SBool -> SBool
.&& SInteger
md SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi
                               SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
md) SInteger
x) SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
md, SInteger
hi) SInteger
x))
                           []

  -- Helper: if a value is in a range of a nonDecreasing array, and if its value is larger than a given mid point, then it's in the higher part
  Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
inRangeHigh <- String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "m" Integer
    -> Forall "x" Integer
    -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "m" Integer
         -> Forall "x" Integer
         -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"inRangeHigh"
                       (\(Forall Arr
arr) (Forall SInteger
lo) (Forall SInteger
hi) (Forall SInteger
md) (Forall SInteger
x)
                           ->  Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x SBool -> SBool -> SBool
.&& SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
md SBool -> SBool -> SBool
.&& SInteger
md SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
md
                           SBool -> SBool -> SBool
.=> Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
mdSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi) SInteger
x)
                       []

  -- Helper: if a value is in a range of a nonDecreasing array, and if its value is lower than a given mid point, then it's in the lowr part
  Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
inRangeLow  <- String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "m" Integer
    -> Forall "x" Integer
    -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "m" Integer
         -> Forall "x" Integer
         -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"inRangeLow"
                       (\(Forall Arr
arr) (Forall SInteger
lo) (Forall SInteger
hi) (Forall SInteger
md) (Forall SInteger
x)
                           ->  Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x SBool -> SBool -> SBool
.&& SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
md SBool -> SBool -> SBool
.&& SInteger
md SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
md
                           SBool -> SBool -> SBool
.=> Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
mdSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)
                       []

  -- Helper: if an array is nonDecreasing, then its parts are also non-decreasing when cut in any middle point
  Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
nonDecreasingInRange <- String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "m" Integer
    -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "m" Integer
         -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"nonDecreasing"
                                (\(Forall Arr
arr) (Forall SInteger
lo) (Forall SInteger
hi) (Forall SInteger
md)
                                    ->  Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
md SBool -> SBool -> SBool
.&& SInteger
md SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi
                                    SBool -> SBool -> SBool
.=> Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
md) SBool -> SBool -> SBool
.&& Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
md, SInteger
hi))
                                []

  -- Prove the case when the target is not in the array
  Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
bsearchAbsent <- String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool)
-> MeasureArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
     Integer
-> (Proof
      (Forall "arr" (ArrayModel Integer Integer)
       -> Forall "lo" Integer
       -> Forall "hi" Integer
       -> Forall "x" Integer
       -> SBool)
    -> StepArgs
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool)
-> MeasureArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
     m
-> (Proof
      (Forall "arr" (ArrayModel Integer Integer)
       -> Forall "lo" Integer
       -> Forall "hi" Integer
       -> Forall "x" Integer
       -> SBool)
    -> StepArgs
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)
         t)
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
sInduct String
"bsearchAbsent"
        (\(Forall Arr
arr) (Forall SInteger
lo) (Forall SInteger
hi) (Forall SInteger
x) ->
            Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x) SBool -> SBool -> SBool
.=> SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x))
        (\Arr
_arr SInteger
lo SInteger
hi SInteger
_x -> SInteger -> SInteger
forall a. Num a => a -> a
abs (SInteger
hi SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)) ((Proof
    (Forall "arr" (ArrayModel Integer Integer)
     -> Forall "lo" Integer
     -> Forall "hi" Integer
     -> Forall "x" Integer
     -> SBool)
  -> StepArgs
       (Forall "arr" (ArrayModel Integer Integer)
        -> Forall "lo" Integer
        -> Forall "hi" Integer
        -> Forall "x" Integer
        -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)))
-> (Proof
      (Forall "arr" (ArrayModel Integer Integer)
       -> Forall "lo" Integer
       -> Forall "hi" Integer
       -> Forall "x" Integer
       -> SBool)
    -> StepArgs
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall a b. (a -> b) -> a -> b
$
        \Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
ih Arr
arr SInteger
lo SInteger
hi SInteger
x ->
              [Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi), SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)]
           [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
           SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold bsearch"
           TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let mid :: SInteger
mid  = (SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
hi) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                  xmid :: SInteger
xmid = Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid
           in SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                             SMaybe Integer
forall a. SymVal a => SMaybe a
sNothing
                             (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                  (SInteger -> SMaybe Integer
forall a. SymVal a => SBV a -> SMaybe a
sJust SInteger
mid)
                                  (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                       (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x)
                                       (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))))
           SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push isNothing down, 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 (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                  SBool
sTrue
                  (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                       SBool
sFalse
                       (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                            (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                            (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))))
           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                    , SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                        SBool
sFalse
                                        (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                             (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                                             (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)))
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let inst1 :: SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SBV a
l SBV a
h SBV a
m = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV a
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                        inst2 :: SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SBV a
l SBV a
h SBV a
m = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV a
m             )
                                        inst3 :: SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 SBV a
l SBV a
h   = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h,              forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                 in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                        (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                                        (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))
                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
notInRange           Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "m" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SInteger
lo      SInteger
hi (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                                 TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
nonDecreasingInRange Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "m" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SInteger
lo      SInteger
hi (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                                 Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
ih                   Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
forall {a} {a}.
SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
hi
                                 Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                        SBool
sTrue
                                        (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))
                                 SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
notInRange           Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "m" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SInteger
lo SInteger
hi      (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                 TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
nonDecreasingInRange Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "m" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SInteger
lo SInteger
hi      (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                 Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
ih                   Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
forall {a} {a}.
SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 SInteger
lo (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                 Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x) SBool
sTrue SBool
sTrue
                                 SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                 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
                    ]

  -- Prove the case when the target is in the array
  Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
bsearchPresent <- String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool)
-> MeasureArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
     Integer
-> (Proof
      (Forall "arr" (ArrayModel Integer Integer)
       -> Forall "lo" Integer
       -> Forall "hi" Integer
       -> Forall "x" Integer
       -> SBool)
    -> StepArgs
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall a m t.
(SInductive a, Proposition a, Zero m, SymVal t,
 EqSymbolic (SBV t)) =>
String
-> a
-> MeasureArgs a m
-> (Proof a -> StepArgs a t)
-> TP (Proof a)
forall m t.
(Proposition
   (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool),
 Zero m, SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool)
-> MeasureArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
     m
-> (Proof
      (Forall "arr" (ArrayModel Integer Integer)
       -> Forall "lo" Integer
       -> Forall "hi" Integer
       -> Forall "x" Integer
       -> SBool)
    -> StepArgs
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)
         t)
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
sInduct String
"bsearchPresent"
        (\(Forall Arr
arr) (Forall SInteger
lo) (Forall SInteger
hi) (Forall SInteger
x) ->
            Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x SBool -> SBool -> SBool
.=> Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
        (\Arr
_arr SInteger
lo SInteger
hi SInteger
_x -> SInteger -> SInteger
forall a. Num a => a -> a
abs (SInteger
hi SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)) ((Proof
    (Forall "arr" (ArrayModel Integer Integer)
     -> Forall "lo" Integer
     -> Forall "hi" Integer
     -> Forall "x" Integer
     -> SBool)
  -> StepArgs
       (Forall "arr" (ArrayModel Integer Integer)
        -> Forall "lo" Integer
        -> Forall "hi" Integer
        -> Forall "x" Integer
        -> SBool)
       Bool)
 -> TP
      (Proof
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)))
-> (Proof
      (Forall "arr" (ArrayModel Integer Integer)
       -> Forall "lo" Integer
       -> Forall "hi" Integer
       -> Forall "x" Integer
       -> SBool)
    -> StepArgs
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)
         Bool)
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall a b. (a -> b) -> a -> b
$
        \Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
ih Arr
arr SInteger
lo SInteger
hi SInteger
x ->
             [Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi), Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x]
          [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
          SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold bsearch"
          TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let mid :: SInteger
mid  = (SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
hi) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                 xmid :: SInteger
xmid = Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid
          in SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                                                 SMaybe Integer
forall a. SymVal a => SMaybe a
sNothing
                                                 (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                                      (SInteger -> SMaybe Integer
forall a. SymVal a => SBV a -> SMaybe a
sJust SInteger
mid)
                                                      (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                                           (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x)
                                                           (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))))
          SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"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 (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                 (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust SMaybe Integer
forall a. SymVal a => SMaybe a
sNothing)
                 (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                      (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid)
                      (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                           (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                           (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))))
          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SInteger
hi SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                   , SInteger
lo SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
hi SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                   , SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<  SInteger
hi SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                       (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid)
                                       (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                            (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                                            (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)))
                                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let inst1 :: SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SBV a
l SBV a
h SBV a
m = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV a
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                       inst2 :: SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SBV a
l SBV a
h SBV a
m = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV a
m             )
                                       inst3 :: SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 SBV a
l SBV a
h   = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h,              forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                in [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> TPProofRaw SBool
forall a. Trivial a => a
trivial
                                         , SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x)
                                                       SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
inRangeHigh          Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "m" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SInteger
lo      SInteger
hi SInteger
mid
                                                       TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
nonDecreasingInRange Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "m" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SInteger
lo      SInteger
hi (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                                                       Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
ih                   Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
forall {a} {a}.
SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
hi
                                                       Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                         , SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
x  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)
                                                       SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
inRangeLow           Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "m" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SInteger
lo SInteger
hi      SInteger
mid
                                                       TPProofRaw SBool -> Proof Bool -> Hinted (TPProofRaw SBool)
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
nonDecreasingInRange Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "m" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "m" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SInteger
lo SInteger
hi      (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                                       Hinted (TPProofRaw SBool)
-> Proof Bool -> Hinted (Hinted (TPProofRaw SBool))
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
ih                   Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
forall {a} {a}.
SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 SInteger
lo (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                                       Hinted (Hinted (TPProofRaw SBool))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
-> ChainsTo (Hinted (Hinted (TPProofRaw SBool)))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed
                                         ]
                   ]

  String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool)
-> StepArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
     Bool
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall t.
(Proposition
   (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool)
-> StepArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
     t
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"bsearchCorrect"
        (\(Forall Arr
arr) (Forall SInteger
lo) (Forall SInteger
hi) (Forall SInteger
x) ->
            Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.=> let res :: SMaybe Integer
res = Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x
                                           in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
                                                  (Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust SMaybe Integer
res SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                                  (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing SMaybe Integer
res)) (StepArgs
   (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "x" Integer
    -> SBool)
   Bool
 -> TP
      (Proof
         (Forall "arr" (ArrayModel Integer Integer)
          -> Forall "lo" Integer
          -> Forall "hi" Integer
          -> Forall "x" Integer
          -> SBool)))
-> StepArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
     Bool
-> TP
     (Proof
        (Forall "arr" (ArrayModel Integer Integer)
         -> Forall "lo" Integer
         -> Forall "hi" Integer
         -> Forall "x" Integer
         -> SBool))
forall a b. (a -> b) -> a -> b
$
        \Arr
arr SInteger
lo SInteger
hi SInteger
x -> [Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi)]
                     [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
|- let res :: SMaybe Integer
res = Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x
                        in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
                               (Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust SMaybe Integer
res SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                               (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing SMaybe Integer
res)
                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, TPProofRaw SBool)] -> TPProofRaw SBool
forall a. [(SBool, TPProofRaw a)] -> TPProofRaw a
cases [ Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x
                                  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x
                                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
bsearchPresent Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SInteger
lo, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SInteger
hi, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                   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
                              , SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
                                  SBool -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. SBool -> TPProofRaw a -> (SBool, TPProofRaw a)
==> SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
                                   SBool -> Proof Bool -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
bsearchAbsent Proof
  (Forall "arr" (ArrayModel Integer Integer)
   -> Forall "lo" Integer
   -> Forall "hi" Integer
   -> Forall "x" Integer
   -> SBool)
-> IArgs
     (Forall "arr" (ArrayModel Integer Integer)
      -> Forall "lo" Integer
      -> Forall "hi" Integer
      -> Forall "x" Integer
      -> SBool)
-> Proof Bool
forall a. Instantiatable a => Proof a -> IArgs a -> Proof Bool
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SInteger
lo, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SInteger
hi, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                   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
                              ]