-----------------------------------------------------------------------------
-- |
-- 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          #-}
{-# LANGUAGE TypeOperators         #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.KD.KnuckleDragger (
         Proposition, Proof, Instantiatable(..), Inst(..), getProofTree, kdShowDepsHTML, KDProofDeps(..)
       , axiom
       , lemma,   lemmaWith
       , theorem, theoremWith
       ,    calc,    calcWith,    calcThm,    calcThmWith
       ,  induct,  inductWith,  inductThm,  inductThmWith
       , sInduct, sInductWith, sInductThm, sInductThmWith
       , sorry
       , KD, runKD, runKDWith, use
       , (|-), (⊢), (=:), (≡), (??), (⁇), split, split2, cases, (==>), (⟹), hasm, hprf, hcmnt, qed, trivial, contradiction
       ) where

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

import Data.SBV.Control hiding (getProof)

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

import qualified Data.SBV.List as SL

import Control.Monad (when)
import Control.Monad.Trans (liftIO)

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

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

import Data.SBV.Utils.TDiff

import Data.Dynamic

-- | 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 -> KDProof
calcProofTree :: KDProof
                                 }

-- | Saturatable things in steps
proofTreeSaturatables :: KDProof -> [SBool]
proofTreeSaturatables :: KDProof -> [SBool]
proofTreeSaturatables = KDProof -> [SBool]
go
  where go :: KDProof -> [SBool]
