-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.KD.KnuckleDragger
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A lightweight theorem proving like interface, built on top of SBV.
-- Inspired by and modeled after Philip Zucker's tool with the same
-- name, see <http://github.com/philzook58/knuckledragger>.
--
-- See the directory Documentation.SBV.Examples.KnuckleDragger for various examples.
-----------------------------------------------------------------------------

{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeAbstractions           #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.KD.KnuckleDragger (
         Proposition, Proof, Instantiatable(..), Inst(..)
       , axiom
       , lemma,   lemmaWith
       , theorem, theoremWith
       ,    calc,    calcWith,    calcThm,    calcThmWith
       ,  induct,  inductWith,  inductThm,  inductThmWith
       , sInduct, sInductWith, sInductThm, sInductThmWith
       , sorry
       , KD, runKD, runKDWith, use
       , (|-), (⊢), (=:), (≡), (??), (⁇), cases, hyp, hprf, qed
       ) where

import Data.SBV
import Data.SBV.Core.Model (qSaturateSavingObservables)

import Data.SBV.Control hiding (getProof)

import Data.SBV.Core.Data(SolverContext)

import Data.SBV.Tools.KD.Kernel
import Data.SBV.Tools.KD.Utils

import Control.Monad (forM_)
import Control.Monad.Trans (liftIO, MonadIO)

import qualified Data.SBV.List as SL

import Data.Char (isSpace)
import Data.List (isPrefixOf, isSuffixOf)
import Data.Maybe (catMaybes)

import Data.Proxy
import GHC.TypeLits (KnownSymbol, symbolVal, Symbol)

import Data.SBV.Utils.TDiff

import Data.Dynamic
import Data.Time (NominalDiffTime)

-- | Bring an IO proof into current proof context.
use :: IO Proof -> KD Proof
use :: IO Proof -> KD Proof
use = IO Proof -> KD Proof
forall a. IO a -> KD a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

-- | Captures the steps for a calculationa proof
data CalcStrategy = CalcStrategy { CalcStrategy -> SBool
calcIntros     :: SBool
                                 , CalcStrategy -> [([Helper], SBool)]
calcProofSteps :: [([Helper], SBool)]
                                 }

-- | Saturatable things in steps
proofStepSaturatables :: [([Helper], SBool)] -> [SBool]
proofStepSaturatables :: [([Helper], SBool)] -> [SBool]
proofStepSaturatables = (([Helper], SBool) -> [SBool]) -> [([Helper], SBool)] -> [SBool]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Helper], SBool) -> [SBool]
forall {t :: * -> *}. Foldable t => (t Helper, SBool) -> [SBool]
getS
  where getS :: (t Helper, SBool) -> [SBool]
getS (t Helper
hs, SBool
b) = SBool
b SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: (Helper -> [SBool]) -> t Helper -> [SBool]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [SBool]
getH t Helper
hs
        getH :: Helper -> [SBool]
getH (HelperProof  Proof
p)  = [Proof -> SBool
getProof Proof
p]
        getH (HelperAssum  SBool
b)  = [SBool
b]
        getH (HelperCase String
_ [SBool]
ss) = [SBool]
ss

-- | Things that are inside calc-strategy that we have to saturate
getCalcStrategySaturatables :: CalcStrategy -> [SBool]
getCalcStrategySaturatables :: CalcStrategy -> [SBool]
getCalcStrategySaturatables (CalcStrategy SBool
calcIntros [([Helper], SBool)]
calcProofSteps) = SBool
calcIntros SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [([Helper], SBool)] -> [SBool]
proofStepSaturatables [([Helper], SBool)]
calcProofSteps

-- | Based on the helpers given, construct the proofs we have to do in the given case
stepCases :: Int -> [Helper] -> Either (String, SBool) ([(String, SBool)], SBool)
stepCases :: Int
-> [Helper] -> Either (String, SBool) ([(String, SBool)], SBool)
stepCases Int
i [Helper]
helpers
   | Bool
hasCase
   = ([(String, SBool)], SBool)
-> Either (String, SBool) ([(String, SBool)], SBool)
forall a b. b -> Either a b
Right ([(String, SBool)]
caseSplits, SBool
cover)
   | Bool
True
   = (String, SBool)
-> Either (String, SBool) ([(String, SBool)], SBool)
forall a b. a -> Either a b
Left (Int -> String
forall a. Show a => a -> String
show Int
i, [SBool] -> SBool
sAnd ((Helper -> SBool) -> [Helper] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map Helper -> SBool
getBools [Helper]
helpers))
  where join :: [(String, SBool)] -> Helper -> [(String, SBool)]
        join :: [(String, SBool)] -> Helper -> [(String, SBool)]
join [(String, SBool)]
sofar (HelperProof Proof
p)     =       ((String, SBool) -> (String, SBool))
-> [(String, SBool)] -> [(String, SBool)]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
n, SBool
cond) -> (String
n, SBool
cond SBool -> SBool -> SBool
.&& Proof -> SBool
getProof Proof
p)) [(String, SBool)]
sofar
        join [(String, SBool)]
sofar (HelperAssum SBool
b)     =       ((String, SBool) -> (String, SBool))
-> [(String, SBool)] -> [(String, SBool)]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
n, SBool
cond) -> (String
n, SBool
cond SBool -> SBool -> SBool
.&&          SBool
b)) [(String, SBool)]
sofar
        join [(String, SBool)]
sofar (HelperCase  String
cn [SBool]
cs) = ((String, SBool) -> [(String, SBool)])
-> [(String, SBool)] -> [(String, SBool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(String
n, SBool
cond) -> [ (String -> String
dotN String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cn String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
j String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]", SBool
cond SBool -> SBool -> SBool
.&& SBool
b)
                                                                  | (Int
j, SBool
b) <- [Int] -> [SBool] -> [(Int, SBool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1::Int)..] [SBool]
cs
                                                                  ]) [(String, SBool)]
sofar

        -- Add a dot if we have a legit prefix
        dotN :: String -> String
dotN String
"" = String
""
        dotN String
s  = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."

        -- Used only when we have ano case splits:
        getBools :: Helper -> SBool
getBools (HelperProof Proof
p) = Proof -> SBool
getProof Proof
p
        getBools (HelperAssum SBool
b) = SBool
b
        getBools (HelperCase{})  = String -> SBool
forall a. HasCallStack => String -> a
error String
"Unexpected case in stepCases: Wasn't expecting to see a HelperCase here."

        -- All case-splits. If there isn't any, we'll get just one case
        caseSplits :: [(String, SBool)]
caseSplits = ([(String, SBool)] -> Helper -> [(String, SBool)])
-> [(String, SBool)] -> [Helper] -> [(String, SBool)]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [(String, SBool)] -> Helper -> [(String, SBool)]
join [(String
"", SBool
sTrue)] [Helper]
helpers

        -- If there were any cases, then we also need coverage
        isCase :: Helper -> Bool
isCase (HelperProof {}) = Bool
False
        isCase (HelperAssum {}) = Bool
False
        isCase (HelperCase  {}) = Bool
True

        hasCase :: Bool
hasCase = (Helper -> Bool) -> [Helper] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Helper -> Bool
isCase [Helper]
helpers

        regulars :: [SBool]
regulars = (Helper -> [SBool]) -> [Helper] -> [SBool]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [SBool]
getHyp [Helper]
helpers
          where getHyp :: Helper -> [SBool]
getHyp (HelperProof Proof
p)  = [Proof -> SBool
getProof Proof
p]
                getHyp (HelperAssum SBool
b)  = [SBool
b]
                getHyp (HelperCase  {}) = []

        cover :: SBool
cover = [SBool] -> SBool
sAnd [SBool]
regulars SBool -> SBool -> SBool
.&& SBool -> SBool
sNot ([SBool] -> SBool
sOr [SBool
b | (String
_, SBool
b) <- [(String, SBool)]
caseSplits])

-- | Propagate the settings for ribbon/timing from top to current. Because in any subsequent configuration
-- in a lemmaWith, inductWith etc., we just want to change the solver, not the actual settings for KD.
kdMergeCfg :: SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg :: SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cur SMTConfig
top = SMTConfig
cur{kdOptions = kdOptions top}

-- | A class for doing equational reasoning style calculational proofs. Use 'calc' to prove a given theorem
-- as a sequence of equalities, each step following from the previous.
class CalcLemma a steps where

  -- | Prove a property via a series of equality steps, using the default solver.
  -- Let @H@ be a list of already established lemmas. Let @P@ be a property we wanted to prove, named @name@.
  -- Consider a call of the form @calc name P (cond, [A, B, C, D]) H@. Note that @H@ is
  -- a list of already proven facts, ensured by the type signature. We proceed as follows:
  --
  --    * Prove: @(H && cond)                                   -> (A == B)@
  --    * Prove: @(H && cond && A == B)                         -> (B == C)@
  --    * Prove: @(H && cond && A == B && B == C)               -> (C == D)@
  --    * Prove: @(H && (cond -> (A == B && B == C && C == D))) -> P@
  --    * If all of the above steps succeed, conclude @P@.
  --
  -- cond acts as the context. Typically, if you are trying to prove @Y -> Z@, then you want cond to be Y.
  -- (This is similar to @intros@ commands in theorem provers.)
  --
  -- So, calc-lemma is essentially modus-ponens, applied in a sequence of stepwise equality reasoning in the case of
  -- non-boolean steps.
  --
  -- If there are no helpers given (i.e., if @H@ is empty), then this call is equivalent to 'lemmaWith'.
  -- If @H@ is a singleton, then we bail out. A single step in @H@ indicates a usage mistake, since there's
  -- no sequence of steps to reason about.
  calc :: Proposition a => String -> a -> steps -> KD Proof

  -- | Same as calc, except tagged as Theorem
  calcThm :: Proposition a => String -> a -> steps -> KD Proof

  -- | Prove a property via a series of equality steps, using the given solver.
  calcWith :: Proposition a => SMTConfig -> String -> a -> steps -> KD Proof

  -- | Same as calcWith, except tagged as Theorem
  calcThmWith :: Proposition a => SMTConfig -> String -> a -> steps -> KD Proof

  -- | Internal, shouldn't be needed outside the library
  {-# MINIMAL calcSteps #-}
  calcSteps :: a -> steps -> Symbolic (SBool, CalcStrategy)

  calc            String
nm a
p steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg  -> SMTConfig -> String -> a -> steps -> KD Proof
forall a steps.
(CalcLemma a steps, Proposition a) =>
SMTConfig -> String -> a -> steps -> KD Proof
calcWith          SMTConfig
cfg                   String
nm a
p steps
steps
  calcThm         String
nm a
p steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg  -> SMTConfig -> String -> a -> steps -> KD Proof
forall a steps.
(CalcLemma a steps, Proposition a) =>
SMTConfig -> String -> a -> steps -> KD Proof
calcThmWith       SMTConfig
cfg                   String
nm a
p steps
steps
  calcWith    SMTConfig
cfg String
nm a
p steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg' -> Bool -> SMTConfig -> String -> a -> steps -> KD Proof
forall a steps.
(CalcLemma a steps, Proposition a) =>
Bool -> SMTConfig -> String -> a -> steps -> KD Proof
calcGeneric Bool
False (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p steps
steps
  calcThmWith SMTConfig
cfg String
nm a
p steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg' -> Bool -> SMTConfig -> String -> a -> steps -> KD Proof
forall a steps.
(CalcLemma a steps, Proposition a) =>
Bool -> SMTConfig -> String -> a -> steps -> KD Proof
calcGeneric Bool
True  (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p steps
steps

  calcGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> KD Proof
  calcGeneric Bool
tagTheorem cfg :: SMTConfig
cfg@SMTConfig{kdOptions :: SMTConfig -> KDOptions
kdOptions = KDOptions{Bool
measureTime :: Bool
measureTime :: KDOptions -> Bool
measureTime}} String
nm a
result steps
steps = do
     kdSt <- KD KDState
getKDState

     liftIO $ runSMTWith cfg $ do

        qSaturateSavingObservables result -- make sure we saturate the result, i.e., get all it's UI's, types etc. pop out

        message cfg $ (if tagTheorem then "Theorem" else "Lemma") ++ ": " ++ nm ++ "\n"

        mbStartTime <- getTimeStampIf measureTime

        (calcGoal, strategy@CalcStrategy {calcIntros, calcProofSteps}) <- calcSteps result steps

        let stepHelpers = (([Helper], SBool) -> [Helper]) -> [([Helper], SBool)] -> [Helper]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Helper], SBool) -> [Helper]
forall a b. (a, b) -> a
fst [([Helper], SBool)]
calcProofSteps

            finish [NominalDiffTime]
et [Proof]
helpers (Int, Maybe NominalDiffTime)
d = SMTConfig
-> String
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishKD SMTConfig
cfg (String
"Q.E.D." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
modulo) (Int, Maybe NominalDiffTime)
d [NominalDiffTime]
et
              where (RootOfTrust
_, String
modulo) = String -> [Proof] -> (RootOfTrust, String)
calculateRootOfTrust String
nm [Proof]
helpers

        -- Collect all subterms and saturate them
        mapM_ qSaturateSavingObservables $ calcIntros : getCalcStrategySaturatables strategy

        let go :: Int -> SBool -> [([Helper], SBool)] -> Query Proof
            go Int
_ SBool
accum [] = do
                [String] -> Query ()
queryDebug [String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Proof end: proving the result:"]
                SMTConfig
-> KDState
-> String
-> Bool
-> Maybe SBool
-> SBool
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO Proof)
-> Query Proof
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Bool
-> Maybe SBool
-> a
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
checkSatThen SMTConfig
cfg KDState
kdSt String
"Result" Bool
True
                             (SBool -> Maybe SBool
forall a. a -> Maybe a
Just (SBool
calcIntros SBool -> SBool -> SBool
.=> SBool
accum))
                             SBool
calcGoal
                             []
                             [String
"", String
""]
                             ([String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
nm, String
"Result"])
                             Maybe (IO ())
forall a. Maybe a
Nothing (((Int, Maybe NominalDiffTime) -> IO Proof) -> Query Proof)
-> ((Int, Maybe NominalDiffTime) -> IO Proof) -> Query Proof
forall a b. (a -> b) -> a -> b
$ \(Int, Maybe NominalDiffTime)
d -> do mbElapsed <- Maybe UTCTime -> IO (Maybe NominalDiffTime)
forall (m :: * -> *).
MonadIO m =>
Maybe UTCTime -> m (Maybe NominalDiffTime)
getElapsedTime Maybe UTCTime
mbStartTime
                                                let (ros, modulo) = calculateRootOfTrust nm (getHelperProofs stepHelpers)
                                                finishKD cfg ("Q.E.D." ++ modulo) d (catMaybes [mbElapsed])

                                                pure Proof { rootOfTrust = ros
                                                           , isUserAxiom = False
                                                           , getProof    = label nm (quantifiedBool result)
                                                           , getProp     = toDyn result
                                                           , proofName   = nm
                                                           }

            go Int
i SBool
accum (([Helper]
by, SBool
s):[([Helper], SBool)]
ss) = do

                 -- Prove that the assumptions follow, if any
                 case [Helper] -> [SBool]
getHelperAssumes [Helper]
by of
                   [] -> () -> Query ()
forall a. a -> QueryT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                   [SBool]
as -> SMTConfig
-> KDState
-> String
-> Bool
-> Maybe SBool
-> SBool
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> Query ()
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Bool
-> Maybe SBool
-> a
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
checkSatThen SMTConfig
cfg KDState
kdSt String
"Asms  "
                                               Bool
True
                                               (SBool -> Maybe SBool
forall a. a -> Maybe a
Just SBool
calcIntros)
                                               ([SBool] -> SBool
sAnd [SBool]
as)
                                               []
                                               [String
"", Int -> String
forall a. Show a => a -> String
show Int
i]
                                               ([String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
nm, Int -> String
forall a. Show a => a -> String
show Int
i, String
"Assumptions"])
                                               Maybe (IO ())
forall a. Maybe a
Nothing
                                               ([NominalDiffTime]
-> [Proof] -> (Int, Maybe NominalDiffTime) -> IO ()
finish [] [])

                 [String] -> Query ()
queryDebug [String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Proof step: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":"]

                 Int
-> SMTConfig
-> KDState
-> Either (String, SBool) ([(String, SBool)], SBool)
-> String
-> SBool
-> String
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> Query ()
forall (m :: * -> *) a.
(Monad m, SolverContext m, MonadIO m, MonadQuery m,
 Proposition a) =>
Int
-> SMTConfig
-> KDState
-> Either (String, SBool) ([(String, SBool)], SBool)
-> String
-> a
-> String
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> m ()
proveAllCases Int
i SMTConfig
cfg KDState
kdSt (Int
-> [Helper] -> Either (String, SBool) ([(String, SBool)], SBool)
stepCases Int
i [Helper]
by) String
"Step  " SBool
s String
nm ([NominalDiffTime]
-> [Proof] -> (Int, Maybe NominalDiffTime) -> IO ()
finish [] ([Helper] -> [Proof]
getHelperProofs [Helper]
by))

                 Int -> SBool -> [([Helper], SBool)] -> Query Proof
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (SBool
s SBool -> SBool -> SBool
.&& SBool
accum) [([Helper], SBool)]
ss

        query $ go (1::Int) sTrue calcProofSteps

proveAllCases :: (Monad m, SolverContext m, MonadIO m, MonadQuery m, Proposition a)
              => Int -> SMTConfig -> KDState
              -> Either (String, SBool) ([(String, SBool)], SBool)
              -> String -> a -> String -> ((Int, Maybe NominalDiffTime) -> IO ()) -> m ()
proveAllCases :: forall (m :: * -> *) a.
(Monad m, SolverContext m, MonadIO m, MonadQuery m,
 Proposition a) =>
Int
-> SMTConfig
-> KDState
-> Either (String, SBool) ([(String, SBool)], SBool)
-> String
-> a
-> String
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> m ()
proveAllCases Int
topStep SMTConfig
cfg KDState
kdSt Either (String, SBool) ([(String, SBool)], SBool)
caseInfo String
stepTag a
s String
nm (Int, Maybe NominalDiffTime) -> IO ()
finalize
  | Left (String
stepName, SBool
asmp) <- Either (String, SBool) ([(String, SBool)], SBool)
caseInfo
  = String -> SBool -> a -> [String] -> Maybe [String] -> m ()
checker String
stepTag SBool
asmp a
s [String
"", String
stepName] ([String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
nm, String
stepName])
  | Right ([(String, SBool)]
proofCases, SBool
coverCond) <- Either (String, SBool) ([(String, SBool)], SBool)
caseInfo
  = do let len :: Int
len   = [(String, SBool)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, SBool)]
proofCases
           ways :: String
ways  = case Int
len of
                     Int
1 -> String
"one way"
                     Int
n -> Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ways"

           slen :: String
slen  = Int -> String
forall a. Show a => a -> String
show Int
len
           clen :: Int
clen  = String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
slen
           sh :: Int -> String
sh Int
i  = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
clen (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse (Int -> String
forall a. Show a => a -> String
show Int
i) String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat Char
' '

       _tab <- IO Int -> m Int
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> m Int) -> IO Int -> m Int
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Bool -> String -> [String] -> IO Int
startKD SMTConfig
cfg Bool
True (String
"Step " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
topStep) [String
"", String
"Case split " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ways String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":"]

       forM_ (zip [(1::Int)..] proofCases) $ \(Int
c, (String
stepName, SBool
asmp)) ->
             String -> SBool -> a -> [String] -> Maybe [String] -> m ()
checker (String
"Case [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
sh Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
len String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]") SBool
asmp a
s [String
"", String
"", String
stepName] ([String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
nm, String
stepName])

       checker "Completeness" coverCond s ["", "", ""] (Just [nm, show topStep, "Completeness"])
  where
     checker :: String -> SBool -> a -> [String] -> Maybe [String] -> m ()
checker String
tag SBool
caseAsmp a
cond [String]
cnm Maybe [String]
fnm = SMTConfig
-> KDState
-> String
-> Bool
-> Maybe SBool
-> a
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> m ()
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Bool
-> Maybe SBool
-> a
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
checkSatThen SMTConfig
cfg KDState
kdSt String
tag Bool
True (SBool -> Maybe SBool
forall a. a -> Maybe a
Just SBool
caseAsmp) a
cond [] [String]
cnm Maybe [String]
fnm Maybe (IO ())
forall a. Maybe a
Nothing (Int, Maybe NominalDiffTime) -> IO ()
finalize

-- | Turn a sequence of steps into a chain of equalities
mkCalcSteps :: EqSymbolic a => (SBool, [ProofStep a]) -> CalcStrategy
mkCalcSteps :: forall a. EqSymbolic a => (SBool, [ProofStep a]) -> CalcStrategy
mkCalcSteps (SBool
intros, [ProofStep a]
xs) = case [ProofStep a] -> [ProofStep a]
forall a. [a] -> [a]
reverse [ProofStep a]
xs of
                             (SingleStep a
_ (Helper
_:[Helper]
_) : [ProofStep a]
_) -> String -> CalcStrategy
forall a. HasCallStack => String -> a
error (String -> CalcStrategy) -> String -> CalcStrategy
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                                         , String
"*** Incorrect calc/induct lemma calculations."
                                                                         , String
"***"
                                                                         , String
"***  The last step in the proof has a helper, which isn't used."
                                                                         , String
"***"
                                                                         , String
"*** Perhaps the hint is off-by-one in its placement?"
                                                                         ]
                             [ProofStep a]
_                       -> CalcStrategy { calcIntros :: SBool
calcIntros     = SBool
intros
                                                                     , calcProofSteps :: [([Helper], SBool)]
calcProofSteps = (ProofStep a -> ProofStep a -> ([Helper], SBool))
-> [ProofStep a] -> [ProofStep a] -> [([Helper], SBool)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ProofStep a -> ProofStep a -> ([Helper], SBool)
forall {a}.
EqSymbolic a =>
ProofStep a -> ProofStep a -> ([Helper], SBool)
merge [ProofStep a]
xs (Int -> [ProofStep a] -> [ProofStep a]
forall a. Int -> [a] -> [a]
drop Int
1 [ProofStep a]
xs)
                                                                     }
  where merge :: ProofStep a -> ProofStep a -> ([Helper], SBool)
merge (SingleStep a
a [Helper]
by) (SingleStep a
b [Helper]
_) = ([Helper]
by, a
a a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
b)

-- | Chaining lemmas that depend on no quantified variables
instance EqSymbolic z => CalcLemma SBool (SBool, [ProofStep z]) where
   calcSteps :: SBool -> (SBool, [ProofStep z]) -> Symbolic (SBool, CalcStrategy)
calcSteps SBool
result (SBool, [ProofStep z])
steps = (SBool, CalcStrategy) -> Symbolic (SBool, CalcStrategy)
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool
result, (SBool, [ProofStep z]) -> CalcStrategy
forall a. EqSymbolic a => (SBool, [ProofStep a]) -> CalcStrategy
mkCalcSteps (SBool, [ProofStep z])
steps)