go (ProofEnd    SBool
b           [Helper]
hs                ) = SBool
b SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: (Helper -> [SBool]) -> [Helper] -> [SBool]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [SBool]
getH [Helper]
hs
        go (ProofStep   SBool
a           [Helper]
hs               KDProof
r) = SBool
a SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: (Helper -> [SBool]) -> [Helper] -> [SBool]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [SBool]
getH [Helper]
hs [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ KDProof -> [SBool]
go KDProof
r
        go (ProofBranch (Bool
_ :: Bool) ([String]
_ :: [String]) [(SBool, KDProof)]
ps) = [[SBool]] -> [SBool]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [SBool
b SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: KDProof -> [SBool]
go KDProof
p | (SBool
b, KDProof
p) <- [(SBool, KDProof)]
ps]

        getH :: Helper -> [SBool]
getH (HelperProof  Proof
p) = [Proof -> SBool
getProof Proof
p]
        getH (HelperAssum  SBool
b) = [SBool
b]
        getH HelperString{}   = []

-- | Things that are inside calc-strategy that we have to saturate
getCalcStrategySaturatables :: CalcStrategy -> [SBool]
getCalcStrategySaturatables :: CalcStrategy -> [SBool]
getCalcStrategySaturatables (CalcStrategy SBool
calcIntros KDProof
calcProofTree) = SBool
calcIntros SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: KDProof -> [SBool]
proofTreeSaturatables KDProof
calcProofTree

-- | 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 SMTConfig
cfg 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"

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

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

        query $ proveProofTree cfg kdSt nm (result, calcGoal) calcIntros calcProofTree

-- | Prove the proof tree. The arguments are:
--
--      result           : The ultimate goal we want to prove. Note that this is a general proposition, and we don't actually prove it. See the next param.
--      resultBool       : The instance of result that, if we prove it, establishes the result itself
--      initialHypotheses: Hypotheses (conjuncted)
--      calcProofTree    : A tree of steps, which give rise to a bunch of equalities
--
-- Note that we do not check the resultBool is the result itself just "instantiated" appropriately. This is the contract with the caller who
-- has to establish that by whatever means it chooses to do so.
--
-- The final proof we have has the following form:
--
--     - For each "link" in the proofTree, prove that intros .=> link
--     - The above will give us a bunch of results, for each leaf node in the tree.
--     - Then prove: (intros .=> sAnd results) .=> resultBool
--     - Then conclude result, based on what assumption that proving resultBool establishes result
proveProofTree :: Proposition a
               => SMTConfig
               -> KDState
               -> String        -- ^ the name of the top result
               -> (a, SBool)    -- ^ goal: as a proposition and as a boolean
               -> SBool         -- ^ hypotheses
               -> KDProof       -- ^ proof tree
               -> Query Proof
proveProofTree :: forall a.
Proposition a =>
SMTConfig
-> KDState
-> String
-> (a, SBool)
-> SBool
-> KDProof
-> Query Proof
proveProofTree SMTConfig
cfg KDState
kdSt String
nm (a
result, SBool
resultBool) SBool
initialHypotheses KDProof
calcProofTree = do

  let SMTConfig{kdOptions :: SMTConfig -> KDOptions
kdOptions = KDOptions{Bool
measureTime :: Bool
measureTime :: KDOptions -> Bool
measureTime}} = SMTConfig
cfg
  mbStartTime <- Bool -> QueryT IO (Maybe UTCTime)
forall (m :: * -> *). MonadIO m => Bool -> m (Maybe UTCTime)
getTimeStampIf Bool
measureTime

  let next :: [Int] -> [Int]
      next [Int]
bs = case [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
bs of
                  Int
i : [Int]
rs -> [Int] -> [Int]
forall a. [a] -> [a]
reverse ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
rs
                  []     -> [Int
1]

      isEnd ProofEnd{}    = Bool
True
      isEnd ProofStep{}   = Bool
False
      isEnd ProofBranch{} = Bool
False

      -- trim the branch-name, if we're in a deeper level, and we're at the end
      trimBN a
level [a]
bn | a
level a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
1, a
1 : [a]
_ <- [a] -> [a]
forall a. [a] -> [a]
reverse [a]
bn = [a] -> [a]
forall a. HasCallStack => [a] -> [a]
init [a]
bn
                      | Bool
True                           = [a]
bn

      -- If the next step is ending and we're the 1st step; our number can be skipped
      mkStepName a
level [a]
bn KDProofGen a bh b
nextStep | KDProofGen a bh b -> Bool
forall {a} {bh} {b}. KDProofGen a bh b -> Bool
isEnd KDProofGen a bh b
nextStep = (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show (a -> [a] -> [a]
forall {a} {a}. (Ord a, Num a, Num a, Eq a) => a -> [a] -> [a]
trimBN a
level [a]
bn)
                                   | Bool
True           = (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
bn

      walk :: SBool -> Int -> ([Int], KDProof) -> Query [SBool]

      -- End of proof, return what it established. If there's a hint associated here, it was probably by mistake; so tell it to the user.
      walk SBool
intros Int
level ([Int]
bn, ProofEnd SBool
calcResult [Helper]
hs)
         | Bool -> Bool
not ([Helper] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Helper]
hs)
         = String -> Query [SBool]
forall a. HasCallStack => String -> a
error (String -> Query [SBool]) -> String -> Query [SBool]
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?"
                           ]
         | Bool
True
         =  do -- If we're not at the top-level and this is the only step, print it.
               -- Otherwise the noise isn't necessary.
               Bool -> QueryT IO () -> QueryT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
level Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ case [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
bn of
                                    Int
1 : [Int]
_ -> IO () -> QueryT IO ()
forall a. IO a -> QueryT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ do tab <- SMTConfig -> Bool -> String -> Int -> KDProofContext -> IO Int
startKD SMTConfig
cfg Bool
False String
"Step" Int
level (Bool -> String -> [String] -> [String] -> KDProofContext
KDProofStep Bool
False String
nm [] ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show ([Int] -> [Int]
forall a. HasCallStack => [a] -> [a]
init [Int]
bn)))
                                                         finishKD cfg "Q.E.D." (tab, Nothing) []
                                    [Int]
_     -> () -> QueryT IO ()
forall a. a -> QueryT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

               [SBool] -> Query [SBool]
forall a. a -> QueryT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SBool
intros SBool -> SBool -> SBool
.=> SBool
calcResult]

      -- Do the branches separately and collect the results. If there's coverage needed, we do it too; which
      -- is essentially the assumption here.
      walk SBool
intros Int
level ([Int]
bnTop, ProofBranch Bool
checkCompleteness [String]
hintStrings [(SBool, KDProof)]
ps) = do

        let bn :: [Int]
bn = Int -> [Int] -> [Int]
forall {a} {a}. (Ord a, Num a, Num a, Eq a) => a -> [a] -> [a]
trimBN Int
level [Int]
bnTop

            addSuffix :: [[a]] -> [a] -> [[a]]
addSuffix [[a]]
xs [a]
s = case [[a]] -> [[a]]
forall a. [a] -> [a]
reverse [[a]]
xs of
                                [a]
l : [[a]]
p -> [[a]] -> [[a]]
forall a. [a] -> [a]
reverse ([[a]] -> [[a]]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> a -> b
$ ([a]
l [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
s) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [[a]]
p
                                []    -> [[a]
s]

            full :: String
full | Bool
checkCompleteness = String
""
                 | Bool
True              = String
"full "

            stepName :: [String]
stepName = (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [Int]
bn

        _ <- IO Int -> Query Int
forall a. IO a -> QueryT IO a
io (IO Int -> Query Int) -> IO Int -> Query Int
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Bool -> String -> Int -> KDProofContext -> IO Int
startKD SMTConfig
cfg Bool
True String
"Step" Int
level (Bool -> String -> [String] -> [String] -> KDProofContext
KDProofStep Bool
False String
nm [String]
hintStrings ([String] -> String -> [String]
forall {a}. [[a]] -> [a] -> [[a]]
addSuffix [String]
stepName (String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([(SBool, KDProof)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SBool, KDProof)]
ps) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" way " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
full String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"case split)")))

        results <- concat <$> sequence [walk (intros .&& branchCond) (level + 1) (bn ++ [i, 1], p) | (i, (branchCond, p)) <- zip [1..] ps]

        when checkCompleteness $ smtProofStep cfg kdSt "Step" (level+1)
                                                       (KDProofStep False nm [] (stepName ++ ["Completeness"]))
                                                       (Just intros)
                                                       (sOr (map fst ps))
                                                       (\(Int, Maybe NominalDiffTime)
d -> SMTConfig
-> String
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishKD SMTConfig
cfg String
"Q.E.D." (Int, Maybe NominalDiffTime)
d [])
        pure results

      -- Do a proof step
      walk SBool
intros Int
level ([Int]
bn, ProofStep SBool
cur [Helper]
hs KDProof
p) = do

           let finish :: [NominalDiffTime]
-> [Proof] -> (Int, Maybe NominalDiffTime) -> IO ()
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

               stepName :: [String]
stepName = Int -> [Int] -> KDProof -> [String]
forall {a} {a} {a} {bh} {b}.
(Show a, Ord a, Num a, Num a, Eq a) =>
a -> [a] -> KDProofGen a bh b -> [String]
mkStepName Int
level [Int]
bn KDProof
p

           -- First prove the assumptions, if there are any. We stay quiet, unless timing is asked for
           let (SMTConfig
quietCfg, (Int, Maybe NominalDiffTime) -> IO ()
finalizer)
                 | Bool
measureTime = (SMTConfig
cfg,                                              [NominalDiffTime]
-> [Proof] -> (Int, Maybe NominalDiffTime) -> IO ()
finish [] [])
                 | Bool
True        = (SMTConfig
cfg{kdOptions = (kdOptions cfg) { quiet = True}}, IO () -> (Int, Maybe NominalDiffTime) -> IO ()
forall a b. a -> b -> a
const (() -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()))

               as :: [SBool]
as = (Helper -> [SBool]) -> [Helper] -> [SBool]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [SBool]
getHelperAssumes [Helper]
hs
               ss :: [String]
ss = [Helper] -> [String]
getHelperText [Helper]
hs
           case [SBool]
as of
             [] -> () -> QueryT IO ()
forall a. a -> QueryT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
             [SBool]
_  -> SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe SBool
-> SBool
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> QueryT IO ()
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe SBool
-> a
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep SMTConfig
quietCfg KDState
kdSt String
"Asms" Int
level
                                         (Bool -> String -> [String] -> [String] -> KDProofContext
KDProofStep Bool
True String
nm [] [String]
stepName)
                                         (SBool -> Maybe SBool
forall a. a -> Maybe a
Just SBool
intros)
                                         ([SBool] -> SBool
sAnd [SBool]
as)
                                         (Int, Maybe NominalDiffTime) -> IO ()
finalizer

           -- Now prove the step
           let by :: [Proof]
by = (Helper -> [Proof]) -> [Helper] -> [Proof]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [Proof]
getHelperProofs [Helper]
hs
           SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe SBool
-> SBool
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> QueryT IO ()
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe SBool
-> a
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep SMTConfig
cfg KDState
kdSt String
"Step" Int
level
                                 (Bool -> String -> [String] -> [String] -> KDProofContext
KDProofStep Bool
False String
nm [String]
ss [String]
stepName)
                                 (SBool -> Maybe SBool
forall a. a -> Maybe a
Just ([SBool] -> SBool
sAnd (SBool
intros SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [SBool]
as [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ (Proof -> SBool) -> [Proof] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map Proof -> SBool
getProof [Proof]
by)))
                                 SBool
cur
                                 ([NominalDiffTime]
-> [Proof] -> (Int, Maybe NominalDiffTime) -> IO ()
finish [] [Proof]
by)

           -- Move to next
           SBool -> Int -> ([Int], KDProof) -> Query [SBool]
walk SBool
intros Int
level ([Int] -> [Int]
next [Int]
bn, KDProof
p)

  results <- walk initialHypotheses 1 ([1], calcProofTree)

  queryDebug [nm ++ ": Proof end: proving the result:"]

  smtProofStep cfg kdSt "Result" 1
               (KDProofStep False nm [] [""])
               (Just (initialHypotheses .=> sAnd results))
               resultBool $ \(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 (concatMap getHelperProofs (getAllHelpers calcProofTree))
                    finishKD cfg ("Q.E.D." ++ modulo) d (catMaybes [mbElapsed])

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

-- Helper data-type for calc-step below
data CalcContext a = CalcStart     [Helper] -- Haven't started yet
                   | CalcStep  a a [Helper] -- Intermediate step: first value, prev value

-- | Turn a sequence of steps into a chain of equalities
mkCalcSteps :: EqSymbolic a => (SBool, KDProofRaw a) -> CalcStrategy
mkCalcSteps :: forall a. EqSymbolic a => (SBool, KDProofRaw a) -> CalcStrategy
mkCalcSteps (SBool
intros, KDProofRaw a
kdp) = CalcStrategy { calcIntros :: SBool
calcIntros    = SBool
intros
                                         , calcProofTree :: KDProof
calcProofTree = CalcContext a -> KDProofRaw a -> KDProof
forall a. EqSymbolic a => CalcContext a -> KDProofRaw a -> KDProof
go ([Helper] -> CalcContext a
forall a. [Helper] -> CalcContext a
CalcStart []) KDProofRaw a
kdp
                                         }
  where go :: EqSymbolic a => CalcContext a -> KDProofRaw a -> KDProof

        -- End of the proof; tie the begin and end
        go :: forall a. EqSymbolic a => CalcContext a -> KDProofRaw a -> KDProof
go CalcContext a
step (ProofEnd () [Helper]
hs) = case CalcContext a
step of
                                     -- It's tempting to error out if we're at the start and already reached the end
                                     -- This means we're given a sequence of no-steps. While this is useless in the
                                     -- general case, it's quite valid in a case-split; where one of the case-splits
                                     -- might be easy enough for the solver to deduce so the user simply says "just derive it for me."
                                     CalcStart [Helper]
hs'          -> SBool -> [Helper] -> KDProof
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd SBool
sTrue           ([Helper]
hs' [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs) -- Nothing proven!
                                     CalcStep a
begin a
end [Helper]
hs' -> SBool -> [Helper] -> KDProof
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd (a
begin a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
end) ([Helper]
hs' [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs)

        -- Branch: Just push it down. We use the hints from previous step, and pass the current ones down.
        go CalcContext a
step (ProofBranch Bool
c [Helper]
hs [(SBool, KDProofGen a [Helper] ())]
ps) = Bool -> [String] -> [(SBool, KDProof)] -> KDProof
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
c ([Helper] -> [String]
getHelperText [Helper]
hs) [(SBool
branchCond, CalcContext a -> KDProofGen a [Helper] () -> KDProof
forall a. EqSymbolic a => CalcContext a -> KDProofRaw a -> KDProof
go CalcContext a
step' KDProofGen a [Helper] ()
p) | (SBool
branchCond, KDProofGen a [Helper] ()
p) <- [(SBool, KDProofGen a [Helper] ())]
ps]
           where step' :: CalcContext a
step' = case CalcContext a
step of
                           CalcStart [Helper]
hs'     -> [Helper] -> CalcContext a
forall a. [Helper] -> CalcContext a
CalcStart ([Helper]
hs' [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs)
                           CalcStep  a
a a
b [Helper]
hs' -> a -> a -> [Helper] -> CalcContext a
forall a. a -> a -> [Helper] -> CalcContext a
CalcStep a
a a
b ([Helper]
hs' [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs)

        -- Step:
        go (CalcStart [Helper]
hs)           (ProofStep a
cur [Helper]
hs' KDProofGen a [Helper] ()
p) =                               CalcContext a -> KDProofGen a [Helper] () -> KDProof
forall a. EqSymbolic a => CalcContext a -> KDProofRaw a -> KDProof
go (a -> a -> [Helper] -> CalcContext a
forall a. a -> a -> [Helper] -> CalcContext a
CalcStep a
cur   a
cur ([Helper]
hs' [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs)) KDProofGen a [Helper] ()
p
        go (CalcStep a
first a
prev [Helper]
hs) (ProofStep a
cur [Helper]
hs' KDProofGen a [Helper] ()
p) = SBool -> [Helper] -> KDProof -> KDProof
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep (a
prev  a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
cur) [Helper]
hs (CalcContext a -> KDProofGen a [Helper] () -> KDProof
forall a. EqSymbolic a => CalcContext a -> KDProofRaw a -> KDProof
go (a -> a -> [Helper] -> CalcContext a
forall a. a -> a -> [Helper] -> CalcContext a
CalcStep a
first a
cur [Helper]
hs')         KDProofGen a [Helper] ()
p)

-- | Chaining lemmas that depend on no extra variables
instance EqSymbolic z => CalcLemma SBool (SBool, KDProofRaw z) where
   calcSteps :: SBool -> (SBool, KDProofRaw z) -> Symbolic (SBool, CalcStrategy)
calcSteps SBool
result (SBool, KDProofRaw 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, KDProofRaw z) -> CalcStrategy
forall a. EqSymbolic a => (SBool, KDProofRaw a) -> CalcStrategy
mkCalcSteps (SBool, KDProofRaw z)
steps)

-- | Chaining lemmas that depend on a single extra variable.
instance (KnownSymbol na, SymVal a, EqSymbolic z) => CalcLemma (Forall na a -> SBool) (SBV a -> (SBool, KDProofRaw z)) where
   calcSteps :: (Forall na a -> SBool)
-> (SBV a -> (SBool, KDProofRaw z))
-> Symbolic (SBool, CalcStrategy)
calcSteps Forall na a -> SBool
result SBV a -> (SBool, KDProofRaw 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 extra 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, KDProofRaw z)) where
   calcSteps :: (Forall na a -> Forall nb b -> SBool)
-> (SBV a -> SBV b -> (SBool, KDProofRaw z))
-> Symbolic (SBool, CalcStrategy)
calcSteps Forall na a -> Forall nb b -> SBool
result SBV a -> SBV b -> (SBool, KDProofRaw 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 extra 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, KDProofRaw z)) where
   calcSteps :: (Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> (SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z))
-> Symbolic (SBool, CalcStrategy)
calcSteps Forall na a -> Forall nb b -> Forall nc c -> SBool
result SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw 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 extra 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, KDProofRaw 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, KDProofRaw 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, KDProofRaw 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 extra 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, KDProofRaw 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, KDProofRaw 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, KDProofRaw 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. Base case might be nothing, to cover strong induction.
data InductionStrategy = InductionStrategy { InductionStrategy -> SBool
inductionIntros    :: SBool
                                           , InductionStrategy -> Maybe SBool
inductionMeasure   :: Maybe SBool
                                           , InductionStrategy -> Maybe SBool
inductionBaseCase  :: Maybe SBool
                                           , InductionStrategy -> KDProof
inductionProofTree :: KDProof
                                           , InductionStrategy -> SBool
inductiveStep      :: SBool
                                           }

-- | Are we doing regular induction or measure based general induction?
data InductionStyle = RegularInduction | GeneralInduction

getInductionStrategySaturatables :: InductionStrategy -> [SBool]
getInductionStrategySaturatables :: InductionStrategy -> [SBool]
getInductionStrategySaturatables (InductionStrategy SBool
inductionIntros
                                                    Maybe SBool
inductionMeasure
                                                    Maybe SBool
inductionBaseCase
                                                    KDProof
inductionProofSteps
                                                    SBool
inductiveStep)
  = SBool
inductionIntros SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: SBool
inductiveStep SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: KDProof -> [SBool]
proofTreeSaturatables KDProof
inductionProofSteps [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ Maybe SBool -> [SBool]
forall a. Maybe a -> [a]
maybeToList Maybe SBool
inductionBaseCase [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ Maybe SBool -> [SBool]
forall a. Maybe a -> [a]
maybeToList Maybe SBool
inductionMeasure

-- | A class for doing regular inductive proofs.
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 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

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

   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
-> Symbolic InductionStrategy
-> KD Proof
forall a.
Proposition a =>
InductionStyle
-> Bool
-> SMTConfig
-> String
-> a
-> Symbolic InductionStrategy
-> KD Proof
inductionEngine InductionStyle
RegularInduction Bool
False (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p (a -> (Proof -> steps) -> Symbolic InductionStrategy
forall a steps.
(Inductive a steps, Proposition a) =>
a -> (Proof -> steps) -> Symbolic InductionStrategy
inductionStrategy 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
-> Symbolic InductionStrategy
-> KD Proof
forall a.
Proposition a =>
InductionStyle
-> Bool
-> SMTConfig
-> String
-> a
-> Symbolic InductionStrategy
-> KD Proof
inductionEngine InductionStyle
RegularInduction Bool
True  (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p (a -> (Proof -> steps) -> Symbolic InductionStrategy
forall a steps.
(Inductive a steps, Proposition a) =>
a -> (Proof -> steps) -> Symbolic InductionStrategy
inductionStrategy a
p Proof -> steps
steps)

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

-- | A class of measures, used for inductive arguments.
class OrdSymbolic a => Measure a where
  zero :: a

-- | An integer as a measure
instance Measure SInteger where
   zero :: SInteger
zero = SInteger
0

-- | A tuple of integers as a measure
instance Measure (SInteger, SInteger) where
  zero :: (SInteger, SInteger)
zero = (SInteger
0, SInteger
0)

-- | A triple of integers as a measure
instance Measure (SInteger, SInteger, SInteger) where
  zero :: (SInteger, SInteger, SInteger)
zero = (SInteger
0, SInteger
0, SInteger
0)

-- | A quadruple of integers as a measure
instance Measure (SInteger, SInteger, SInteger, SInteger) where
  zero :: (SInteger, SInteger, SInteger, SInteger)
zero = (SInteger
0, SInteger
0, SInteger
0, SInteger
0)

instance Measure (SInteger, SInteger, SInteger, SInteger, SInteger) where
  zero :: (SInteger, SInteger, SInteger, SInteger, SInteger)
zero = (SInteger
0, SInteger
0, SInteger
0, SInteger
0, SInteger
0)

-- | A class for doing generalized measure based strong inductive proofs.
class SInductive a measure steps where
   -- | Inductively prove a lemma, using measure based 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 -> measure -> (Proof -> steps) -> KD Proof

   -- | Inductively prove a theorem, using measure based 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 -> measure -> (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 -> measure -> (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 -> measure -> (Proof -> steps) -> KD Proof

   sInduct            String
nm a
p measure
m 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 -> measure -> (Proof -> steps) -> KD Proof
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
SMTConfig -> String -> a -> measure -> (Proof -> steps) -> KD Proof
sInductWith                            SMTConfig
cfg                   String
nm a
p measure
m Proof -> steps
steps
   sInductThm         String
nm a
p measure
m 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 -> measure -> (Proof -> steps) -> KD Proof
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
SMTConfig -> String -> a -> measure -> (Proof -> steps) -> KD Proof
sInductThmWith                         SMTConfig
cfg                   String
nm a
p measure
m Proof -> steps
steps
   sInductWith    SMTConfig
cfg String
nm a
p measure
m 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
-> Symbolic InductionStrategy
-> KD Proof
forall a.
Proposition a =>
InductionStyle
-> Bool
-> SMTConfig
-> String
-> a
-> Symbolic InductionStrategy
-> KD Proof
inductionEngine InductionStyle
GeneralInduction Bool
False (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p (a -> measure -> (Proof -> steps) -> Symbolic InductionStrategy
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
a -> measure -> (Proof -> steps) -> Symbolic InductionStrategy
sInductionStrategy a
p measure
m Proof -> steps
steps)
   sInductThmWith SMTConfig
cfg String
nm a
p measure
m 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
-> Symbolic InductionStrategy
-> KD Proof
forall a.
Proposition a =>
InductionStyle
-> Bool
-> SMTConfig
-> String
-> a
-> Symbolic InductionStrategy
-> KD Proof
inductionEngine InductionStyle
GeneralInduction Bool
True  (SMTConfig -> SMTConfig -> SMTConfig
kdMergeCfg SMTConfig
cfg SMTConfig
cfg') String
nm a
p (a -> measure -> (Proof -> steps) -> Symbolic InductionStrategy
forall a measure steps.
(SInductive a measure steps, Proposition a) =>
a -> measure -> (Proof -> steps) -> Symbolic InductionStrategy
sInductionStrategy a
p measure
m Proof -> steps
steps)

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

-- | Do an inductive proof, based on the given strategy
inductionEngine :: Proposition a => InductionStyle -> Bool -> SMTConfig -> String -> a -> Symbolic InductionStrategy -> KD Proof
inductionEngine :: forall a.
Proposition a =>
InductionStyle
-> Bool
-> SMTConfig
-> String
-> a
-> Symbolic InductionStrategy
-> KD Proof
inductionEngine InductionStyle
style Bool
tagTheorem SMTConfig
cfg String
nm a
result Symbolic InductionStrategy
getStrategy = 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 qual = case InductionStyle
style of
                   InductionStyle
RegularInduction -> String
""
                   InductionStyle
GeneralInduction  -> String
" (strong)"

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

      strategy@InductionStrategy { inductionIntros
                                 , inductionMeasure
                                 , inductionBaseCase
                                 , inductionProofTree
                                 , inductiveStep
                                 } <- getStrategy

      mapM_ qSaturateSavingObservables $ getInductionStrategySaturatables strategy

      query $ do

       case inductionMeasure of
          Maybe SBool
Nothing -> [String] -> QueryT IO ()
queryDebug [String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Induction" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
qual String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", there is no custom measure to show non-negativeness."]
          Just SBool
ms -> do [String] -> QueryT IO ()
queryDebug [String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Induction, proving measure is always non-negative:"]
                        SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe SBool
-> SBool
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> QueryT IO ()
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe SBool
-> a
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep SMTConfig
cfg KDState
kdSt String
"Step" Int
1
                                              (Bool -> String -> [String] -> [String] -> KDProofContext
KDProofStep Bool
False String
nm [] [String
"Measure is non-negative"])
                                              (SBool -> Maybe SBool
forall a. a -> Maybe a
Just SBool
inductionIntros)
                                              SBool
ms
                                              (\(Int, Maybe NominalDiffTime)
d -> SMTConfig
-> String
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishKD SMTConfig
cfg String
"Q.E.D." (Int, Maybe NominalDiffTime)
d [])
       case inductionBaseCase of
          Maybe SBool
Nothing -> [String] -> QueryT IO ()
queryDebug [String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Induction" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
qual String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", there is no base case to prove."]
          Just SBool
bc -> do [String] -> QueryT IO ()
queryDebug [String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Induction, proving base case:"]
                        SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe SBool
-> SBool
-> ((Int, Maybe NominalDiffTime) -> IO ())
-> QueryT IO ()
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe SBool
-> a
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep SMTConfig
cfg KDState
kdSt String
"Step" Int
1
                                              (Bool -> String -> [String] -> [String] -> KDProofContext
KDProofStep Bool
False String
nm [] [String
"Base"])
                                              (SBool -> Maybe SBool
forall a. a -> Maybe a
Just SBool
inductionIntros)
                                              SBool
bc
                                              (\(Int, Maybe NominalDiffTime)
d -> SMTConfig
-> String
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishKD SMTConfig
cfg String
"Q.E.D." (Int, Maybe NominalDiffTime)
d [])

       proveProofTree cfg kdSt nm (result, inductiveStep) inductionIntros inductionProofTree

-- Induction strategy helper
mkIndStrategy :: EqSymbolic a => Maybe SBool -> Maybe SBool -> (SBool, KDProofRaw a) -> SBool -> InductionStrategy
mkIndStrategy :: forall a.
EqSymbolic a =>
Maybe SBool
-> Maybe SBool
-> (SBool, KDProofRaw a)
-> SBool
-> InductionStrategy
mkIndStrategy Maybe SBool
mbMeasure Maybe SBool
mbBaseCase (SBool, KDProofRaw a)
indSteps SBool
step =
        let CalcStrategy { SBool
calcIntros :: CalcStrategy -> SBool
calcIntros :: SBool
calcIntros, KDProof
calcProofTree :: CalcStrategy -> KDProof
calcProofTree :: KDProof
calcProofTree } = (SBool, KDProofRaw a) -> CalcStrategy
forall a. EqSymbolic a => (SBool, KDProofRaw a) -> CalcStrategy
mkCalcSteps (SBool, KDProofRaw a)
indSteps
        in InductionStrategy { inductionIntros :: SBool
inductionIntros    = SBool
calcIntros
                             , inductionMeasure :: Maybe SBool
inductionMeasure   = Maybe SBool
mbMeasure
                             , inductionBaseCase :: Maybe SBool
inductionBaseCase  = Maybe SBool
mbBaseCase
                             , inductionProofTree :: KDProof
inductionProofTree = KDProof
calcProofTree
                             , inductiveStep :: SBool
inductiveStep      = SBool
step
                             }

-- | Create a new variable with the given name, return both the variable and the name
mkVar :: (KnownSymbol n, SymVal a) => proxy n -> Symbolic (SBV a, String)
mkVar :: forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar proxy n
x = do let nn :: String
nn = proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy n
x
             n <- String -> Symbolic (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nn
             pure (n, nn)

-- | Create a new variable with the given name, return both the variable and the name. List version.
mkLVar :: (KnownSymbol n, SymVal a) => proxy n -> Symbolic (SBV a, SList a, String)
mkLVar :: forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar proxy n
x = do let nxs :: String
nxs = proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy n
x
                  nx :: String
nx  = String -> String
singular String
nxs
              e  <- String -> Symbolic (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
nx
              es <- free nxs
              pure (e, es, nx ++ ":" ++ nxs)

-- | Helper for induction result
indResult :: [String] -> SBool -> SBool
indResult :: [String] -> SBool -> SBool
indResult [String]
nms = (Bool -> Bool) -> String -> SBool -> SBool
forall a. SymVal a => (a -> Bool) -> String -> SBV a -> SBV a
observeIf Bool -> Bool
not (String
"P(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
nms String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")")

-- | Induction over 'SInteger'
instance (KnownSymbol nn, EqSymbolic z) => Inductive (Forall nn Integer -> SBool) (SInteger -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition (Forall nn Integer -> SBool) =>
(Forall nn Integer -> SBool)
-> (Proof -> SInteger -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nn Integer -> SBool
result Proof -> SInteger -> (SBool, KDProofRaw z)
steps = do
       (n, nn) <- Proxy nn -> Symbolic (SInteger, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nn)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall 0)))
                            (steps (internalAxiom "IH" (n .>= zero .=> result (Forall n))) n)
                            (indResult [nn ++ "+1"] (result (Forall (n+1))))

-- | Induction over 'SInteger', taking an extra argument
instance (KnownSymbol nn, KnownSymbol na, SymVal a, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> SBool) (SInteger -> SBV a -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition (Forall nn Integer -> Forall na a -> SBool) =>
(Forall nn Integer -> Forall na a -> SBool)
-> (Proof -> SInteger -> SBV a -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nn Integer -> Forall na a -> SBool
result Proof -> SInteger -> SBV a -> (SBool, KDProofRaw z)
steps = do
       (n, nn) <- Proxy nn -> Symbolic (SInteger, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nn)
       (a, na) <- mkVar (Proxy @na)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall 0) (Forall a)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
forall a. Measure a => a
zero SBool -> SBool -> SBool
.=> Forall nn Integer -> Forall na a -> SBool
result (SInteger -> Forall nn Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
n) (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a'))) n a)
                            (indResult [nn ++ "+1", na] (result (Forall (n+1)) (Forall a)))

-- | Induction over 'SInteger', taking two extra arguments
instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> SBool) (SInteger -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition
  (Forall nn Integer -> Forall na a -> Forall nb b -> SBool) =>
(Forall nn Integer -> Forall na a -> Forall nb b -> SBool)
-> (Proof -> SInteger -> SBV a -> SBV b -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nn Integer -> Forall na a -> Forall nb b -> SBool
result Proof -> SInteger -> SBV a -> SBV b -> (SBool, KDProofRaw z)
steps = do
       (n, nn) <- Proxy nn -> Symbolic (SInteger, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nn)
       (a, na) <- mkVar (Proxy @na)
       (b, nb) <- mkVar (Proxy @nb)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall 0) (Forall a) (Forall b)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
forall a. Measure a => a
zero SBool -> SBool -> SBool
.=> Forall nn Integer -> Forall na a -> Forall nb b -> SBool
result (SInteger -> Forall nn Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
n) (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'))) n a b)
                            (indResult [nn ++ "+1", na, nb] (result (Forall (n+1)) (Forall a) (Forall b)))

-- | Induction over 'SInteger', taking three extra arguments
instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition
  (Forall nn Integer
   -> Forall na a -> Forall nb b -> Forall nc c -> SBool) =>
(Forall nn Integer
 -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> (Proof
    -> SInteger -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nn Integer
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result Proof
-> SInteger -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)
steps = do
       (n, nn) <- Proxy nn -> Symbolic (SInteger, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nn)
       (a, na) <- mkVar (Proxy @na)
       (b, nb) <- mkVar (Proxy @nb)
       (c, nc) <- mkVar (Proxy @nc)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall 0) (Forall a) (Forall b) (Forall c)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
forall a. Measure a => a
zero SBool -> SBool -> SBool
.=> Forall nn Integer
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SInteger -> Forall nn Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
n) (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'))) n a b c)
                            (indResult [nn ++ "+1", na, nb, nc] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c)))

-- | Induction over 'SInteger', taking four extra arguments
instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition
  (Forall nn Integer
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> SBool) =>
(Forall nn 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, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nn 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, KDProofRaw z)
steps = do
       (n, nn) <- Proxy nn -> Symbolic (SInteger, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nn)
       (a, na) <- mkVar (Proxy @na)
       (b, nb) <- mkVar (Proxy @nb)
       (c, nc) <- mkVar (Proxy @nc)
       (d, nd) <- mkVar (Proxy @nd)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall 0) (Forall a) (Forall b) (Forall c) (Forall d)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) (Forall SBV d
d' :: Forall nd d) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
forall a. Measure a => a
zero SBool -> SBool -> SBool
.=> Forall nn Integer
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SInteger -> Forall nn Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
n) (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'))) n a b c d)
                            (indResult [nn ++ "+1", na, nb, nc, nd] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c) (Forall d)))

-- | Induction over 'SInteger', taking five extra arguments
instance (KnownSymbol nn, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z) => Inductive (Forall nn Integer -> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> Forall ne e -> SBool) (SInteger -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition
  (Forall nn Integer
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> Forall ne e
   -> SBool) =>
(Forall nn Integer
 -> Forall na a
 -> Forall nb b
 -> Forall nc c
 -> Forall nd d
 -> Forall ne e
 -> SBool)
-> (Proof
    -> SInteger
    -> SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nn Integer
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result Proof
-> SInteger
-> SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> (SBool, KDProofRaw z)
steps = do
       (n, nn) <- Proxy nn -> Symbolic (SInteger, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nn)
       (a, na) <- mkVar (Proxy @na)
       (b, nb) <- mkVar (Proxy @nb)
       (c, nc) <- mkVar (Proxy @nc)
       (d, nd) <- mkVar (Proxy @nd)
       (e, ne) <- mkVar (Proxy @ne)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall 0) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) (Forall SBV d
d' :: Forall nd d) (Forall SBV e
e' :: Forall ne e) -> SInteger
n SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
forall a. Measure a => a
zero SBool -> SBool -> SBool
.=> Forall nn Integer
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SInteger -> Forall nn Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SInteger
n) (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'))) n a b c d e)
                            (indResult [nn ++ "+1", na, nb, nc, nd, ne] (result (Forall (n+1)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))

-- 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"

-- | Induction over 'SList'
instance (KnownSymbol nxs, SymVal x, EqSymbolic z) => Inductive (Forall nxs [x] -> SBool) (SBV x -> SList x -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition (Forall nxs [x] -> SBool) =>
(Forall nxs [x] -> SBool)
-> (Proof -> SBV x -> SList x -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nxs [x] -> SBool
result Proof -> SBV x -> SList x -> (SBool, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil)))
                            (steps (internalAxiom "IH" (result (Forall xs))) x xs)
                            (indResult [nxxs] (result (Forall (x SL..: xs))))

-- | Induction over 'SList', taking an extra argument
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, EqSymbolic z) => Inductive (Forall nxs [x] -> Forall na a -> SBool) (SBV x -> SList x -> SBV a -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition (Forall nxs [x] -> Forall na a -> SBool) =>
(Forall nxs [x] -> Forall na a -> SBool)
-> (Proof -> SBV x -> SList x -> SBV a -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nxs [x] -> Forall na a -> SBool
result Proof -> SBV x -> SList x -> SBV a -> (SBool, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (a, na)       <- mkVar  (Proxy @na)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil) (Forall a)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) -> Forall nxs [x] -> Forall na a -> SBool
result (SList x -> Forall nxs [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'))) x xs a)
                            (indResult [nxxs, na] (result (Forall (x SL..: xs)) (Forall a)))

-- | Induction over 'SList', taking two extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition
  (Forall nxs [x] -> Forall na a -> Forall nb b -> SBool) =>
(Forall nxs [x] -> Forall na a -> Forall nb b -> SBool)
-> (Proof
    -> SBV x -> SList x -> SBV a -> SBV b -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nxs [x] -> Forall na a -> Forall nb b -> SBool
result Proof
-> SBV x -> SList x -> SBV a -> SBV b -> (SBool, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (a, na)       <- mkVar  (Proxy @na)
       (b, nb)       <- mkVar  (Proxy @nb)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil) (Forall a) (Forall b)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) -> Forall nxs [x] -> Forall na a -> Forall nb b -> SBool
result (SList x -> Forall nxs [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'))) x xs a b)
                            (indResult [nxxs, na, nb] (result (Forall (x SL..: xs)) (Forall a) (Forall b)))

-- | Induction over 'SList', taking three extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => Inductive (Forall nxs [x] -> Forall na a -> Forall nb b -> Forall nc c -> SBool) (SBV x -> SList x -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition
  (Forall nxs [x]
   -> Forall na a -> Forall nb b -> Forall nc c -> SBool) =>
(Forall nxs [x]
 -> Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> (Proof
    -> SBV x
    -> SList x
    -> SBV a
    -> SBV b
    -> SBV c
    -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nxs [x]
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result Proof
-> SBV x
-> SList x
-> SBV a
-> SBV b
-> SBV c
-> (SBool, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (a, na)       <- mkVar  (Proxy @na)
       (b, nb)       <- mkVar  (Proxy @nb)
       (c, nc)       <- mkVar  (Proxy @nc)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) -> Forall nxs [x]
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SList x -> Forall nxs [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'))) x xs a b c)
                            (indResult [nxxs, na, nb, nc] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c)))

-- | Induction over 'SList', taking four extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => Inductive (Forall nxs [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, KDProofRaw z)) where
  inductionStrategy :: Proposition
  (Forall nxs [x]
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> SBool) =>
(Forall nxs [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, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nxs [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, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (a, na)       <- mkVar  (Proxy @na)
       (b, nb)       <- mkVar  (Proxy @nb)
       (c, nc)       <- mkVar  (Proxy @nc)
       (d, nd)       <- mkVar  (Proxy @nd)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) (Forall SBV d
d' :: Forall nd d) -> Forall nxs [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SList x -> Forall nxs [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'))) x xs a b c d)
                            (indResult [nxxs, na, nb, nc, nd] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c) (Forall d)))

-- | Induction over 'SList', taking five extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z) => Inductive (Forall nxs [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, KDProofRaw z)) where
  inductionStrategy :: Proposition
  (Forall nxs [x]
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> Forall ne e
   -> SBool) =>
(Forall nxs [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, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy Forall nxs [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, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (a, na)       <- mkVar  (Proxy @na)
       (b, nb)       <- mkVar  (Proxy @nb)
       (c, nc)       <- mkVar  (Proxy @nc)
       (d, nd)       <- mkVar  (Proxy @nd)
       (e, ne)       <- mkVar  (Proxy @ne)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) (Forall SBV d
d' :: Forall nd d) (Forall SBV e
e' :: Forall ne e) -> Forall nxs [x]
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SList x -> Forall nxs [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'))) x xs a b c d e)
                            (indResult [nxxs, na, nb, nc, nd, ne] (result (Forall (x SL..: xs)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))

-- | Induction over two 'SList', simultaneously
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> SBool) ((SBV x, SList x, SBV y, SList y) -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition ((Forall nxs [x], Forall nys [y]) -> SBool) =>
((Forall nxs [x], Forall nys [y]) -> SBool)
-> (Proof
    -> (SBV x, SList x, SBV y, SList y) -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy (Forall nxs [x], Forall nys [y]) -> SBool
result Proof -> (SBV x, SList x, SBV y, SList y) -> (SBool, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (y, ys, nyys) <- mkLVar (Proxy @nys)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil, Forall SL.nil) .&& result (Forall SL.nil, Forall (y SL..: ys)) .&& result (Forall (x SL..: xs), Forall SL.nil)))
                            (steps (internalAxiom "IH" (result (Forall xs, Forall ys))) (x, xs, y, ys))
                            (indResult [nxxs, nyys] (result (Forall (x SL..: xs), Forall (y SL..: ys))))

-- | Induction over two 'SList', simultaneously, taking an extra argument
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool) ((SBV x, SList x, SBV y, SList y) -> SBV a -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition
  ((Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool) =>
((Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool)
-> (Proof
    -> (SBV x, SList x, SBV y, SList y)
    -> SBV a
    -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy (Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool
result Proof
-> (SBV x, SList x, SBV y, SList y)
-> SBV a
-> (SBool, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (y, ys, nyys) <- mkLVar (Proxy @nys)
       (a, na)       <- mkVar  (Proxy @na)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) -> (Forall nxs [x], Forall nys [y]) -> Forall na a -> SBool
result (SList x -> Forall nxs [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs, SList y -> Forall nys [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'))) (x, xs, y, ys) a)
                            (indResult [nxxs, nyys, na] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a)))

-- | Induction over two 'SList', simultaneously, taking two extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [y]) -> Forall na a -> Forall nb b -> SBool) ((SBV x, SList x, SBV y, SList y) -> SBV a -> SBV b -> (SBool, KDProofRaw z)) where
  inductionStrategy :: Proposition
  ((Forall nxs [x], Forall nys [y])
   -> Forall na a -> Forall nb b -> SBool) =>
((Forall nxs [x], Forall nys [y])
 -> Forall na a -> Forall nb b -> SBool)
-> (Proof
    -> (SBV x, SList x, SBV y, SList y)
    -> SBV a
    -> SBV b
    -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy (Forall nxs [x], Forall nys [y])
-> Forall na a -> Forall nb b -> SBool
result Proof
-> (SBV x, SList x, SBV y, SList y)
-> SBV a
-> SBV b
-> (SBool, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (y, ys, nyys) <- mkLVar (Proxy @nys)
       (a, na)       <- mkVar  (Proxy @na)
       (b, nb)       <- mkVar  (Proxy @nb)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) -> (Forall nxs [x], Forall nys [y])
-> Forall na a -> Forall nb b -> SBool
result (SList x -> Forall nxs [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs, SList y -> Forall nys [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'))) (x, xs, y, ys) a b)
                            (indResult [nxxs, nyys, na, nb] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b)))

-- | Generalized induction with one parameter
instance (KnownSymbol na, SymVal a, EqSymbolic z, Measure m) => SInductive (Forall na a -> SBool) (SBV a -> m) (SBV a -> (SBool, KDProofRaw z)) where
  sInductionStrategy :: Proposition (Forall na a -> SBool) =>
(Forall na a -> SBool)
-> (SBV a -> m)
-> (Proof -> SBV a -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
sInductionStrategy Forall na a -> SBool
result SBV a -> m
measure Proof -> SBV a -> (SBool, KDProofRaw z)
steps = do
      (a, na) <- Proxy na -> Symbolic (SBV a, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
      pure $ mkIndStrategy (Just (measure a .>= zero))
                           Nothing
                           (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) -> SBV a -> m
measure SBV a
a' m -> m -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a -> m
measure SBV a
a SBool -> SBool -> SBool
.=> Forall na a -> SBool
result (SBV a -> Forall na a
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV a
a'))) a)
                           (indResult [na] (result (Forall a)))

-- | Generalized induction with two parameters
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, EqSymbolic z, Measure m) => SInductive (Forall na a -> Forall nb b -> SBool) (SBV a -> SBV b -> m) (SBV a -> SBV b -> (SBool, KDProofRaw z)) where
  sInductionStrategy :: Proposition (Forall na a -> Forall nb b -> SBool) =>
(Forall na a -> Forall nb b -> SBool)
-> (SBV a -> SBV b -> m)
-> (Proof -> SBV a -> SBV b -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
sInductionStrategy Forall na a -> Forall nb b -> SBool
result SBV a -> SBV b -> m
measure Proof -> SBV a -> SBV b -> (SBool, KDProofRaw z)
steps = do
      (a, na) <- Proxy na -> Symbolic (SBV a, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
      (b, nb) <- mkVar (Proxy @nb)
      pure $ mkIndStrategy (Just (measure a b .>= zero))
                           Nothing
                           (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) -> SBV a -> SBV b -> m
measure SBV a
a' SBV b
b' m -> m -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a -> SBV b -> m
measure SBV a
a SBV b
b SBool -> SBool -> SBool
.=> Forall na a -> Forall nb b -> SBool
result (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'))) a b)
                           (indResult [na, nb] (result (Forall a) (Forall b)))

-- | Generalized induction with three parameters
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z, Measure m) => SInductive (Forall na a -> Forall nb b -> Forall nc c -> SBool) (SBV a -> SBV b -> SBV c -> m) (SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)) where
  sInductionStrategy :: Proposition (Forall na a -> Forall nb b -> Forall nc c -> SBool) =>
(Forall na a -> Forall nb b -> Forall nc c -> SBool)
-> (SBV a -> SBV b -> SBV c -> m)
-> (Proof -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
sInductionStrategy Forall na a -> Forall nb b -> Forall nc c -> SBool
result SBV a -> SBV b -> SBV c -> m
measure Proof -> SBV a -> SBV b -> SBV c -> (SBool, KDProofRaw z)
steps = do
      (a, na) <- Proxy na -> Symbolic (SBV a, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
      (b, nb) <- mkVar (Proxy @nb)
      (c, nc) <- mkVar (Proxy @nc)
      pure $ mkIndStrategy (Just (measure a b c .>= zero))
                           Nothing
                           (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) -> SBV a -> SBV b -> SBV c -> m
measure SBV a
a' SBV b
b' SBV c
c' m -> m -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a -> SBV b -> SBV c -> m
measure SBV a
a SBV b
b SBV c
c SBool -> SBool -> SBool
.=> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (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'))) a b c)
                           (indResult [na, nb, nc] (result (Forall a) (Forall b) (Forall c)))

-- | Generalized induction with four parameters
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z, Measure m) => SInductive (Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) (SBV a -> SBV b -> SBV c -> SBV d -> m) (SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)) where
  sInductionStrategy :: Proposition
  (Forall na a
   -> Forall nb b -> Forall nc c -> Forall nd d -> SBool) =>
(Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool)
-> (SBV a -> SBV b -> SBV c -> SBV d -> m)
-> (Proof
    -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
sInductionStrategy Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool
result SBV a -> SBV b -> SBV c -> SBV d -> m
measure Proof -> SBV a -> SBV b -> SBV c -> SBV d -> (SBool, KDProofRaw z)
steps = do
      (a, na) <- Proxy na -> Symbolic (SBV a, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
      (b, nb) <- mkVar (Proxy @nb)
      (c, nc) <- mkVar (Proxy @nc)
      (d, nd) <- mkVar (Proxy @nd)
      pure $ mkIndStrategy (Just (measure a b c d .>= zero))
                           Nothing
                           (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) (Forall SBV d
d' :: Forall nd d) -> SBV a -> SBV b -> SBV c -> SBV d -> m
measure SBV a
a' SBV b
b' SBV c
c' SBV d
d' m -> m -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a -> SBV b -> SBV c -> SBV d -> m
measure SBV a
a SBV b
b SBV c
c SBV d
d SBool -> SBool -> SBool
.=> Forall na a -> Forall nb b -> Forall nc c -> Forall nd d -> SBool
result (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'))) a b c d)
                           (indResult [na, nb, nc, nd] (result (Forall a) (Forall b) (Forall c) (Forall d)))

-- | Generalized induction with five parameters
instance (KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, KnownSymbol ne, SymVal e, EqSymbolic z, Measure m) => SInductive (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 -> m) (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> (SBool, KDProofRaw z)) where
  sInductionStrategy :: Proposition
  (Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> Forall ne e
   -> SBool) =>
(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 -> m)
-> (Proof
    -> SBV a
    -> SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> (SBool, KDProofRaw z))
-> Symbolic InductionStrategy
sInductionStrategy 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 -> m
measure Proof
-> SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> (SBool, KDProofRaw z)
steps = do
      (a, na) <- Proxy na -> Symbolic (SBV a, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, String)
mkVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @na)
      (b, nb) <- mkVar (Proxy @nb)
      (c, nc) <- mkVar (Proxy @nc)
      (d, nd) <- mkVar (Proxy @nd)
      (e, ne) <- mkVar (Proxy @ne)
      pure $ mkIndStrategy (Just (measure a b c d e .>= zero))
                           Nothing
                           (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) (Forall SBV d
d' :: Forall nd d) (Forall SBV e
e' :: Forall ne e) -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> m
measure SBV a
a' SBV b
b' SBV c
c' SBV d
d' SBV e
e' m -> m -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> m
measure SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e SBool -> SBool -> SBool
.=> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (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'))) a b c d e)
                           (indResult [na, nb, nc, nd, ne] (result (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))

-- | Induction over two 'SList', simultaneously, taking three extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [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, KDProofRaw z)) where
  inductionStrategy :: Proposition
  ((Forall nxs [x], Forall nys [y])
   -> Forall na a -> Forall nb b -> Forall nc c -> SBool) =>
((Forall nxs [x], Forall nys [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, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy (Forall nxs [x], Forall nys [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, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (y, ys, nyys) <- mkLVar (Proxy @nys)
       (a, na)       <- mkVar  (Proxy @na)
       (b, nb)       <- mkVar  (Proxy @nb)
       (c, nc)       <- mkVar  (Proxy @nc)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) -> (Forall nxs [x], Forall nys [y])
-> Forall na a -> Forall nb b -> Forall nc c -> SBool
result (SList x -> Forall nxs [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs, SList y -> Forall nys [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'))) (x, xs, y, ys) a b c)
                            (indResult [nxxs, nyys, na, nb, nc] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c)))

-- | Induction over two 'SList', simultaneously, taking four extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, SymVal y, KnownSymbol na, SymVal a, KnownSymbol nb, SymVal b, KnownSymbol nc, SymVal c, KnownSymbol nd, SymVal d, EqSymbolic z) => Inductive ((Forall nxs [x], Forall nys [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, KDProofRaw z)) where
  inductionStrategy :: Proposition
  ((Forall nxs [x], Forall nys [y])
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> SBool) =>
((Forall nxs [x], Forall nys [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, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy (Forall nxs [x], Forall nys [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, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (y, ys, nyys) <- mkLVar (Proxy @nys)
       (a, na)       <- mkVar  (Proxy @na)
       (b, nb)       <- mkVar  (Proxy @nb)
       (c, nc)       <- mkVar  (Proxy @nc)
       (d, nd)       <- mkVar  (Proxy @nd)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) (Forall SBV d
d' :: Forall nd d) -> (Forall nxs [x], Forall nys [y])
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> SBool
result (SList x -> Forall nxs [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs, SList y -> Forall nys [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'))) (x, xs, y, ys) a b c d)
                            (indResult [nxxs, nyys, na, nb, nc, nd] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d)))

-- | Induction over two 'SList', simultaneously, taking five extra arguments
instance (KnownSymbol nxs, SymVal x, KnownSymbol nys, 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 nxs [x], Forall nys [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, KDProofRaw z)) where
  inductionStrategy :: Proposition
  ((Forall nxs [x], Forall nys [y])
   -> Forall na a
   -> Forall nb b
   -> Forall nc c
   -> Forall nd d
   -> Forall ne e
   -> SBool) =>
((Forall nxs [x], Forall nys [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, KDProofRaw z))
-> Symbolic InductionStrategy
inductionStrategy (Forall nxs [x], Forall nys [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, KDProofRaw z)
steps = do
       (x, xs, nxxs) <- Proxy nxs -> Symbolic (SBV x, SList x, String)
forall (n :: Symbol) a (proxy :: Symbol -> *).
(KnownSymbol n, SymVal a) =>
proxy n -> Symbolic (SBV a, SList a, String)
mkLVar (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @nxs)
       (y, ys, nyys) <- mkLVar (Proxy @nys)
       (a, na)       <- mkVar  (Proxy @na)
       (b, nb)       <- mkVar  (Proxy @nb)
       (c, nc)       <- mkVar  (Proxy @nc)
       (d, nd)       <- mkVar  (Proxy @nd)
       (e, ne)       <- mkVar  (Proxy @ne)
       pure $ mkIndStrategy Nothing
                            (Just (result (Forall SL.nil, Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall SL.nil, Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e) .&& result (Forall (x SL..: xs), Forall SL.nil) (Forall a) (Forall b) (Forall c) (Forall d) (Forall e)))
                            (steps (internalAxiom "IH" (\(Forall SBV a
a' :: Forall na a) (Forall SBV b
b' :: Forall nb b) (Forall SBV c
c' :: Forall nc c) (Forall SBV d
d' :: Forall nd d) (Forall SBV e
e' :: Forall ne e) -> (Forall nxs [x], Forall nys [y])
-> Forall na a
-> Forall nb b
-> Forall nc c
-> Forall nd d
-> Forall ne e
-> SBool
result (SList x -> Forall nxs [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SList x
xs, SList y -> Forall nys [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'))) (x, xs, y, ys) a b c d e)
                            (indResult [nxxs, nyys, na, nb, nc, nd, ne] (result (Forall (x SL..: xs), Forall (y SL..: ys)) (Forall a) (Forall b) (Forall c) (Forall d) (Forall 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
            | HelperString String -- Just a text, only used for diagnostics

-- | Get all helpers used in a proof
getAllHelpers :: KDProof -> [Helper]
getAllHelpers :: KDProof -> [Helper]
getAllHelpers (ProofStep   SBool
_           [Helper]
hs               KDProof
p)  = [Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ KDProof -> [Helper]
getAllHelpers KDProof
p
getAllHelpers (ProofBranch (Bool
_ :: Bool) ([String]
_ :: [String]) [(SBool, KDProof)]
ps) = ((SBool, KDProof) -> [Helper]) -> [(SBool, KDProof)] -> [Helper]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (KDProof -> [Helper]
getAllHelpers (KDProof -> [Helper])
-> ((SBool, KDProof) -> KDProof) -> (SBool, KDProof) -> [Helper]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SBool, KDProof) -> KDProof
forall a b. (a, b) -> b
snd) [(SBool, KDProof)]
ps
getAllHelpers (ProofEnd    SBool
_           [Helper]
hs                ) = [Helper]
hs

-- | Get proofs from helpers
getHelperProofs :: Helper -> [Proof]
getHelperProofs :: Helper -> [Proof]
getHelperProofs (HelperProof Proof
p) = [Proof
p]
getHelperProofs HelperAssum {}  = []
getHelperProofs HelperString{}  = []

-- | Get proofs from helpers
getHelperAssumes :: Helper -> [SBool]
getHelperAssumes :: Helper -> [SBool]
getHelperAssumes HelperProof  {} = []
getHelperAssumes (HelperAssum SBool
b) = [SBool
b]
getHelperAssumes HelperString {} = []

-- | Get hint strings from helpers. If there's an explicit comment given, just pass that. If not, collect all the names
getHelperText :: [Helper] -> [String]
getHelperText :: [Helper] -> [String]
getHelperText [Helper]
hs = case [String
s | HelperString String
s <- [Helper]
hs] of
                     [] -> (Helper -> [String]) -> [Helper] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [String]
collect [Helper]
hs
                     [String]
ss -> [String]
ss
  where collect :: Helper -> [String]
        collect :: Helper -> [String]
collect (HelperProof  Proof
p) = [Proof -> String
proofName Proof
p | Proof -> Bool
isUserAxiom Proof
p]  -- Don't put out internals (inductive hypotheses)
        collect HelperAssum  {}  = []
        collect (HelperString String
s) = [String
s]

-- | 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.
hasm :: SBool -> Helper
hasm :: SBool -> Helper
hasm = 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

-- | Smart constructor for adding a comment.
hcmnt :: String -> Helper
hcmnt :: String -> Helper
hcmnt = String -> Helper
HelperString

-- | A proof is a sequence of steps, supporting branching
data KDProofGen a bh b = ProofStep   a    [Helper] (KDProofGen a bh b)          -- ^ A single step
                       | ProofBranch Bool bh       [(SBool, KDProofGen a bh b)] -- ^ A branching step. Bool indicates if completeness check is needed
                       | ProofEnd    b    [Helper]                              -- ^ End of proof

-- | A proof, as written by the user. No produced result, but helpers on branches
type KDProofRaw a = KDProofGen a [Helper] ()

-- | A proof, as processed by KD. Producing a boolean result and each step is a boolean. Helpers on branches dispersed down, only strings are left for printing
type KDProof = KDProofGen SBool [String] SBool

-- | Collect dependencies for a KDProof
getDependencies :: KDProof -> [Proof]
getDependencies :: KDProof -> [Proof]
getDependencies = KDProof -> [Proof]
forall {a} {bh} {b}. KDProofGen a bh b -> [Proof]
collect
  where collect :: KDProofGen a bh b -> [Proof]
collect (ProofStep   a
_ [Helper]
hs KDProofGen a bh b
next) = (Helper -> [Proof]) -> [Helper] -> [Proof]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [Proof]
getHelperProofs [Helper]
hs [Proof] -> [Proof] -> [Proof]
forall a. [a] -> [a] -> [a]
++ KDProofGen a bh b -> [Proof]
collect KDProofGen a bh b
next
        collect (ProofBranch Bool
_ bh
_  [(SBool, KDProofGen a bh b)]
bs)   = ((SBool, KDProofGen a bh b) -> [Proof])
-> [(SBool, KDProofGen a bh b)] -> [Proof]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (KDProofGen a bh b -> [Proof]
collect (KDProofGen a bh b -> [Proof])
-> ((SBool, KDProofGen a bh b) -> KDProofGen a bh b)
-> (SBool, KDProofGen a bh b)
-> [Proof]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SBool, KDProofGen a bh b) -> KDProofGen a bh b
forall a b. (a, b) -> b
snd) [(SBool, KDProofGen a bh b)]
bs
        collect (ProofEnd    b
_    [Helper]
hs)   = (Helper -> [Proof]) -> [Helper] -> [Proof]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Helper -> [Proof]
getHelperProofs [Helper]
hs

-- | Class capturing giving a proof-step helper
type family Hinted a where
  Hinted (KDProofRaw a) = KDProofRaw a
  Hinted a              = KDProofRaw a

-- | Attaching a hint
(??) :: HintsTo a b => a -> b -> Hinted a
?? :: forall a b. HintsTo a b => a -> b -> Hinted a
(??) = a -> b -> Hinted a
forall a b. HintsTo a b => a -> b -> Hinted a
addHint
infixl 2 ??

-- | Class capturing hints
class HintsTo a b where
  addHint :: a -> b -> Hinted a

-- | Giving just one proof as a helper.
instance Hinted a ~ KDProofRaw a => HintsTo a Proof where
  a
a addHint :: a -> Proof -> Hinted a
`addHint` Proof
p = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep a
a [Proof -> Helper
HelperProof Proof
p] KDProofRaw a
forall a. KDProofRaw a
qed

-- | Giving just one boolean as a helper.
instance Hinted a ~ KDProofRaw a => HintsTo a SBool where
  a
a addHint :: a -> SBool -> Hinted a
`addHint` SBool
p = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep a
a [SBool -> Helper
HelperAssum SBool
p] KDProofRaw a
forall a. KDProofRaw a
qed

-- | Giving just one helper
instance Hinted a ~ KDProofRaw a => HintsTo a Helper where
  a
a addHint :: a -> Helper -> Hinted a
`addHint` Helper
h = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep a
a [Helper
h] KDProofRaw a
forall a. KDProofRaw a
qed

-- | Giving a bunch of proofs as a helper.
instance Hinted a ~ KDProofRaw a => HintsTo a [Proof] where
  a
a addHint :: a -> [Proof] -> Hinted a
`addHint` [Proof]
ps = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep a
a ((Proof -> Helper) -> [Proof] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map Proof -> Helper
HelperProof [Proof]
ps) KDProofRaw a
forall a. KDProofRaw a
qed

-- | Giving a bunch of booleans as a helper.
instance Hinted a ~ KDProofRaw a => HintsTo a [SBool] where
  a
a addHint :: a -> [SBool] -> Hinted a
`addHint` [SBool]
ps = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep a
a ((SBool -> Helper) -> [SBool] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> Helper
HelperAssum [SBool]
ps) KDProofRaw a
forall a. KDProofRaw a
qed

-- | Giving a set of helpers
instance Hinted a ~ KDProofRaw a => HintsTo a [Helper] where
  a
a addHint :: a -> [Helper] -> Hinted a
`addHint` [Helper]
hs = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep a
a [Helper]
hs KDProofRaw a
forall a. KDProofRaw a
qed

-- | Giving user a hint as a string. This doesn't actually do anything for the solver, it just helps with readability
instance Hinted a ~ KDProofRaw a => HintsTo a String where
  a
a addHint :: a -> String -> Hinted a
`addHint` String
s = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep a
a [String -> Helper
HelperString String
s] KDProofRaw a
forall a. KDProofRaw a
qed

-- | Giving just one proof as a helper, starting from a proof
instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) Proof where
  ProofStep   a
a [Helper]
hs KDProofRaw a
ps addHint :: KDProofRaw a -> Proof -> Hinted (KDProofRaw a)
`addHint` Proof
h = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep   a
a ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Proof -> Helper
HelperProof Proof
h]) KDProofRaw a
ps
  ProofBranch Bool
b [Helper]
hs [(SBool, KDProofRaw a)]
bs `addHint` Proof
h = Bool -> [Helper] -> [(SBool, KDProofRaw a)] -> KDProofRaw a
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Proof -> Helper
HelperProof Proof
h]) [(SBool, KDProofRaw a)]
bs
  ProofEnd    ()
b [Helper]
hs    `addHint` Proof
h = () -> [Helper] -> KDProofRaw a
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd    ()
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Proof -> Helper
HelperProof Proof
h])

-- | Giving just one boolean as a helper.
instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) SBool where
  ProofStep   a
a [Helper]
hs KDProofRaw a
ps addHint :: KDProofRaw a -> SBool -> Hinted (KDProofRaw a)
`addHint` SBool
h = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep   a
a ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [SBool -> Helper
HelperAssum SBool
h]) KDProofRaw a
ps
  ProofBranch Bool
b [Helper]
hs [(SBool, KDProofRaw a)]
bs `addHint` SBool
h = Bool -> [Helper] -> [(SBool, KDProofRaw a)] -> KDProofRaw a
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [SBool -> Helper
HelperAssum SBool
h]) [(SBool, KDProofRaw a)]
bs
  ProofEnd    ()
b [Helper]
hs    `addHint` SBool
h = () -> [Helper] -> KDProofRaw a
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd    ()
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [SBool -> Helper
HelperAssum SBool
h])

-- | Giving just one helper
instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) Helper where
  ProofStep   a
a [Helper]
hs KDProofRaw a
ps addHint :: KDProofRaw a -> Helper -> Hinted (KDProofRaw a)
`addHint` Helper
h = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep   a
a ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper
h]) KDProofRaw a
ps
  ProofBranch Bool
b [Helper]
hs [(SBool, KDProofRaw a)]
bs `addHint` Helper
h = Bool -> [Helper] -> [(SBool, KDProofRaw a)] -> KDProofRaw a
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper
h]) [(SBool, KDProofRaw a)]
bs
  ProofEnd    ()
b [Helper]
hs    `addHint` Helper
h = () -> [Helper] -> KDProofRaw a
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd    ()
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper
h])

-- | Giving a bunch of proofs as a helper.
instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) [Proof] where
  ProofStep   a
a [Helper]
hs KDProofRaw a
ps addHint :: KDProofRaw a -> [Proof] -> Hinted (KDProofRaw a)
`addHint` [Proof]
hs' = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep   a
a ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ (Proof -> Helper) -> [Proof] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map Proof -> Helper
HelperProof [Proof]
hs') KDProofRaw a
ps
  ProofBranch Bool
b [Helper]
hs [(SBool, KDProofRaw a)]
bs `addHint` [Proof]
hs' = Bool -> [Helper] -> [(SBool, KDProofRaw a)] -> KDProofRaw a
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ (Proof -> Helper) -> [Proof] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map Proof -> Helper
HelperProof [Proof]
hs') [(SBool, KDProofRaw a)]
bs
  ProofEnd    ()
b [Helper]
hs    `addHint` [Proof]
hs' = () -> [Helper] -> KDProofRaw a
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd    ()
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ (Proof -> Helper) -> [Proof] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map Proof -> Helper
HelperProof [Proof]
hs')

-- | Giving a bunch of booleans as a helper.
instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) [SBool] where
  ProofStep   a
a [Helper]
hs KDProofRaw a
ps addHint :: KDProofRaw a -> [SBool] -> Hinted (KDProofRaw a)
`addHint` [SBool]
hs' = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep   a
a ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ (SBool -> Helper) -> [SBool] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> Helper
HelperAssum [SBool]
hs') KDProofRaw a
ps
  ProofBranch Bool
b [Helper]
hs [(SBool, KDProofRaw a)]
bs `addHint` [SBool]
hs' = Bool -> [Helper] -> [(SBool, KDProofRaw a)] -> KDProofRaw a
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ (SBool -> Helper) -> [SBool] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> Helper
HelperAssum [SBool]
hs') [(SBool, KDProofRaw a)]
bs
  ProofEnd    ()
b [Helper]
hs    `addHint` [SBool]
hs' = () -> [Helper] -> KDProofRaw a
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd    ()
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ (SBool -> Helper) -> [SBool] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> Helper
HelperAssum [SBool]
hs')

-- | Giving a set of helpers
instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) [Helper] where
  ProofStep   a
a [Helper]
hs KDProofRaw a
ps addHint :: KDProofRaw a -> [Helper] -> Hinted (KDProofRaw a)
`addHint` [Helper]
hs' = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep   a
a ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs') KDProofRaw a
ps
  ProofBranch Bool
b [Helper]
hs [(SBool, KDProofRaw a)]
bs `addHint` [Helper]
hs' = Bool -> [Helper] -> [(SBool, KDProofRaw a)] -> KDProofRaw a
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs') [(SBool, KDProofRaw a)]
bs
  ProofEnd    ()
b [Helper]
hs    `addHint` [Helper]
hs' = () -> [Helper] -> KDProofRaw a
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd    ()
b ([Helper]
hs [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [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 {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) String where
  KDProofRaw a
a addHint :: KDProofRaw a -> String -> Hinted (KDProofRaw a)
`addHint` String
s = KDProofRaw a
a KDProofRaw a -> Helper -> Hinted (KDProofRaw a)
forall a b. HintsTo a b => a -> b -> Hinted a
`addHint` String -> Helper
HelperString String
s

-- | Giving a bunch of strings as hints. This doesn't actually do anything for the solver, it just helps with readability
instance {-# OVERLAPPING #-} Hinted (KDProofRaw a) ~ KDProofRaw a => HintsTo (KDProofRaw a) [String] where
  KDProofRaw a
a addHint :: KDProofRaw a -> [String] -> Hinted (KDProofRaw a)
`addHint` [String]
ss = KDProofRaw a
a KDProofRaw a -> [Helper] -> Hinted (KDProofRaw a)
forall a b. HintsTo a b => a -> b -> Hinted a
`addHint` (String -> Helper) -> [String] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map String -> Helper
HelperString [String]
ss

-- | 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 (KDProofRaw a) = KDProofRaw a
  ChainsTo a              = KDProofRaw 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 (KDProofRaw a) where
  chain :: a -> KDProofRaw a -> KDProofRaw a
chain a
x KDProofRaw a
y = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep a
x [] KDProofRaw a
y

-- | Chaining from another proof step
instance ChainStep (KDProofRaw a) (KDProofRaw a) where
  chain :: KDProofRaw a -> KDProofRaw a -> KDProofRaw a
chain (ProofStep   a
a  [Helper]
hs  KDProofRaw a
p)  KDProofRaw a
y = a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep   a
a [Helper]
hs (KDProofRaw a -> KDProofRaw a -> KDProofRaw a
forall a b. ChainStep a b => a -> b -> b
chain KDProofRaw a
p KDProofRaw a
y)
  chain (ProofBranch Bool
c  [Helper]
hs  [(SBool, KDProofRaw a)]
ps) KDProofRaw a
y = Bool -> [Helper] -> [(SBool, KDProofRaw a)] -> KDProofRaw a
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
c [Helper]
hs [(SBool
branchCond, KDProofRaw a -> KDProofRaw a -> KDProofRaw a
forall a b. ChainStep a b => a -> b -> b
chain KDProofRaw a
p KDProofRaw a
y) | (SBool
branchCond, KDProofRaw a
p) <- [(SBool, KDProofRaw a)]
ps]
  chain (ProofEnd    () [Helper]
hs)     KDProofRaw a
y = case KDProofRaw a
y of
                                      ProofStep   a
a  [Helper]
hs' KDProofRaw a
p  -> a -> [Helper] -> KDProofRaw a -> KDProofRaw a
forall a bh b.
a -> [Helper] -> KDProofGen a bh b -> KDProofGen a bh b
ProofStep   a
a  ([Helper]
hs' [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs) KDProofRaw a
p
                                      ProofBranch Bool
b  [Helper]
hs' [(SBool, KDProofRaw a)]
bs -> Bool -> [Helper] -> [(SBool, KDProofRaw a)] -> KDProofRaw a
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
b  ([Helper]
hs' [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs) [(SBool, KDProofRaw a)]
bs
                                      ProofEnd    () [Helper]
hs'    -> () -> [Helper] -> KDProofRaw a
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd    () ([Helper]
hs' [Helper] -> [Helper] -> [Helper]
forall a. [a] -> [a] -> [a]
++ [Helper]
hs)

-- | Mark the end of a calculational proof.
qed :: KDProofRaw a
qed :: forall a. KDProofRaw a
qed = () -> [Helper] -> KDProofGen a [Helper] ()
forall a bh b. b -> [Helper] -> KDProofGen a bh b
ProofEnd () []

-- | Mark a trivial proof. This is essentially the same as 'qed', but reads better in proof scripts.
class Trivial a where
  -- | Mark a proof as trivial, i.e., the solver should be able to deduce it without any help.
  trivial :: a

-- | Trivial proofs with no arguments
instance Trivial (KDProofRaw a) where
  trivial :: KDProofRaw a
trivial = KDProofRaw a
forall a. KDProofRaw a
qed

-- | Trivial proofs with many arguments arguments
instance Trivial a => Trivial (b -> a) where
  trivial :: b -> a
trivial = a -> b -> a
forall a b. a -> b -> a
const a
forall a. Trivial a => a
trivial

-- | Mark a contradictory proof path. This is essentially the same as @sFalse := qed@, but reads better in proof scripts.
class Contradiction a where
  -- | Mark a proof as contradiction, i.e., the solver should be able to conclude it by reasoning that the current path is infeasible
  contradiction :: a

-- | Contradiction proofs with no arguments
instance Contradiction (KDProofRaw SBool) where
  contradiction :: KDProofRaw SBool
contradiction = SBool
sFalse SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed

-- | Contradiction proofs with many arguments
instance Contradiction a => Contradiction (b -> a) where
  contradiction :: b -> a
contradiction = a -> b -> a
forall a b. a -> b -> a
const a
forall a. Contradiction a => a
contradiction


-- | 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] -> KDProofRaw a -> (SBool, KDProofRaw a)
[SBool]
bs |- :: forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- KDProofRaw a
p = ([SBool] -> SBool
sAnd [SBool]
bs, KDProofRaw a
p)
infixl 0 |-

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

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

-- | The boolean case-split
cases :: [(SBool, KDProofRaw a)] -> KDProofRaw a
cases :: forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases = Bool
-> [Helper]
-> [(SBool, KDProofGen a [Helper] ())]
-> KDProofGen a [Helper] ()
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
True []

-- | Case splitting over a list; empty and full cases
split :: SymVal a => SList a -> KDProofRaw r -> (SBV a -> SList a -> KDProofRaw r) -> KDProofRaw r
split :: forall a r.
SymVal a =>
SList a
-> KDProofRaw r
-> (SBV a -> SList a -> KDProofRaw r)
-> KDProofRaw r
split SList a
xs KDProofRaw r
empty SBV a -> SList a -> KDProofRaw r
cons = Bool -> [Helper] -> [(SBool, KDProofRaw r)] -> KDProofRaw r
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
False [] [ (      SList a -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList a
xs,  KDProofRaw r
empty)
                                           , (SBool -> SBool
sNot (SList a -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList a
xs), SBV a -> SList a -> KDProofRaw r
cons (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
SL.head SList a
xs) (SList a -> SList a
forall a. SymVal a => SList a -> SList a
SL.tail SList a
xs))
                                           ]

-- | Case splitting over two lists; empty and full cases for each
split2 :: (SymVal a, SymVal b)
       => (SList a, SList b)
       -> KDProofRaw r
       -> ((SBV b, SList b)                     -> KDProofRaw r) -- empty first
       -> ((SBV a, SList a)                     -> KDProofRaw r) -- empty second
       -> ((SBV a, SList a) -> (SBV b, SList b) -> KDProofRaw r) -- neither empty
       -> KDProofRaw r
split2 :: forall a b r.
(SymVal a, SymVal b) =>
(SList a, SList b)
-> KDProofRaw r
-> ((SBV b, SList b) -> KDProofRaw r)
-> ((SBV a, SList a) -> KDProofRaw r)
-> ((SBV a, SList a) -> (SBV b, SList b) -> KDProofRaw r)
-> KDProofRaw r
split2 (SList a
xs, SList b
ys) KDProofRaw r
ee (SBV b, SList b) -> KDProofRaw r
ec (SBV a, SList a) -> KDProofRaw r
ce (SBV a, SList a) -> (SBV b, SList b) -> KDProofRaw r
cc = Bool -> [Helper] -> [(SBool, KDProofRaw r)] -> KDProofRaw r
forall a bh b.
Bool -> bh -> [(SBool, KDProofGen a bh b)] -> KDProofGen a bh b
ProofBranch Bool
False
                                          []
                                          [ (      SList a -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList a
xs  SBool -> SBool -> SBool
.&&       SList b -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList b
ys , KDProofRaw r
ee)
                                          , (      SList a -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList a
xs  SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (SList b -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList b
ys), (SBV b, SList b) -> KDProofRaw r
ec (SList b -> SBV b
forall a. SymVal a => SList a -> SBV a
SL.head SList b
ys, SList b -> SList b
forall a. SymVal a => SList a -> SList a
SL.tail SList b
ys))
                                          , (SBool -> SBool
sNot (SList a -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList a
xs) SBool -> SBool -> SBool
.&&       SList b -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList b
ys , (SBV a, SList a) -> KDProofRaw r
ce (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
SL.head SList a
xs, SList a -> SList a
forall a. SymVal a => SList a -> SList a
SL.tail SList a
xs))
                                          , (SBool -> SBool
sNot (SList a -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList a
xs) SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (SList b -> SBool
forall a. SymVal a => SList a -> SBool
SL.null SList b
ys), (SBV a, SList a) -> (SBV b, SList b) -> KDProofRaw r
cc (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
SL.head SList a
xs, SList a -> SList a
forall a. SymVal a => SList a -> SList a
SL.tail SList a
xs) (SList b -> SBV b
forall a. SymVal a => SList a -> SBV a
SL.head SList b
ys, SList b -> SList b
forall a. SymVal a => SList a -> SList a
SL.tail SList b
ys))
                                          ]

-- | Specifying a case-split, helps with the boolean case.
(==>) :: SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> :: forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
(==>) = (,)
infix 0 ==>

-- | Alternative unicode for `==>`
(⟹) :: SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
⟹ :: forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
(⟹) = SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
(==>)
infix 0 ⟹

{- HLint ignore module "Eta reduce" -}