-- | Chaining lemmas that depend on a single quantified variable.
instance (KnownSymbol na, SymVal a, EqSymbolic z) => CalcLemma (Forall na a -> SBool) (SBV a -> (SBool, [ProofStep z])) where
   calcSteps :: (Forall na a -> SBool)
-> (SBV a -> (SBool, [ProofStep z]))
-> Symbolic (SBool, CalcStrategy)
calcSteps Forall na a -> SBool
result SBV a -> (SBool, [ProofStep z])
steps = do a <- String -> Symbolic (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na))
                               pure (result (Forall a), mkCalcSteps (steps a))

-- | Chaining lemmas that depend on two quantified variables.
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z)
      => CalcLemma (Forall na a -> Forall nb b -> SBool)
                   (SBV a -> SBV b -> (SBool, [ProofStep z])) where
   calcSteps :: (Forall na a -> Forall nb b -> SBool)
-> (SBV a -> SBV b -> (SBool, [ProofStep z]))
-> Symbolic (SBool, CalcStrategy)
calcSteps Forall na a -> Forall nb b -> SBool
result SBV a -> SBV b -> (SBool, [ProofStep z])
steps = do (a, b) <- (,) (SBV a -> SBV b -> (SBV a, SBV b))
-> SymbolicT IO (SBV a) -> SymbolicT IO (SBV b -> (SBV a, SBV b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SymbolicT IO (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)) SymbolicT IO (SBV b -> (SBV a, SBV b))
-> SymbolicT IO (SBV b) -> SymbolicT IO (SBV a, SBV b)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV b)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb))
                               pure (result (Forall a) (Forall b), mkCalcSteps (steps a b))

-- | Chaining lemmas that depend on three quantified variables.
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z)
      => CalcLemma (Forall na a -> Forall nb b -> Forall nc c -> SBool)
                   (SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z])) where
   calcSteps :: (Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> (SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z]))
-> Symbolic (SBool, CalcStrategy)
calcSteps Forall na a -> Forall nb b -> Forall nc c -> SBool
result SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z])
steps = do (a, b, c) <- (,,) (SBV a -> SBV b -> SBV c -> (SBV a, SBV b, SBV c))
-> SymbolicT IO (SBV a)
-> SymbolicT IO (SBV b -> SBV c -> (SBV a, SBV b, SBV c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SymbolicT IO (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)) SymbolicT IO (SBV b -> SBV c -> (SBV a, SBV b, SBV c))
-> SymbolicT IO (SBV b)
-> SymbolicT IO (SBV c -> (SBV a, SBV b, SBV c))
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV b)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)) SymbolicT IO (SBV c -> (SBV a, SBV b, SBV c))
-> SymbolicT IO (SBV c) -> SymbolicT IO (SBV a, SBV b, SBV c)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV c)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc))
                               pure (result (Forall a) (Forall b) (Forall c), mkCalcSteps (steps a b c))

-- | Chaining lemmas that depend on four quantified variables.
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z)
      => CalcLemma (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
                   (SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z])) where
   calcSteps :: (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
-> (SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z]))
-> Symbolic (SBool, CalcStrategy)
calcSteps Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool
result SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z])
steps = do (a, b, c, d) <- (,,,) (SBV a -> SBV b -> SBV c -> SBV d -> (SBV a, SBV b, SBV c, SBV d))
-> SymbolicT IO (SBV a)
-> SymbolicT
     IO (SBV b -> SBV c -> SBV d -> (SBV a, SBV b, SBV c, SBV d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SymbolicT IO (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)) SymbolicT
  IO (SBV b -> SBV c -> SBV d -> (SBV a, SBV b, SBV c, SBV d))
-> SymbolicT IO (SBV b)
-> SymbolicT IO (SBV c -> SBV d -> (SBV a, SBV b, SBV c, SBV d))
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV b)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)) SymbolicT IO (SBV c -> SBV d -> (SBV a, SBV b, SBV c, SBV d))
-> SymbolicT IO (SBV c)
-> SymbolicT IO (SBV d -> (SBV a, SBV b, SBV c, SBV d))
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV c)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)) SymbolicT IO (SBV d -> (SBV a, SBV b, SBV c, SBV d))
-> SymbolicT IO (SBV d)
-> SymbolicT IO (SBV a, SBV b, SBV c, SBV d)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV d)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nd -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nd))
                               pure (result (Forall a) (Forall b) (Forall c) (Forall d), mkCalcSteps (steps a b c d))

-- | Chaining lemmas that depend on five quantified variables.
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z)
      => CalcLemma (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool)
                   (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, [ProofStep z])) where
   calcSteps :: (Forall na a
 -> Forall nb b
 -> Forall nc c
 -> Forall nd d
 -> Forall ne e
 -> SBool)
-> (SBV a
    -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, [ProofStep z]))
-> Symbolic (SBool, CalcStrategy)
calcSteps Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, [ProofStep z])
steps = do (a, b, c, d, e) <- (,,,,) (SBV a
 -> SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> (SBV a, SBV b, SBV c, SBV d, SBV e))
-> SymbolicT IO (SBV a)
-> SymbolicT
     IO
     (SBV b
      -> SBV c -> SBV d -> SBV e -> (SBV a, SBV b, SBV c, SBV d, SBV e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SymbolicT IO (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)) SymbolicT
  IO
  (SBV b
   -> SBV c -> SBV d -> SBV e -> (SBV a, SBV b, SBV c, SBV d, SBV e))
-> SymbolicT IO (SBV b)
-> SymbolicT
     IO (SBV c -> SBV d -> SBV e -> (SBV a, SBV b, SBV c, SBV d, SBV e))
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV b)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)) SymbolicT
  IO (SBV c -> SBV d -> SBV e -> (SBV a, SBV b, SBV c, SBV d, SBV e))
-> SymbolicT IO (SBV c)
-> SymbolicT
     IO (SBV d -> SBV e -> (SBV a, SBV b, SBV c, SBV d, SBV e))
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV c)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)) SymbolicT
  IO (SBV d -> SBV e -> (SBV a, SBV b, SBV c, SBV d, SBV e))
-> SymbolicT IO (SBV d)
-> SymbolicT IO (SBV e -> (SBV a, SBV b, SBV c, SBV d, SBV e))
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV d)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy nd -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nd)) SymbolicT IO (SBV e -> (SBV a, SBV b, SBV c, SBV d, SBV e))
-> SymbolicT IO (SBV e)
-> SymbolicT IO (SBV a, SBV b, SBV c, SBV d, SBV e)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> SymbolicT IO (SBV e)
forall a. SymVal a => String -> Symbolic (SBV a)
free (Proxy ne -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ne))
                               pure (result (Forall a) (Forall b) (Forall c) (Forall d) (Forall e), mkCalcSteps (steps a b c d e))

-- | Captures the schema for an inductive proof
data InductionStrategy = InductionStrategy { InductionStrategy -> SBool
inductionIntros         :: SBool
                                           , InductionStrategy -> SBool
inductionBaseCase       :: SBool
                                           , InductionStrategy -> [([Helper], SBool)]
inductionProofSteps     :: [([Helper], SBool)]
                                           , InductionStrategy -> String
inductionBaseFailureMsg :: String
                                           , InductionStrategy -> SBool
inductiveStep           :: SBool
                                           }

-- | Are we doing strong induction or regular induction?
data InductionStyle = RegularInduction | StrongInduction

getInductionStrategySaturatables :: InductionStrategy -> [SBool]
getInductionStrategySaturatables :: InductionStrategy -> [SBool]
getInductionStrategySaturatables (InductionStrategy SBool
inductionIntros
                                                    SBool
inductionBaseCase
                                                    [([Helper], SBool)]
inductionProofSteps
                                                    String
_inductionBaseFailureMsg
                                                    SBool
inductiveStep)
  = SBool
inductionIntros SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: SBool
inductionBaseCase SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: SBool
inductiveStep SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [([Helper], SBool)] -> [SBool]
proofStepSaturatables [([Helper], SBool)]
inductionProofSteps

-- | A class for doing inductive proofs, with the possibility of explicit steps.
class Inductive a steps where
   -- | Inductively prove a lemma, using the default config.
   -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
   -- partial correctness is guaranteed if non-terminating functions are involved.
   induct  :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof

   -- | Inductively prove a lemma, using strong induction, using the default config.
   -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
   -- partial correctness is guaranteed if non-terminating functions are involved.
   sInduct :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof

   -- | Inductively prove a theorem. Same as 'induct', but tagged as a theorem, using the default config.
   -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
   -- partial correctness is guaranteed if non-terminating functions are involved.
   inductThm :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof

   -- | Inductively prove a theorem, using strong induction. Same as 'sInduct', but tagged as a theorem, using the default config.
   -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
   -- partial correctness is guaranteed if non-terminating functions are involved.
   sInductThm :: Proposition a => String -> a -> (Proof -> steps) -> KD Proof

   -- | Same as 'induct', but with the given solver configuration.
   -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
   -- partial correctness is guaranteed if non-terminating functions are involved.
   inductWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof

   -- | Same as 'sInduct', but with the given solver configuration.
   -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
   -- partial correctness is guaranteed if non-terminating functions are involved.
   sInductWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof

   -- | Same as 'inductThm', but with the given solver configuration.
   -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
   -- partial correctness is guaranteed if non-terminating functions are involved.
   inductThmWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof

   -- | Same as 'sInductThm', but with the given solver configuration.
   -- Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only
   -- partial correctness is guaranteed if non-terminating functions are involved.
   sInductThmWith :: Proposition a => SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof

   induct            String
nm a
p Proof -> steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg  -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
inductWith                           SMTConfig
cfg String
nm a
p Proof -> steps
steps
   inductThm         String
nm a
p Proof -> steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg  -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
inductThmWith                        SMTConfig
cfg String
nm a
p Proof -> steps
steps
   inductWith    SMTConfig
cfg String
nm a
p Proof -> steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg' -> InductionStyle
-> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
InductionStyle
-> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
inductGeneric InductionStyle
RegularInduction Bool
False (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p Proof -> steps
steps
   inductThmWith SMTConfig
cfg String
nm a
p Proof -> steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg' -> InductionStyle
-> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
InductionStyle
-> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
inductGeneric InductionStyle
RegularInduction Bool
True  (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p Proof -> steps
steps

   sInduct            String
nm a
p Proof -> steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg  -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
sInductWith                          SMTConfig
cfg String
nm a
p Proof -> steps
steps
   sInductThm         String
nm a
p Proof -> steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg  -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
sInductThmWith                       SMTConfig
cfg String
nm a
p Proof -> steps
steps
   sInductWith    SMTConfig
cfg String
nm a
p Proof -> steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg' -> InductionStyle
-> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
InductionStyle
-> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
inductGeneric  InductionStyle
StrongInduction Bool
False (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p Proof -> steps
steps
   sInductThmWith SMTConfig
cfg String
nm a
p Proof -> steps
steps = KD SMTConfig
getKDConfig KD SMTConfig -> (SMTConfig -> KD Proof) -> KD Proof
forall a b. KD a -> (a -> KD b) -> KD b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTConfig
cfg' -> InductionStyle
-> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
forall a steps.
(Inductive a steps, Proposition a) =>
InductionStyle
-> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
inductGeneric  InductionStyle
StrongInduction Bool
True  (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p Proof -> steps
steps

   -- | Internal, shouldn't be needed outside the library
   {-# MINIMAL inductionStrategy #-}
   inductionStrategy :: Proposition a => InductionStyle -> a -> (Proof -> steps) -> Symbolic InductionStrategy

   inductGeneric :: Proposition a => InductionStyle -> Bool -> SMTConfig -> String -> a -> (Proof -> steps) -> KD Proof
   inductGeneric InductionStyle
style Bool
tagTheorem cfg :: SMTConfig
cfg@SMTConfig{kdOptions :: SMTConfig -> KDOptions
kdOptions = KDOptions{Bool
measureTime :: KDOptions -> Bool
measureTime :: Bool
measureTime}} String
nm a
result Proof -> steps
steps = do
      kdSt <- KD KDState
getKDState

      liftIO $ runSMTWith cfg $ do

         qSaturateSavingObservables result -- make sure we saturate the result, i.e., get all it's UI's, types etc. pop out

         let strong = case InductionStyle
style of
                        InductionStyle
RegularInduction -> String
""
                        InductionStyle
StrongInduction  -> String
" (strong)"

         message cfg $ "Inductive " ++ (if tagTheorem then "theorem" else "lemma") ++ strong ++ ": " ++ nm ++ "\n"

         mbStartTime <- getTimeStampIf measureTime

         strategy@InductionStrategy { inductionIntros
                                    , inductionBaseCase
                                    , inductionProofSteps
                                    , inductionBaseFailureMsg
                                    , inductiveStep
                                    } <- inductionStrategy style result steps

         let stepHelpers = (([Helper], SBool) -> [Helper]) -> [([Helper], SBool)] -> [Helper]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Helper], SBool) -> [Helper]
forall a b. (a, b) -> a
fst [([Helper], SBool)]
inductionProofSteps

             finish [NominalDiffTime]
et [Proof]
helpers (Int, Maybe NominalDiffTime)
d = SMTConfig
-> String
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishKD SMTConfig
cfg (String
"Q.E.D." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
modulo) (Int, Maybe NominalDiffTime)
d [NominalDiffTime]
et
               where (RootOfTrust
_, String
modulo) = String -> [Proof] -> (RootOfTrust, String)
calculateRootOfTrust String
nm [Proof]
helpers

         -- Collect all subterms and saturate them
         mapM_ qSaturateSavingObservables $ getInductionStrategySaturatables strategy

         query $ do

          queryDebug [nm ++ ": Induction, proving base case:"]
          checkSatThen cfg kdSt "Base" True (Just inductionIntros) inductionBaseCase [] [nm, "Base"] Nothing
                       (Just (liftIO (putStrLn inductionBaseFailureMsg)))
                       (finish [] [])

          let loop Int
i SBool
accum (([Helper]
by, SBool
s):[([Helper], SBool)]
ss) = do

                  -- Prove that the assumptions follow, if any
                  case [Helper] -> [SBool]
getHelperAssumes [Helper]
by of
                    [] -> () -> Query ()
forall a. a -> QueryT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                    [SBool]
as -> SMTConfig
-> KDState
-> String
-> Bool
-> Maybe SBool
-> SBool
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> Query ()
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Bool
-> Maybe SBool
-> a
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
checkSatThen SMTConfig
cfg KDState
kdSt String
"Asms"
                                                Bool
True
                                                (SBool -> Maybe SBool
forall a. a -> Maybe a
Just SBool
inductionIntros)
                                                ([SBool] -> SBool
sAnd [SBool]
as)
                                                []
                                                [String
"", Int -> String
forall a. Show a => a -> String
show Int
i]
                                                ([String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
nm, Int -> String
forall a. Show a => a -> String
show Int
i, String
"Assumptions"])
                                                Maybe (IO ())
forall a. Maybe a
Nothing
                                                ([NominalDiffTime]
-> [Proof] -> (Int, Maybe NominalDiffTime) -> IO ()
finish [] [])

                  [String] -> Query ()
queryDebug [String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Induction, proving step: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i]

                  Int
-> SMTConfig
-> KDState
-> Either (String, SBool) ([(String, SBool)], SBool)
-> String
-> SBool
-> String
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> Query ()
forall (m :: * -> *) a.
(Monad m, SolverContext m, MonadIO m, MonadQuery m,
 Proposition a) =>
Int
-> SMTConfig
-> KDState
-> Either (String, SBool) ([(String, SBool)], SBool)
-> String
-> a
-> String
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> m ()
proveAllCases Int
i SMTConfig
cfg KDState
kdSt (Int
-> [Helper] -> Either (String, SBool) ([(String, SBool)], SBool)
stepCases Int
i [Helper]
by) String
"Step" SBool
s String
nm ([NominalDiffTime]
-> [Proof] -> (Int, Maybe NominalDiffTime) -> IO ()
finish [] ([Helper] -> [Proof]
getHelperProofs [Helper]
by))

                  Int -> SBool -> [([Helper], SBool)] -> QueryT IO SBool
loop (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (SBool
accum SBool -> SBool -> SBool
.&& SBool
s) [([Helper], SBool)]
ss

              loop Int
_ SBool
accum [] = SBool -> QueryT IO SBool
forall a. a -> QueryT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SBool
accum

          -- Get the schema
          indSchema <- loop (1::Int) sTrue inductionProofSteps

          -- Do the final proof:
          queryDebug [nm ++ ": Induction, proving inductive step:"]
          checkSatThen cfg kdSt "Step"
                                True
                                (Just (inductionIntros .=> indSchema))
                                inductiveStep
                                []
                                [nm, "Step"]
                                Nothing
                                Nothing $ \(Int, Maybe NominalDiffTime)
d -> do

            mbElapsed <- Maybe UTCTime -> IO (Maybe NominalDiffTime)
forall (m :: * -> *).
MonadIO m =>
Maybe UTCTime -> m (Maybe NominalDiffTime)
getElapsedTime Maybe UTCTime
mbStartTime

            let (ros, modulo) = calculateRootOfTrust nm (getHelperProofs stepHelpers)
            finishKD cfg ("Q.E.D." ++ modulo) d (catMaybes [mbElapsed])

            pure $ Proof { rootOfTrust = ros
                         , isUserAxiom = False
                         , getProof    = label nm $ quantifiedBool result
                         , getProp     = toDyn result
                         , proofName   = nm
                         }

-- | Induction over 'SInteger'.
instance (KnownSymbol nk, EqSymbolic z) => Inductive (Forall nk Integer -> SBool) (SInteger -> (SBool, [ProofStep z])) where
   inductionStrategy :: Proposition (Forall nk Integer -> SBool) =>
InductionStyle
-> (Forall nk Integer -> SBool)
-> (Proof -> SInteger -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nk Integer -> SBool
result Proof -> SInteger -> (SBool, [ProofStep z])
steps = do
       let predicate :: SInteger -> SBool
predicate SInteger
k = Forall nk Integer -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k)
           nk :: String
nk          = Proxy nk -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nk)

       k <- String -> Symbolic SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nk

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> SBool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" (SBool -> Proof) -> SBool -> Proof
forall a b. (a -> b) -> a -> b
$                                                   Forall nk Integer -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k)
                  InductionStyle
StrongInduction  -> String -> (Forall nk Integer -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nk Integer -> SBool) -> Proof)
-> (Forall nk Integer -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
k' :: Forall nk Integer) -> SInteger
k' SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k SBool -> SBool -> SBool
.=> Forall nk Integer -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k')
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k

       pure InductionStrategy {
                inductionIntros         = k .>= 0 .&& calcIntros
              , inductionBaseCase       = predicate 0
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0."
              , inductiveStep           = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1))
              }

-- | Induction over 'SInteger' taking an extra argument.
instance forall na a nk z. (KnownSymbol na, SymVal a, KnownSymbol nk, EqSymbolic z)
      => Inductive (Forall nk Integer -> Forall na a -> SBool)
                   (SInteger -> SBV a -> (SBool, [ProofStep z])) where
   inductionStrategy :: Proposition (Forall nk Integer -> Forall na a -> SBool) =>
InductionStyle
-> (Forall nk Integer -> Forall na a -> SBool)
-> (Proof -> SInteger -> SBV a -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nk Integer -> Forall na a -> SBool
result Proof -> SInteger -> SBV a -> (SBool, [ProofStep z])
steps = do
       let predicate :: SInteger -> SBV a -> SBool
predicate SInteger
k SBV a
a = Forall nk Integer -> Forall na a -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a)
           nk :: String
nk            = Proxy nk -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nk)
           na :: String
na            = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)

       k <- String -> Symbolic SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nk
       a <- free na

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> (Forall na a -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> SBool) -> Proof)
-> (Forall na a -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                                 Forall na a
a' ->                           Forall nk Integer -> Forall na a -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k)  (Forall na a
a' :: Forall na a)
                  InductionStyle
StrongInduction  -> String -> (Forall nk Integer -> Forall na a -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nk Integer -> Forall na a -> SBool) -> Proof)
-> (Forall nk Integer -> Forall na a -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
k' :: Forall nk Integer) Forall na a
a' -> SInteger
0 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k' SBool -> SBool -> SBool
.&& SInteger
k' SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k SBool -> SBool -> SBool
.=> Forall nk Integer -> Forall na a -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k') (Forall na a
a' :: Forall na a)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k a

       pure InductionStrategy {
                inductionIntros         = k .>= 0 .&& calcIntros
              , inductionBaseCase       = predicate 0 a
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0."
              , inductiveStep           = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1) a)
              }

-- | Induction over 'SInteger' taking two extra arguments.
instance forall na a nb b nk z. (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nk, EqSymbolic z)
      => Inductive (Forall nk Integer -> Forall na a -> Forall nb b -> SBool)
                   (SInteger -> SBV a -> SBV b -> (SBool, [ProofStep z])) where
   inductionStrategy :: Proposition
  (Forall nk Integer -> Forall na a -> Forall nb b -> SBool) =>
InductionStyle
-> (Forall nk Integer -> Forall na a -> Forall nb b -> SBool)
-> (Proof -> SInteger -> SBV a -> SBV b -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nk Integer -> Forall na a -> Forall nb b -> SBool
result Proof -> SInteger -> SBV a -> SBV b -> (SBool, [ProofStep z])
steps = do
       let predicate :: SInteger -> SBV a -> SBV b -> SBool
predicate SInteger
k SBV a
a SBV b
b = Forall nk Integer -> Forall na a -> Forall nb b -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b)
           nk :: String
nk              = Proxy nk -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nk)
           na :: String
na              = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb              = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)

       k <- String -> Symbolic SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nk
       a <- free na
       b <- free nb

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> (Forall na a -> Forall nb b -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> Forall nb b -> SBool) -> Proof)
-> (Forall na a -> Forall nb b -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                                 Forall na a
a' Forall nb b
b' ->                           Forall nk Integer -> Forall na a -> Forall nb b -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b)
                  InductionStyle
StrongInduction  -> String
-> (Forall nk Integer -> Forall na a -> Forall nb b -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nk Integer -> Forall na a -> Forall nb b -> SBool)
 -> Proof)
-> (Forall nk Integer -> Forall na a -> Forall nb b -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
k' :: Forall nk Integer) Forall na a
a' Forall nb b
b' -> SInteger
0 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k' SBool -> SBool -> SBool
.&& SInteger
k' SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k SBool -> SBool -> SBool
.=> Forall nk Integer -> Forall na a -> Forall nb b -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k a b

       pure InductionStrategy {
                inductionIntros         = k .>= 0 .&& calcIntros
              , inductionBaseCase       = predicate 0 a b
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0."
              , inductiveStep           = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1) a b)
              }

-- | Induction over 'SInteger' taking three extra arguments.
instance forall na a nb b nc c nk z. (KnownSymbol na, SymVal a , KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nk, EqSymbolic z)
     => Inductive (Forall nk Integer -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
                  (SInteger -> SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z]))
 where
   inductionStrategy :: Proposition
  (Forall nk Integer
   -> Forall na a -> Forall nb b -> Forall nc c -> SBool) =>
InductionStyle
-> (Forall nk Integer
    -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> (Proof
    -> SInteger -> SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nk Integer
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result Proof
-> SInteger -> SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z])
steps = do
       let predicate :: SInteger -> SBV a -> SBV b -> SBV c -> SBool
predicate SInteger
k SBV a
a SBV b
b SBV c
c = Forall nk Integer
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c)
           nk :: String
nk                = Proxy nk -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nk)
           na :: String
na                = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nc :: String
nc                = Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)

       k <- String -> Symbolic SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nk
       a <- free na
       b <- free nb
       c <- free nc

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String
-> (Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof)
-> (Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                                 Forall na a
a' Forall nb b
b' Forall nc c
c' ->                           Forall nk Integer
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c)
                  InductionStyle
StrongInduction  -> String
-> (Forall nk Integer
    -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nk Integer
  -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
 -> Proof)
-> (Forall nk Integer
    -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
k' :: Forall nk Integer) Forall na a
a' Forall nb b
b' Forall nc c
c' -> SInteger
0 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k' SBool -> SBool -> SBool
.&& SInteger
k' SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k SBool -> SBool -> SBool
.=> Forall nk Integer
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k a b c

       pure InductionStrategy {
                inductionIntros         = k .>= 0 .&& calcIntros
              , inductionBaseCase       = predicate 0 a b c
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0."
              , inductiveStep           = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1) a b c)
              }

-- | Induction over 'SInteger' taking four extra arguments.
instance forall na a nb b nc c nd d nk z. (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol nk, EqSymbolic z)
      => Inductive (Forall nk Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
                   (SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z])) where
   inductionStrategy :: Proposition
  (Forall nk Integer
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> SBool) =>
InductionStyle
-> (Forall nk Integer
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> (Proof
    -> SInteger
    -> SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nk Integer
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result Proof
-> SInteger
-> SBV a
-> SBV b
-> SBV c
-> SBV d
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> SBool
predicate SInteger
k SBV a
a SBV b
b SBV c
c SBV d
d = Forall nk Integer
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c) (SBV d -> Forall nd d
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV d
d)
           nk :: String
nk                  = Proxy nk -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nk)
           na :: String
na                  = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                  = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nc :: String
nc                  = Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)
           nd :: String
nd                  = Proxy nd -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nd)

       k <- String -> Symbolic SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nk
       a <- free na
       b <- free nb
       c <- free nc
       d <- free nd

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String
-> (Forall na a
    -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a
  -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
 -> Proof)
-> (Forall na a
    -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \                                 Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' ->                           Forall nk Integer
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d)
                  InductionStyle
StrongInduction  -> String
-> (Forall nk Integer
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nk Integer
  -> Forall na a
  -> Forall nb b
  -> Forall nc c
  -> Forall nd d
  -> SBool)
 -> Proof)
-> (Forall nk Integer
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
k' :: Forall nk Integer) Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' -> SInteger
0 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k' SBool -> SBool -> SBool
.&& SInteger
k' SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
k SBool -> SBool -> SBool
.=> Forall nk Integer
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SInteger -> Forall nk Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
k') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih k a b c d

       pure InductionStrategy {
                inductionIntros         = k .>= 0 .&& calcIntros
              , inductionBaseCase       = predicate 0 a b c d
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nk ++ " = 0."
              , inductiveStep           = observeIf not ("P(" ++ nk ++ "+1)") (predicate (k+1) a b c d)
              }

-- Given a user name for the list, get a name for the element, in the most suggestive way possible
--   xs  -> x
--   xss -> xs
--   foo -> fooElt
singular :: String -> String
singular :: String -> String
singular String
n = case String -> String
forall a. [a] -> [a]
reverse String
n of
               Char
's':Char
_:String
_ -> String -> String
forall a. HasCallStack => [a] -> [a]
init String
n
               String
_       -> String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Elt"

-- | Metric for induction over lists. Currently we simply require the list we're assuming correctness for is shorter in length, which
-- is a measure that is guarenteed >= 0. Note that we use .<= here, since when called, the second argument is always the tail
-- of the induction argument. Later on, we might want to generalize this to a user given measure.
lexLeq :: SymVal a => SList a -> SList a -> SBool
lexLeq :: forall a. SymVal a => SList a -> SList a -> SBool
lexLeq SList a
xs SList a
ys = SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
SL.length SList a
xs SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
SL.length SList a
ys

-- | Metric for induction over two lists. We use lexicographic ordering. Again, we don't expose this directly. The
-- second argument is always the tail of the induction argument, so we use .<=. Later on, we might want to generalize
-- this to a user given measure.
lexLeq2 :: (SymVal a, SymVal b) => (SList a, SList b) -> (SList a, SList b) -> SBool
lexLeq2 :: forall a b.
(SymVal a, SymVal b) =>
(SList a, SList b) -> (SList a, SList b) -> SBool
lexLeq2 (SList a
xs', SList b
ys') (SList a
xs, SList b
ys) =   SInteger
lxs' SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
lxs                     -- tail of the first is the same, i.e., the first went down. So, we're good.
                            SBool -> SBool -> SBool
.|| (    SInteger
lxs' SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
SL.length SList a
xs   -- OR, the tail did not grow (note the +1 due to us receiving the tail)
                                 SBool -> SBool -> SBool
.&& SInteger
lys' SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
lys                -- and the tail of the second went down. 
                                )
 where lxs :: SInteger
lxs  = SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
SL.length SList a
xs
       lys :: SInteger
lys  = SList b -> SInteger
forall a. SymVal a => SList a -> SInteger
SL.length SList b
ys
       lxs' :: SInteger
lxs' = SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
SL.length SList a
xs'
       lys' :: SInteger
lys' = SList b -> SInteger
forall a. SymVal a => SList a -> SInteger
SL.length SList b
ys'

-- | Induction over 'SList'.
instance (KnownSymbol nx, SymVal x, EqSymbolic z)
      => Inductive (Forall nx [x] -> SBool)
                   (SBV x -> SList x -> (SBool, [ProofStep z]))
 where
   inductionStrategy :: Proposition (Forall nx [x] -> SBool) =>
InductionStyle
-> (Forall nx [x] -> SBool)
-> (Proof -> SBV x -> SList x -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x] -> SBool
result Proof -> SBV x -> SList x -> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SBool
predicate SList x
xs = Forall nx [x] -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)
           nxs :: String
nxs          = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx           = String -> String
singular String
nxs

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> SBool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" (SBool -> Proof) -> SBool -> Proof
forall a b. (a -> b) -> a -> b
$                                                       Forall nx [x] -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)
                  InductionStyle
StrongInduction  -> String -> (Forall nx [x] -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x] -> SBool) -> Proof)
-> (Forall nx [x] -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) -> SList x
xs' SList x -> SList x -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`lexLeq` SList x
xs SBool -> SBool -> SBool
.=> Forall nx [x] -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs')
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []."
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs))
              }

-- | Induction over 'SList' taking an extra argument
instance forall na a nx x z. (KnownSymbol na, SymVal a, KnownSymbol nx, SymVal x, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall na a -> SBool)
                   (SBV x -> SList x -> SBV a -> (SBool, [ProofStep z]))
 where
   inductionStrategy :: Proposition (Forall nx [x] -> Forall na a -> SBool) =>
InductionStyle
-> (Forall nx [x] -> Forall na a -> SBool)
-> (Proof -> SBV x -> SList x -> SBV a -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x] -> Forall na a -> SBool
result Proof -> SBV x -> SList x -> SBV a -> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SBV a -> SBool
predicate SList x
xs SBV a
a = Forall nx [x] -> Forall na a -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a)
           na :: String
na             = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nxs :: String
nxs            = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx             = String -> String
singular String
nxs

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs
       a  <- free na

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> (Forall na a -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> SBool) -> Proof)
-> (Forall na a -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                              Forall na a
a' ->                     Forall nx [x] -> Forall na a -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (Forall na a
a' :: Forall na a)
                  InductionStyle
StrongInduction  -> String -> (Forall nx [x] -> Forall na a -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x] -> Forall na a -> SBool) -> Proof)
-> (Forall nx [x] -> Forall na a -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) Forall na a
a' -> SList x
xs' SList x -> SList x -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`lexLeq` SList x
xs SBool -> SBool -> SBool
.=> Forall nx [x] -> Forall na a -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (Forall na a
a' :: Forall na a)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil a
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []."
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a)
              }

-- | Induction over 'SList' taking two extra arguments
instance forall na a nb b nx x z. (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nx, SymVal x, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall na a -> Forall nb b -> SBool)
                   (SBV x -> SList x -> SBV a -> SBV b -> (SBool, [ProofStep z]))
 where
   inductionStrategy :: Proposition
  (Forall nx [x] -> Forall na a -> Forall nb b -> SBool) =>
InductionStyle
-> (Forall nx [x] -> Forall na a -> Forall nb b -> SBool)
-> (Proof
    -> SBV x -> SList x -> SBV a -> SBV b -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x] -> Forall na a -> Forall nb b -> SBool
result Proof
-> SBV x -> SList x -> SBV a -> SBV b -> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SBV a -> SBV b -> SBool
predicate SList x
xs SBV a
a SBV b
b = Forall nx [x] -> Forall na a -> Forall nb b -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b)
           na :: String
na               = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb               = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nxs :: String
nxs              = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx               = String -> String
singular String
nxs

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs
       a  <- free na
       b  <- free nb

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> (Forall na a -> Forall nb b -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> Forall nb b -> SBool) -> Proof)
-> (Forall na a -> Forall nb b -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                              Forall na a
a' Forall nb b
b' ->                     Forall nx [x] -> Forall na a -> Forall nb b -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x] -> Forall na a -> Forall nb b -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x] -> Forall na a -> Forall nb b -> SBool) -> Proof)
-> (Forall nx [x] -> Forall na a -> Forall nb b -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) Forall na a
a' Forall nb b
b' -> SList x
xs' SList x -> SList x -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`lexLeq` SList x
xs SBool -> SBool -> SBool
.=> Forall nx [x] -> Forall na a -> Forall nb b -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil a b
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []."
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a b)
              }

-- | Induction over 'SList' taking three extra arguments
instance forall na a nb b nc c nx x z. (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nx, SymVal x, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
                   (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z]))
 where
   inductionStrategy :: Proposition
  (Forall nx [x]
   -> Forall na a -> Forall nb b -> Forall nc c -> SBool) =>
InductionStyle
-> (Forall nx [x]
    -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV a
    -> SBV b
    -> SBV c
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool
result Proof
-> SBV x
-> SList x
-> SBV a
-> SBV b
-> SBV c
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SBV a -> SBV b -> SBV c -> SBool
predicate SList x
xs SBV a
a SBV b
b SBV c
c = Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c)
           na :: String
na                 = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                 = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nc :: String
nc                 = Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)
           nxs :: String
nxs                = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx                 = String -> String
singular String
nxs

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs
       a  <- free na
       b  <- free nb
       c  <- free nc

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String
-> (Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof)
-> (Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                              Forall na a
a' Forall nb b
b' Forall nc c
c' ->                     Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x]
    -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x]
  -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
 -> Proof)
-> (Forall nx [x]
    -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) Forall na a
a' Forall nb b
b' Forall nc c
c' -> SList x
xs' SList x -> SList x -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`lexLeq` SList x
xs SBool -> SBool -> SBool
.=> Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil a b c
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []."
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a b c)
              }

-- | Induction over 'SList' taking four extra arguments
instance forall na a nb b nc c nd d nx x z. (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol nx, SymVal x, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
                   (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z]))
 where
   inductionStrategy :: Proposition
  (Forall nx [x]
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> SBool) =>
InductionStyle
-> (Forall nx [x]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result Proof
-> SBV x
-> SList x
-> SBV a
-> SBV b
-> SBV c
-> SBV d
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SBV a -> SBV b -> SBV c -> SBV d -> SBool
predicate SList x
xs SBV a
a SBV b
b SBV c
c SBV d
d = Forall nx [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c) (SBV d -> Forall nd d
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV d
d)
           na :: String
na                   = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                   = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nc :: String
nc                   = Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)
           nd :: String
nd                   = Proxy nd -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nd)
           nxs :: String
nxs                  = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx                   = String -> String
singular String
nxs

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs
       a  <- free na
       b  <- free nb
       c  <- free nc
       d  <- free nd

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String
-> (Forall na a
    -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a
  -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
 -> Proof)
-> (Forall na a
    -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \                              Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' ->                     Forall nx [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x]
  -> Forall na a
  -> Forall nb b
  -> Forall nc c
  -> Forall nd d
  -> SBool)
 -> Proof)
-> (Forall nx [x]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' -> SList x
xs' SList x -> SList x -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`lexLeq` SList x
xs SBool -> SBool -> SBool
.=> Forall nx [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c d

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil a b c d
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []."
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a b c d)
              }

-- | Induction over 'SList' taking five extra arguments
instance forall na a nb b nc c nd d ne e nx x z. (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, KnownSymbol nx, SymVal x, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool)
                   (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, [ProofStep z]))
 where
   inductionStrategy :: Proposition
  (Forall nx [x]
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> Forall ne e
   -> SBool) =>
InductionStyle
-> (Forall nx [x]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result Proof
-> SBV x
-> SList x
-> SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool
predicate SList x
xs SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e = Forall nx [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c) (SBV d -> Forall nd d
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV d
d) (SBV e -> Forall ne e
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV e
e)
           na :: String
na                     = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                     = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nc :: String
nc                     = Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)
           nd :: String
nd                     = Proxy nd -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nd)
           ne :: String
ne                     = Proxy ne -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ne)
           nxs :: String
nxs                    = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx                     = String -> String
singular String
nxs

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs
       a  <- free na
       b  <- free nb
       c  <- free nc
       d  <- free nd
       e  <- free ne

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String
-> (Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a
  -> Forall nb b
  -> Forall nc c
  -> Forall nd d
  -> Forall ne e
  -> SBool)
 -> Proof)
-> (Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \                              Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' Forall ne e
e' ->                     Forall nx [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d) (Forall ne e
e' :: Forall ne e)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x]
  -> Forall na a
  -> Forall nb b
  -> Forall nc c
  -> Forall nd d
  -> Forall ne e
  -> SBool)
 -> Proof)
-> (Forall nx [x]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' Forall ne e
e' -> SList x
xs' SList x -> SList x -> SBool
forall a. SymVal a => SList a -> SList a -> SBool
`lexLeq` SList x
xs SBool -> SBool -> SBool
.=> Forall nx [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d) (Forall ne e
e' :: Forall ne e)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs a b c d e

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil a b c d e
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = []."
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ")") (predicate (x SL..: xs) a b c d e)
              }

-- | Induction over two lists, simultaneously
instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall ny [y] -> SBool)
                   (SBV x -> SList x -> SBV y -> SList y -> (SBool, [ProofStep z]))
  where
   inductionStrategy :: Proposition (Forall nx [x] -> Forall ny [y] -> SBool) =>
InductionStyle
-> (Forall nx [x] -> Forall ny [y] -> SBool)
-> (Proof
    -> SBV x -> SList x -> SBV y -> SList y -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x] -> Forall ny [y] -> SBool
result Proof
-> SBV x -> SList x -> SBV y -> SList y -> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SList y -> SBool
predicate SList x
xs SList y
ys = Forall nx [x] -> Forall ny [y] -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys)
           nxs :: String
nxs             = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx              = String -> String
singular String
nxs
           nys :: String
nys             = Proxy ny -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ny)
           ny :: String
ny              = String -> String
singular String
nys

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs

       y  <- free ny
       ys <- free nys

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> SBool -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" (SBool -> Proof) -> SBool -> Proof
forall a b. (a -> b) -> a -> b
$                                                                                                   Forall nx [x] -> Forall ny [y] -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys)
                  InductionStyle
StrongInduction  -> String -> (Forall nx [x] -> Forall ny [y] -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x] -> Forall ny [y] -> SBool) -> Proof)
-> (Forall nx [x] -> Forall ny [y] -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) (Forall SList y
ys' :: Forall ny [y]) -> (SList x
xs', SList y
ys') (SList x, SList y) -> (SList x, SList y) -> SBool
forall a b.
(SymVal a, SymVal b) =>
(SList a, SList b) -> (SList a, SList b) -> SBool
`lexLeq2` (SList x
xs, SList y
ys) SBool -> SBool -> SBool
.=> Forall nx [x] -> Forall ny [y] -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys')
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil SL.nil .&& predicate SL.nil (y SL..: ys) .&& predicate (x SL..: xs) SL.nil
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys))
              }

-- | Induction over two lists, simultaneously, taking one extra argument
instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool)
                   (SBV x -> SList x -> SBV y -> SList y -> SBV a -> (SBool, [ProofStep z]))
  where
   inductionStrategy :: Proposition
  (Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool) =>
InductionStyle
-> (Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV y
    -> SList y
    -> SBV a
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool
result Proof
-> SBV x
-> SList x
-> SBV y
-> SList y
-> SBV a
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SList y -> SBV a -> SBool
predicate SList x
xs SList y
ys SBV a
a = Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a)
           nxs :: String
nxs               = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx                = String -> String
singular String
nxs
           nys :: String
nys               = Proxy ny -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ny)
           ny :: String
ny                = String -> String
singular String
nys
           na :: String
na                = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs

       y  <- free ny
       ys <- free nys

       a  <- free na

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> (Forall na a -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> SBool) -> Proof)
-> (Forall na a -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                                                            Forall na a
a' ->                                   Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys)  (Forall na a
a' :: Forall na a)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool) -> Proof)
-> (Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) (Forall SList y
ys' :: Forall ny [y]) Forall na a
a' -> (SList x
xs', SList y
ys') (SList x, SList y) -> (SList x, SList y) -> SBool
forall a b.
(SymVal a, SymVal b) =>
(SList a, SList b) -> (SList a, SList b) -> SBool
`lexLeq2` (SList x
xs, SList y
ys) SBool -> SBool -> SBool
.=> Forall nx [x] -> Forall ny [y] -> Forall na a -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys') (Forall na a
a' :: Forall na a)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil SL.nil a .&& predicate SL.nil (y SL..: ys) a .&& predicate (x SL..: xs) SL.nil a
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a)
              }

-- | Induction over two lists, simultaneously, taking two extra arguments
instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> Forall nb b -> SBool)
                   (SBV x -> SList x -> SBV y -> SList y -> SBV a -> SBV b -> (SBool, [ProofStep z]))
  where
   inductionStrategy :: Proposition
  (Forall nx [x]
   -> Forall ny [y] -> Forall na a -> Forall nb b -> SBool) =>
InductionStyle
-> (Forall nx [x]
    -> Forall ny [y] -> Forall na a -> Forall nb b -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV y
    -> SList y
    -> SBV a
    -> SBV b
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x]
-> Forall ny [y] -> Forall na a -> Forall nb b -> SBool
result Proof
-> SBV x
-> SList x
-> SBV y
-> SList y
-> SBV a
-> SBV b
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SList y -> SBV a -> SBV b -> SBool
predicate SList x
xs SList y
ys SBV a
a SBV b
b = Forall nx [x]
-> Forall ny [y] -> Forall na a -> Forall nb b -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b)
           nxs :: String
nxs                 = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx                  = String -> String
singular String
nxs
           nys :: String
nys                 = Proxy ny -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ny)
           ny :: String
ny                  = String -> String
singular String
nys
           na :: String
na                  = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                  = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs

       y  <- free ny
       ys <- free nys

       a  <- free na
       b  <- free nb

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String -> (Forall na a -> Forall nb b -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> Forall nb b -> SBool) -> Proof)
-> (Forall na a -> Forall nb b -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                                                            Forall na a
a' Forall nb b
b' ->                                   Forall nx [x]
-> Forall ny [y] -> Forall na a -> Forall nb b -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x]
    -> Forall ny [y] -> Forall na a -> Forall nb b -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x]
  -> Forall ny [y] -> Forall na a -> Forall nb b -> SBool)
 -> Proof)
-> (Forall nx [x]
    -> Forall ny [y] -> Forall na a -> Forall nb b -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) (Forall SList y
ys' :: Forall ny [y]) Forall na a
a' Forall nb b
b' -> (SList x
xs', SList y
ys') (SList x, SList y) -> (SList x, SList y) -> SBool
forall a b.
(SymVal a, SymVal b) =>
(SList a, SList b) -> (SList a, SList b) -> SBool
`lexLeq2` (SList x
xs, SList y
ys) SBool -> SBool -> SBool
.=> Forall nx [x]
-> Forall ny [y] -> Forall na a -> Forall nb b -> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil SL.nil a b .&& predicate SL.nil (y SL..: ys) a b .&& predicate (x SL..: xs) SL.nil a b
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a b)
              }

-- | Induction over two lists, simultaneously, taking three extra arguments
instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
                   (SBV x -> SList x -> SBV y -> SList y -> SBV a -> SBV b -> SBV c -> (SBool, [ProofStep z]))
  where
   inductionStrategy :: Proposition
  (Forall nx [x]
   -> Forall ny [y]
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> SBool) =>
InductionStyle
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV y
    -> SList y
    -> SBV a
    -> SBV b
    -> SBV c
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> SBool
result Proof
-> SBV x
-> SList x
-> SBV y
-> SList y
-> SBV a
-> SBV b
-> SBV c
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SList y -> SBV a -> SBV b -> SBV c -> SBool
predicate SList x
xs SList y
ys SBV a
a SBV b
b SBV c
c = Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c)
           nxs :: String
nxs                   = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx                    = String -> String
singular String
nxs
           nys :: String
nys                   = Proxy ny -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ny)
           ny :: String
ny                    = String -> String
singular String
nys
           na :: String
na                    = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                    = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nc :: String
nc                    = Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs

       y  <- free ny
       ys <- free nys

       a  <- free na
       b  <- free nb
       c  <- free nc

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String
-> (Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof)
-> (Forall na a -> Forall nb b -> Forall nc c -> SBool) -> Proof
forall a b. (a -> b) -> a -> b
$ \                                                            Forall na a
a' Forall nb b
b' Forall nc c
c' ->                                   Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x]
  -> Forall ny [y]
  -> Forall na a
  -> Forall nb b
  -> Forall nc c
  -> SBool)
 -> Proof)
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) (Forall SList y
ys' :: Forall ny [y]) Forall na a
a' Forall nb b
b' Forall nc c
c' -> (SList x
xs', SList y
ys') (SList x, SList y) -> (SList x, SList y) -> SBool
forall a b.
(SymVal a, SymVal b) =>
(SList a, SList b) -> (SList a, SList b) -> SBool
`lexLeq2` (SList x
xs, SList y
ys) SBool -> SBool -> SBool
.=> Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil SL.nil a b c .&& predicate SL.nil (y SL..: ys) a b c .&& predicate (x SL..: xs) SL.nil a b c
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a b c)
              }

-- | Induction over two lists, simultaneously, taking four extra arguments
instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
                   (SBV x -> SList x -> SBV y -> SList y -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, [ProofStep z]))
  where
   inductionStrategy :: Proposition
  (Forall nx [x]
   -> Forall ny [y]
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> SBool) =>
InductionStyle
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV y
    -> SList y
    -> SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result Proof
-> SBV x
-> SList x
-> SBV y
-> SList y
-> SBV a
-> SBV b
-> SBV c
-> SBV d
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x -> SList y -> SBV a -> SBV b -> SBV c -> SBV d -> SBool
predicate SList x
xs SList y
ys SBV a
a SBV b
b SBV c
c SBV d
d = Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c) (SBV d -> Forall nd d
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV d
d)
           nxs :: String
nxs                     = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx                      = String -> String
singular String
nxs
           nys :: String
nys                     = Proxy ny -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ny)
           ny :: String
ny                      = String -> String
singular String
nys
           na :: String
na                      = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                      = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nc :: String
nc                      = Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)
           nd :: String
nd                      = Proxy nd -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nd)

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs

       y  <- free ny
       ys <- free nys

       a  <- free na
       b  <- free nb
       c  <- free nc
       d  <- free nd

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String
-> (Forall na a
    -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a
  -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
 -> Proof)
-> (Forall na a
    -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \                                                            Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' ->                                   Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x]
  -> Forall ny [y]
  -> Forall na a
  -> Forall nb b
  -> Forall nc c
  -> Forall nd d
  -> SBool)
 -> Proof)
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) (Forall SList y
ys' :: Forall ny [y]) Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' -> (SList x
xs', SList y
ys') (SList x, SList y) -> (SList x, SList y) -> SBool
forall a b.
(SymVal a, SymVal b) =>
(SList a, SList b) -> (SList a, SList b) -> SBool
`lexLeq2` (SList x
xs, SList y
ys) SBool -> SBool -> SBool
.=> Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c d

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil SL.nil a b c d .&& predicate SL.nil (y SL..: ys) a b c d .&& predicate (x SL..: xs) SL.nil a b c d
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a b c d)
              }

-- | Induction over two lists, simultaneously, taking four extra arguments
instance (KnownSymbol nx, SymVal x, KnownSymbol ny, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z)
      => Inductive (Forall nx [x] -> Forall ny [y] -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool)
                   (SBV x -> SList x -> SBV y -> SList y -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, [ProofStep z]))
  where
   inductionStrategy :: Proposition
  (Forall nx [x]
   -> Forall ny [y]
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> Forall ne e
   -> SBool) =>
InductionStyle
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV y
    -> SList y
    -> SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> (SBool, [ProofStep z]))
-> Symbolic InductionStrategy
inductionStrategy InductionStyle
style Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result Proof
-> SBV x
-> SList x
-> SBV y
-> SList y
-> SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> (SBool, [ProofStep z])
steps = do
       let predicate :: SList x
-> SList y -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool
predicate SList x
xs SList y
ys SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e = Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs) (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c) (SBV d -> Forall nd d
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV d
d) (SBV e -> Forall ne e
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV e
e)
           nxs :: String
nxs                       = Proxy nx -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nx)
           nx :: String
nx                        = String -> String
singular String
nxs
           nys :: String
nys                       = Proxy ny -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ny)
           ny :: String
ny                        = String -> String
singular String
nys
           na :: String
na                        = Proxy na -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
           nb :: String
nb                        = Proxy nb -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nb)
           nc :: String
nc                        = Proxy nc -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nc)
           nd :: String
nd                        = Proxy nd -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nd)
           ne :: String
ne                        = Proxy ne -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @ne)

       x  <- String -> Symbolic (SBV x)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
       xs <- free nxs

       y  <- free ny
       ys <- free nys

       a  <- free na
       b  <- free nb
       c  <- free nc
       d  <- free nd
       e  <- free ne

       let ih = case InductionStyle
style of
                  InductionStyle
RegularInduction -> String
-> (Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall na a
  -> Forall nb b
  -> Forall nc c
  -> Forall nd d
  -> Forall ne e
  -> SBool)
 -> Proof)
-> (Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \                                                            Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' Forall ne e
e' ->                                   Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs)  (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys)  (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d) (Forall ne e
e' :: Forall ne e)
                  InductionStyle
StrongInduction  -> String
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
"IH" ((Forall nx [x]
  -> Forall ny [y]
  -> Forall na a
  -> Forall nb b
  -> Forall nc c
  -> Forall nd d
  -> Forall ne e
  -> SBool)
 -> Proof)
-> (Forall nx [x]
    -> Forall ny [y]
    -> Forall na a
    -> Forall nb b
    -> Forall nc c
    -> Forall nd d
    -> Forall ne e
    -> SBool)
-> Proof
forall a b. (a -> b) -> a -> b
$ \(Forall SList x
xs' :: Forall nx [x]) (Forall SList y
ys' :: Forall ny [y]) Forall na a
a' Forall nb b
b' Forall nc c
c' Forall nd d
d' Forall ne e
e' -> (SList x
xs', SList y
ys') (SList x, SList y) -> (SList x, SList y) -> SBool
forall a b.
(SymVal a, SymVal b) =>
(SList a, SList b) -> (SList a, SList b) -> SBool
`lexLeq2` (SList x
xs, SList y
ys) SBool -> SBool -> SBool
.=> Forall nx [x]
-> Forall ny [y]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SList x -> Forall nx [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs') (SList y -> Forall ny [y]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList y
ys') (Forall na a
a' :: Forall na a) (Forall nb b
b' :: Forall nb b) (Forall nc c
c' :: Forall nc c) (Forall nd d
d' :: Forall nd d) (Forall ne e
e' :: Forall ne e)
           CalcStrategy { calcIntros, calcProofSteps } = mkCalcSteps $ steps ih x xs y ys a b c d e

       pure InductionStrategy {
                inductionIntros         = calcIntros
              , inductionBaseCase       = predicate SL.nil SL.nil a b c d e .&& predicate SL.nil (y SL..: ys) a b c d e .&& predicate (x SL..: xs) SL.nil a b c d e
              , inductionProofSteps     = calcProofSteps
              , inductionBaseFailureMsg = "Property fails for " ++ nxs ++ " = [] OR " ++ nys ++ " = []"
              , inductiveStep           = observeIf not ("P(" ++ nx ++ ":" ++ nxs ++ ", " ++ ny ++ ":" ++ nys ++ ")") (predicate (x SL..: xs) (y SL..: ys) a b c d e)
              }

-- | Instantiation for a universally quantified variable
newtype Inst (nm :: Symbol) a = Inst (SBV a)

instance KnownSymbol nm => Show (Inst nm a) where
   show :: Inst nm a -> String
show (Inst SBV a
a) = Proxy nm -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nm) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" |-> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall a. Show a => a -> String
show SBV a
a

-- | Instantiating a proof at different types of arguments. This is necessarily done using
-- dynamics, hand has a cost of not being applicable.
class Instantiatable a where
  -- | Apply a universal proof to some arguments, creating an instance of the proof itself.
  at :: Proof -> a -> Proof

-- | Single parameter
instance (KnownSymbol na, HasKind a, Typeable a) => Instantiatable (Inst na a) where
  at :: Proof -> Inst na a -> Proof
at = ((Forall na a -> SBool) -> Inst na a -> SBool)
-> Proof -> Inst na a -> Proof
forall f arg.
(Typeable f, Show arg) =>
(f -> arg -> SBool) -> Proof -> arg -> Proof
instantiate (((Forall na a -> SBool) -> Inst na a -> SBool)
 -> Proof -> Inst na a -> Proof)
-> ((Forall na a -> SBool) -> Inst na a -> SBool)
-> Proof
-> Inst na a
-> Proof
forall a b. (a -> b) -> a -> b
$ \Forall na a -> SBool
f (Inst SBV a
a) -> Forall na a -> SBool
f (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a :: Forall na a)

-- | Two parameters
instance ( KnownSymbol na, HasKind a, Typeable a
         , KnownSymbol nb, HasKind b, Typeable b
         ) => Instantiatable (Inst na a, Inst nb b) where
  at :: Proof -> (Inst na a, Inst nb b) -> Proof
at = ((Forall na a -> Forall nb b -> SBool)
 -> (Inst na a, Inst nb b) -> SBool)
-> Proof -> (Inst na a, Inst nb b) -> Proof
forall f arg.
(Typeable f, Show arg) =>
(f -> arg -> SBool) -> Proof -> arg -> Proof
instantiate (((Forall na a -> Forall nb b -> SBool)
  -> (Inst na a, Inst nb b) -> SBool)
 -> Proof -> (Inst na a, Inst nb b) -> Proof)
-> ((Forall na a -> Forall nb b -> SBool)
    -> (Inst na a, Inst nb b) -> SBool)
-> Proof
-> (Inst na a, Inst nb b)
-> Proof
forall a b. (a -> b) -> a -> b
$ \Forall na a -> Forall nb b -> SBool
f (Inst SBV a
a, Inst SBV b
b) -> Forall na a -> Forall nb b -> SBool
f (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a :: Forall na a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b :: Forall nb b)

-- | Three parameters
instance ( KnownSymbol na, HasKind a, Typeable a
         , KnownSymbol nb, HasKind b, Typeable b
         , KnownSymbol nc, HasKind c, Typeable c
         ) => Instantiatable (Inst na a, Inst nb b, Inst nc c) where
  at :: Proof -> (Inst na a, Inst nb b, Inst nc c) -> Proof
at = ((Forall na a -> Forall nb b -> Forall nc c -> SBool)
 -> (Inst na a, Inst nb b, Inst nc c) -> SBool)
-> Proof -> (Inst na a, Inst nb b, Inst nc c) -> Proof
forall f arg.
(Typeable f, Show arg) =>
(f -> arg -> SBool) -> Proof -> arg -> Proof
instantiate (((Forall na a -> Forall nb b -> Forall nc c -> SBool)
  -> (Inst na a, Inst nb b, Inst nc c) -> SBool)
 -> Proof -> (Inst na a, Inst nb b, Inst nc c) -> Proof)
-> ((Forall na a -> Forall nb b -> Forall nc c -> SBool)
    -> (Inst na a, Inst nb b, Inst nc c) -> SBool)
-> Proof
-> (Inst na a, Inst nb b, Inst nc c)
-> Proof
forall a b. (a -> b) -> a -> b
$ \Forall na a -> Forall nb b -> Forall nc c -> SBool
f (Inst SBV a
a, Inst SBV b
b, Inst SBV c
c) -> Forall na a -> Forall nb b -> Forall nc c -> SBool
f (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a :: Forall na a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b :: Forall nb b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c :: Forall nc c)

-- | Four parameters
instance ( KnownSymbol na, HasKind a, Typeable a
         , KnownSymbol nb, HasKind b, Typeable b
         , KnownSymbol nc, HasKind c, Typeable c
         , KnownSymbol nd, HasKind d, Typeable d
         ) => Instantiatable (Inst na a, Inst nb b, Inst nc c, Inst nd d) where
  at :: Proof -> (Inst na a, Inst nb b, Inst nc c, Inst nd d) -> Proof
at = ((Forall na a
  -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
 -> (Inst na a, Inst nb b, Inst nc c, Inst nd d) -> SBool)
-> Proof -> (Inst na a, Inst nb b, Inst nc c, Inst nd d) -> Proof
forall f arg.
(Typeable f, Show arg) =>
(f -> arg -> SBool) -> Proof -> arg -> Proof
instantiate (((Forall na a
   -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
  -> (Inst na a, Inst nb b, Inst nc c, Inst nd d) -> SBool)
 -> Proof -> (Inst na a, Inst nb b, Inst nc c, Inst nd d) -> Proof)
-> ((Forall na a
     -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
    -> (Inst na a, Inst nb b, Inst nc c, Inst nd d) -> SBool)
-> Proof
-> (Inst na a, Inst nb b, Inst nc c, Inst nd d)
-> Proof
forall a b. (a -> b) -> a -> b
$ \Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool
f (Inst SBV a
a, Inst SBV b
b, Inst SBV c
c, Inst SBV d
d) -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool
f (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a :: Forall na a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b :: Forall nb b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c :: Forall nc c) (SBV d -> Forall nd d
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV d
d :: Forall nd d)

-- | Five parameters
instance ( KnownSymbol na, HasKind a, Typeable a
         , KnownSymbol nb, HasKind b, Typeable b
         , KnownSymbol nc, HasKind c, Typeable c
         , KnownSymbol nd, HasKind d, Typeable d
         , KnownSymbol ne, HasKind e, Typeable e
         ) => Instantiatable (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e) where
  at :: Proof
-> (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e) -> Proof
at = ((Forall na a
  -> Forall nb b
  -> Forall nc c
  -> Forall nd d
  -> Forall ne e
  -> SBool)
 -> (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e)
 -> SBool)
-> Proof
-> (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e)
-> Proof
forall f arg.
(Typeable f, Show arg) =>
(f -> arg -> SBool) -> Proof -> arg -> Proof
instantiate (((Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> Forall ne e
   -> SBool)
  -> (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e)
  -> SBool)
 -> Proof
 -> (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e)
 -> Proof)
-> ((Forall na a
     -> Forall nb b
     -> Forall nc c
     -> Forall nd d
     -> Forall ne e
     -> SBool)
    -> (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e)
    -> SBool)
-> Proof
-> (Inst na a, Inst nb b, Inst nc c, Inst nd d, Inst ne e)
-> Proof
forall a b. (a -> b) -> a -> b
$ \Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
f (Inst SBV a
a, Inst SBV b
b, Inst SBV c
c, Inst SBV d
d, Inst SBV e
e) -> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
f (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a :: Forall na a) (SBV b -> Forall nb b
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV b
b :: Forall nb b) (SBV c -> Forall nc c
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV c
c :: Forall nc c) (SBV d -> Forall nd d
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV d
d :: Forall nd d) (SBV e -> Forall ne e
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV e
e :: Forall ne e)

-- | Instantiate a proof over an arg. This uses dynamic typing, kind of hacky, but works sufficiently well.
instantiate :: (Typeable f, Show arg) => (f -> arg -> SBool) -> Proof -> arg -> Proof
instantiate :: forall f arg.
(Typeable f, Show arg) =>
(f -> arg -> SBool) -> Proof -> arg -> Proof
instantiate f -> arg -> SBool
ap p :: Proof
p@Proof{Dynamic
getProp :: Proof -> Dynamic
getProp :: Dynamic
getProp, String
proofName :: Proof -> String
proofName :: String
proofName} arg
a = case Dynamic -> Maybe f
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
getProp of
                                                 Maybe f
Nothing -> Proof
cantInstantiate
                                                 Just f
f  -> let result :: SBool
result = f
f f -> arg -> SBool
`ap` arg
a
                                                                nm :: String
nm     = String
proofName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" @ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
paren String
sha
                                                            in Proof
p { getProof  = label nm result
                                                                 , getProp   = toDyn result
                                                                 , proofName = nm
                                                                 }
 where sha :: String
sha = arg -> String
forall a. Show a => a -> String
show arg
a
       cantInstantiate :: Proof
cantInstantiate = String -> Proof
forall a. HasCallStack => String -> a
error (String -> Proof) -> String -> Proof
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"at: Cannot instantiate proof:"
                                         , String
"   Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proofName
                                         , String
"   Type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
trim (Dynamic -> String
forall a. Show a => a -> String
show Dynamic
getProp)
                                         , String
"   At  : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sha
                                         ]

       -- dynamic puts funky <</>> at the beginning and end; trim it:
       trim :: String -> String
trim  (Char
'<':Char
'<':String
s) = String -> String
forall a. [a] -> [a]
reverse (String -> String
trimE (String -> String
forall a. [a] -> [a]
reverse String
s))
       trim  String
s           = String
s
       trimE :: String -> String
trimE (Char
'>':Char
'>':String
s) = String
s
       trimE String
s           = String
s

       -- Add parens if necessary
       paren :: String -> String
paren String
s | String
"(" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
s Bool -> Bool -> Bool
&& String
")" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` String
s = String
s
               | Bool -> Bool
not ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
s)                      = String
s
               | Bool
True                                     = Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Helpers for a step
data Helper = HelperProof Proof          -- A previously proven theorem
            | HelperAssum SBool          -- A hypothesis
            | HelperCase  String [SBool] -- Case split

-- | Get proofs from helpers
getHelperProofs :: [Helper] -> [Proof]
getHelperProofs :: [Helper] -> [Proof]
getHelperProofs = (Helper -> [Proof]) -> [Helper] -> [Proof]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [Proof]
get
  where get :: Helper -> [Proof]
get (HelperProof Proof
p) = [Proof
p]
        get HelperAssum {}  = []
        get HelperCase  {}  = []

-- | Get proofs from helpers
getHelperAssumes :: [Helper] -> [SBool]
getHelperAssumes :: [Helper] -> [SBool]
getHelperAssumes = (Helper -> [SBool]) -> [Helper] -> [SBool]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [SBool]
get
  where get :: Helper -> [SBool]
get HelperProof  {} = []
        get (HelperAssum SBool
b) = [SBool
b]
        get HelperCase   {} = []

-- | Smart constructor for creating a helper from a boolean. This is hardly needed, unless you're
-- mixing proofs and booleans in one group of hints.
hyp :: SBool -> Helper
hyp :: SBool -> Helper
hyp = SBool -> Helper
HelperAssum

-- | Smart constructor for creating a helper from a boolean. This is hardly needed, unless you're
-- mixing proofs and booleans in one group of hints.
hprf :: Proof -> Helper
hprf :: Proof -> Helper
hprf = Proof -> Helper
HelperProof

-- | A proof-step with associated helpers
data ProofStep a = SingleStep a [Helper]

-- | Class capturing giving a proof-step helper
class ProofHint a b where
  -- | Specify a helper for the given proof step
  (??) :: a -> b -> ProofStep a
  infixl 2 ??

-- | Giving just one proof as a helper.
instance ProofHint a Proof where
  a
a ?? :: a -> Proof -> ProofStep a
?? Proof
p = a -> [Helper] -> ProofStep a
forall a. a -> [Helper] -> ProofStep a
SingleStep a
a [Proof -> Helper
HelperProof Proof
p]

-- | Giving just one boolean as a helper.
instance ProofHint a SBool where
  a
a ?? :: a -> SBool -> ProofStep a
?? SBool
p = a -> [Helper] -> ProofStep a
forall a. a -> [Helper] -> ProofStep a
SingleStep a
a [SBool -> Helper
HelperAssum SBool
p]

-- | Giving just one helper
instance ProofHint a Helper where
  a
a ?? :: a -> Helper -> ProofStep a
?? Helper
h = a -> [Helper] -> ProofStep a
forall a. a -> [Helper] -> ProofStep a
SingleStep a
a [Helper
h]

-- | Giving a bunch of proofs as a helper.
instance ProofHint a [Proof] where
  a
a ?? :: a -> [Proof] -> ProofStep a
?? [Proof]
ps = a -> [Helper] -> ProofStep a
forall a. a -> [Helper] -> ProofStep a
SingleStep a
a ((Proof -> Helper) -> [Proof] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map Proof -> Helper
HelperProof [Proof]
ps)

-- | Giving a bunch of booleans as a helper.
instance ProofHint a [SBool] where
  a
a ?? :: a -> [SBool] -> ProofStep a
?? [SBool]
ps = a -> [Helper] -> ProofStep a
forall a. a -> [Helper] -> ProofStep a
SingleStep a
a ((SBool -> Helper) -> [SBool] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> Helper
HelperAssum [SBool]
ps)

-- | Giving a set of helpers
instance ProofHint a [Helper] where
  a
a ?? :: a -> [Helper] -> ProofStep a
?? [Helper]
hs = a -> [Helper] -> ProofStep a
forall a. a -> [Helper] -> ProofStep a
SingleStep a
a [Helper]
hs

-- | Giving user a hint as a string. This doesn't actually do anything for the solver, it just helps with readability
instance ProofHint a String where
  a
a ?? :: a -> String -> ProofStep a
?? String
_ = a -> [Helper] -> ProofStep a
forall a. a -> [Helper] -> ProofStep a
SingleStep a
a []

-- | Capture what a given step can chain-to. This is a closed-type family, i.e.,
-- we don't allow users to change this and write other chainable things. Probably it is not really necessary,
-- but we'll cross that bridge if someone actually asks for it.
type family ChainsTo a where
  ChainsTo (ProofStep a) = [ProofStep a]
  ChainsTo a             = [ProofStep a]

-- | Chain steps in a calculational proof.
(=:) :: ChainStep a (ChainsTo a) =>  a -> ChainsTo a -> ChainsTo a
=: :: forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
(=:) = a -> ChainsTo a -> ChainsTo a
forall a b. ChainStep a b => a -> b -> b
chain
infixr 1 =:

-- | Unicode alternative for `=:`.
(≡) :: ChainStep a (ChainsTo a) =>  a -> ChainsTo a -> ChainsTo a
≡ :: forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
(≡) = a -> ChainsTo a -> ChainsTo a
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
(=:)
infixr 1 ≡

-- | Chaining two steps together
class ChainStep a b where
  chain :: a -> b -> b

-- | Chaining from a value without any annotation
instance ChainStep a [ProofStep a] where
  chain :: a -> [ProofStep a] -> [ProofStep a]
chain a
x [ProofStep a]
y = a -> [Helper] -> ProofStep a
forall a. a -> [Helper] -> ProofStep a
SingleStep a
x [] ProofStep a -> [ProofStep a] -> [ProofStep a]
forall a. a -> [a] -> [a]
: [ProofStep a]
y

-- | Chaining from another proof step
instance ChainStep (ProofStep a) [ProofStep a] where
  chain :: ProofStep a -> [ProofStep a] -> [ProofStep a]
chain ProofStep a
x [ProofStep a]
y = ProofStep a
x ProofStep a -> [ProofStep a] -> [ProofStep a]
forall a. a -> [a] -> [a]
: [ProofStep a]
y

-- | Mark the end of a calculational proof.
qed :: [ProofStep a]
qed :: forall a. [ProofStep a]
qed = []

-- | Start a calculational proof, with the given hypothesis. Use @[]@ as the
-- first argument if the calculation holds unconditionally. The first argument is
-- typically used to introduce hypotheses in proofs of implications such as @A .=> B .=> C@, where
-- we would put @[A, B]@ as the starting assumption. You can name these and later use in the derivation steps.
(|-) :: [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
[SBool]
bs |- :: forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
|- [ProofStep a]
ps = ([SBool] -> SBool
sAnd [SBool]
bs, [ProofStep a]
ps)
infixl 0 |-

-- | Alternative unicode for `|-`.
(⊢) :: [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ :: forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
(⊢) = [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
(|-)
infixl 0 ⊢

-- | Alternative unicode for `??`.
(⁇) :: ProofHint a b => a -> b -> ProofStep a
⁇ :: forall a b. ProofHint a b => a -> b -> ProofStep a
(⁇) = a -> b -> ProofStep a
forall a b. ProofHint a b => a -> b -> ProofStep a
(??)
infixl 2 ⁇

-- | Specifying a case-split
cases :: String -> [SBool] -> Helper
cases :: String -> [SBool] -> Helper
cases = String -> [SBool] -> Helper
HelperCase