-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.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 FunctionalDependencies     #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE TypeAbstractions           #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.KnuckleDragger (
       -- * Propositions and their proofs
         Proposition, Proof
       -- * Adding axioms/definitions
       , axiom
       -- * Basic proofs
       , lemma,        lemmaWith
       , theorem,      theoremWith
       -- * Chain of reasoning
       , chainLemma,   chainLemmaWith
       , chainTheorem, chainTheoremWith
       -- * Induction
       , Induction(..)
       -- * Faking proofs
       , sorry
       -- * Running KnuckleDragger proofs
       , KD, runKD, runKDWith
       ) where

import Control.Monad.Trans (liftIO)

import Data.SBV
import Data.SBV.Tools.KDKernel
import Data.SBV.Tools.KDUtils

import Control.Monad        (when)
import Control.Monad.Reader (ask)

-- | A class for doing equational reasoning style chained proofs. Use 'chainLemma' to prove a given theorem
-- as a sequence of equalities, each step following from the previous.
class ChainLemma steps step | steps -> step 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 @chainLemma name P [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 -> A == B@
  --    * Prove: @H && A == B -> B == C@
  --    * Prove: @H && A == B && B == C -> C == D@
  --    * Prove: @H && A == B && B == C && C == D -> P@
  --    * If all of the above steps succeed, conclude @P@.
  --
  -- Note that if the type of steps (i.e., @A@ .. @D@ above) is 'SBool', then we use implication
  -- as opposed to equality; which better captures line of reasoning.
  --
  -- So, chain-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 error-out. A single step in @H@ indicates a user-error, since there's
  -- no sequence of steps to reason about.
  chainLemma :: Proposition a => String -> a -> steps -> [Proof] -> KD Proof

  -- | Same as chainLemma, except tagged as Theorem
  chainTheorem :: Proposition a => String -> a -> steps -> [Proof] -> KD Proof

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

  -- | Same as chainLemmaWith, except tagged as Theorem
  chainTheoremWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof

  -- | Internal, shouldn't be needed outside the library
  makeSteps :: steps -> [step]
  makeInter :: steps -> step -> step -> SBool

  chainLemma String
nm a
p steps
steps [Proof]
by = do cfg <- KD SMTConfig
forall r (m :: * -> *). MonadReader r m => m r
ask
                                chainLemmaWith cfg nm p steps by

  chainTheorem String
nm a
p steps
steps [Proof]
by = do cfg <- KD SMTConfig
forall r (m :: * -> *). MonadReader r m => m r
ask
                                  chainTheoremWith cfg nm p steps by

  chainLemmaWith   = Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
forall a.
Proposition a =>
Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
forall steps step a.
(ChainLemma steps step, Proposition a) =>
Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
chainGeneric Bool
False
  chainTheoremWith = Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
forall a.
Proposition a =>
Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
forall steps step a.
(ChainLemma steps step, Proposition a) =>
Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
chainGeneric Bool
True

  chainGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> [Proof] -> KD Proof
  chainGeneric Bool
taggedTheorem SMTConfig
cfg String
nm a
result steps
steps [Proof]
base = do
        IO () -> KD ()
forall a. IO a -> KD a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> KD ()) -> IO () -> KD ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Chain: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm
        let proofSteps :: [step]
proofSteps = steps -> [step]
forall steps step. ChainLemma steps step => steps -> [step]
makeSteps steps
steps
            len :: Int
len        = [step] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [step]
proofSteps

        Bool -> KD () -> KD ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (KD () -> KD ()) -> KD () -> KD ()
forall a b. (a -> b) -> a -> b
$
         String -> KD ()
forall a. HasCallStack => String -> a
error (String -> KD ()) -> String -> KD ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
"Incorrect use of chainLemma on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":"
                           , String
"**   There must be either none, or at least two steps."
                           , String
"**   Was given only one step."
                           ]

        Int -> [Proof] -> [SBool] -> KD Proof
forall {a} {t}.
(QuantifiedBool a, QNot a, Skolemize (NegatesTo a),
 Satisfiable (Symbolic (SkolemsTo (NegatesTo a))),
 Constraint Symbolic (SkolemsTo (NegatesTo a)), Show t, Num t) =>
t -> [Proof] -> [a] -> KD Proof
go (Int
1 :: Int) [Proof]
base ((step -> step -> SBool) -> [step] -> [step] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (steps -> step -> step -> SBool
forall steps step.
ChainLemma steps step =>
steps -> step -> step -> SBool
makeInter steps
steps) [step]
proofSteps (Int -> [step] -> [step]
forall a. Int -> [a] -> [a]
drop Int
1 [step]
proofSteps))

     where go :: t -> [Proof] -> [a] -> KD Proof
go t
_ [Proof]
sofar []
              | Bool
taggedTheorem = SMTConfig -> String -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> a -> [Proof] -> KD Proof
theoremWith SMTConfig
cfg String
nm a
result [Proof]
sofar
              | Bool
True          = SMTConfig -> String -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> a -> [Proof] -> KD Proof
lemmaWith   SMTConfig
cfg String
nm a
result [Proof]
sofar
           go t
i [Proof]
sofar (a
p:[a]
ps)
            | Bool
True
            = do step <- SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
lemmaGen SMTConfig
cfg String
"Lemma" ([String
nm, t -> String
forall a. Show a => a -> String
show t
i]) a
p [Proof]
sofar
                 go (i+1) (step : sofar) ps

-- | Chaining lemmas that depend on a single quantified variable.
instance (SymVal a, EqSymbolic z) => ChainLemma (SBV a -> [z]) (SBV a -> z) where
   makeSteps :: (SBV a -> [z]) -> [SBV a -> z]
makeSteps SBV a -> [z]
steps = [\SBV a
a -> SBV a -> [z]
steps SBV a
a [z] -> Int -> z
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [z] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> [z]
steps SBV a
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> [z]) -> (SBV a -> z) -> (SBV a -> z) -> SBool
makeInter SBV a -> [z]
_ SBV a -> z
x SBV a -> z
y = (Forall "a" a -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a -> SBool) -> SBool)
-> (Forall "a" a -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) -> SBV a -> z
x SBV a
a z -> z -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a -> z
y SBV a
a

-- | Chaining lemmas that depend on two quantified variables.
instance (SymVal a, SymVal b, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> [z]) (SBV a -> SBV b -> z) where
   makeSteps :: (SBV a -> SBV b -> [z]) -> [SBV a -> SBV b -> z]
makeSteps SBV a -> SBV b -> [z]
steps = [\SBV a
a SBV b
b -> SBV a -> SBV b -> [z]
steps SBV a
a SBV b
b [z] -> Int -> z
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [z] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> SBV b -> [z]
steps SBV a
forall a. HasCallStack => a
undefined SBV b
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> SBV b -> [z])
-> (SBV a -> SBV b -> z) -> (SBV a -> SBV b -> z) -> SBool
makeInter SBV a -> SBV b -> [z]
_ SBV a -> SBV b -> z
x SBV a -> SBV b -> z
y = (Forall "a" a -> Forall "b" b -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a -> Forall "b" b -> SBool) -> SBool)
-> (Forall "a" a -> Forall "b" b -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) (Forall @"b" SBV b
b) -> SBV a -> SBV b -> z
x SBV a
a SBV b
b z -> z -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a -> SBV b -> z
y SBV a
a SBV b
b

-- | Chaining lemmas that depend on three quantified variables.
instance (SymVal a, SymVal b, SymVal c, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> SBV c -> [z]) (SBV a -> SBV b -> SBV c -> z) where
   makeSteps :: (SBV a -> SBV b -> SBV c -> [z]) -> [SBV a -> SBV b -> SBV c -> z]
makeSteps SBV a -> SBV b -> SBV c -> [z]
steps = [\SBV a
a SBV b
b SBV c
c -> SBV a -> SBV b -> SBV c -> [z]
steps SBV a
a SBV b
b SBV c
c [z] -> Int -> z
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [z] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> SBV b -> SBV c -> [z]
steps SBV a
forall a. HasCallStack => a
undefined SBV b
forall a. HasCallStack => a
undefined SBV c
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> SBV b -> SBV c -> [z])
-> (SBV a -> SBV b -> SBV c -> z)
-> (SBV a -> SBV b -> SBV c -> z)
-> SBool
makeInter SBV a -> SBV b -> SBV c -> [z]
_ SBV a -> SBV b -> SBV c -> z
x SBV a -> SBV b -> SBV c -> z
y = (Forall "a" a -> Forall "b" b -> Forall "c" c -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a -> Forall "b" b -> Forall "c" c -> SBool) -> SBool)
-> (Forall "a" a -> Forall "b" b -> Forall "c" c -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) (Forall @"b" SBV b
b) (Forall @"c" SBV c
c) -> SBV a -> SBV b -> SBV c -> z
x SBV a
a SBV b
b SBV c
c z -> z -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a -> SBV b -> SBV c -> z
y SBV a
a SBV b
b SBV c
c

-- | Chaining lemmas that depend on four quantified variables.
instance (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> SBV c -> SBV d -> [z]) (SBV a -> SBV b -> SBV c -> SBV d -> z) where
   makeSteps :: (SBV a -> SBV b -> SBV c -> SBV d -> [z])
-> [SBV a -> SBV b -> SBV c -> SBV d -> z]
makeSteps SBV a -> SBV b -> SBV c -> SBV d -> [z]
steps = [\SBV a
a SBV b
b SBV c
c SBV d
d -> SBV a -> SBV b -> SBV c -> SBV d -> [z]
steps SBV a
a SBV b
b SBV c
c SBV d
d [z] -> Int -> z
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [z] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> SBV b -> SBV c -> SBV d -> [z]
steps SBV a
forall a. HasCallStack => a
undefined SBV b
forall a. HasCallStack => a
undefined SBV c
forall a. HasCallStack => a
undefined SBV d
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> SBV b -> SBV c -> SBV d -> [z])
-> (SBV a -> SBV b -> SBV c -> SBV d -> z)
-> (SBV a -> SBV b -> SBV c -> SBV d -> z)
-> SBool
makeInter SBV a -> SBV b -> SBV c -> SBV d -> [z]
_ SBV a -> SBV b -> SBV c -> SBV d -> z
x SBV a -> SBV b -> SBV c -> SBV d -> z
y = (Forall "a" a
 -> Forall "b" b -> Forall "c" c -> Forall "d" d -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a
  -> Forall "b" b -> Forall "c" c -> Forall "d" d -> SBool)
 -> SBool)
-> (Forall "a" a
    -> Forall "b" b -> Forall "c" c -> Forall "d" d -> SBool)
-> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) (Forall @"b" SBV b
b) (Forall @"c" SBV c
c) (Forall @"d" SBV d
d) -> SBV a -> SBV b -> SBV c -> SBV d -> z
x SBV a
a SBV b
b SBV c
c SBV d
d z -> z -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a -> SBV b -> SBV c -> SBV d -> z
y SBV a
a SBV b
b SBV c
c SBV d
d

-- | Chaining lemmas that depend on five quantified variables.
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [z]) (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where
   makeSteps :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [z])
-> [SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z]
makeSteps SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [z]
steps = [\SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [z]
steps SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e [z] -> Int -> z
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [z] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [z]
steps SBV a
forall a. HasCallStack => a
undefined SBV b
forall a. HasCallStack => a
undefined SBV c
forall a. HasCallStack => a
undefined SBV d
forall a. HasCallStack => a
undefined SBV e
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [z])
-> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z)
-> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z)
-> SBool
makeInter SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [z]
_ SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z
x SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z
y = (Forall "a" a
 -> Forall "b" b
 -> Forall "c" c
 -> Forall "d" d
 -> Forall "e" e
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a
  -> Forall "b" b
  -> Forall "c" c
  -> Forall "d" d
  -> Forall "e" e
  -> SBool)
 -> SBool)
-> (Forall "a" a
    -> Forall "b" b
    -> Forall "c" c
    -> Forall "d" d
    -> Forall "e" e
    -> SBool)
-> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) (Forall @"b" SBV b
b) (Forall @"c" SBV c
c) (Forall @"d" SBV d
d) (Forall @"e" SBV e
e) -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z
x SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e z -> z -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z
y SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e

-- | Chaining lemmas that depend on a single quantified variable. Overlapping version for 'SBool' that uses implication.
instance {-# OVERLAPPING #-} SymVal a => ChainLemma (SBV a -> [SBool]) (SBV a -> SBool) where
   makeSteps :: (SBV a -> [SBool]) -> [SBV a -> SBool]
makeSteps SBV a -> [SBool]
steps = [\SBV a
a -> SBV a -> [SBool]
steps SBV a
a [SBool] -> Int -> SBool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [SBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> [SBool]
steps SBV a
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> [SBool]) -> (SBV a -> SBool) -> (SBV a -> SBool) -> SBool
makeInter SBV a -> [SBool]
_ SBV a -> SBool
x SBV a -> SBool
y = (Forall "a" a -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a -> SBool) -> SBool)
-> (Forall "a" a -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) -> SBV a -> SBool
x SBV a
a SBool -> SBool -> SBool
.=> SBV a -> SBool
y SBV a
a

-- | Chaining lemmas that depend on two quantified variables. Overlapping version for 'SBool' that uses implication.
instance {-# OVERLAPPING #-} (SymVal a, SymVal b) => ChainLemma (SBV a -> SBV b -> [SBool]) (SBV a -> SBV b -> SBool) where
   makeSteps :: (SBV a -> SBV b -> [SBool]) -> [SBV a -> SBV b -> SBool]
makeSteps SBV a -> SBV b -> [SBool]
steps = [\SBV a
a SBV b
b -> SBV a -> SBV b -> [SBool]
steps SBV a
a SBV b
b [SBool] -> Int -> SBool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [SBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> SBV b -> [SBool]
steps SBV a
forall a. HasCallStack => a
undefined SBV b
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> SBV b -> [SBool])
-> (SBV a -> SBV b -> SBool) -> (SBV a -> SBV b -> SBool) -> SBool
makeInter SBV a -> SBV b -> [SBool]
_ SBV a -> SBV b -> SBool
x SBV a -> SBV b -> SBool
y = (Forall "a" a -> Forall "b" b -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a -> Forall "b" b -> SBool) -> SBool)
-> (Forall "a" a -> Forall "b" b -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) (Forall @"b" SBV b
b) -> SBV a -> SBV b -> SBool
x SBV a
a SBV b
b SBool -> SBool -> SBool
.=> SBV a -> SBV b -> SBool
y SBV a
a SBV b
b

-- | Chaining lemmas that depend on three quantified variables. Overlapping version for 'SBool' that uses implication.
instance {-# OVERLAPPING #-} (SymVal a, SymVal b, SymVal c) => ChainLemma (SBV a -> SBV b -> SBV c -> [SBool]) (SBV a -> SBV b -> SBV c -> SBool) where
   makeSteps :: (SBV a -> SBV b -> SBV c -> [SBool])
-> [SBV a -> SBV b -> SBV c -> SBool]
makeSteps SBV a -> SBV b -> SBV c -> [SBool]
steps = [\SBV a
a SBV b
b SBV c
c -> SBV a -> SBV b -> SBV c -> [SBool]
steps SBV a
a SBV b
b SBV c
c [SBool] -> Int -> SBool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [SBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> SBV b -> SBV c -> [SBool]
steps SBV a
forall a. HasCallStack => a
undefined SBV b
forall a. HasCallStack => a
undefined SBV c
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> SBV b -> SBV c -> [SBool])
-> (SBV a -> SBV b -> SBV c -> SBool)
-> (SBV a -> SBV b -> SBV c -> SBool)
-> SBool
makeInter SBV a -> SBV b -> SBV c -> [SBool]
_ SBV a -> SBV b -> SBV c -> SBool
x SBV a -> SBV b -> SBV c -> SBool
y = (Forall "a" a -> Forall "b" b -> Forall "c" c -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a -> Forall "b" b -> Forall "c" c -> SBool) -> SBool)
-> (Forall "a" a -> Forall "b" b -> Forall "c" c -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) (Forall @"b" SBV b
b) (Forall @"c" SBV c
c) -> SBV a -> SBV b -> SBV c -> SBool
x SBV a
a SBV b
b SBV c
c SBool -> SBool -> SBool
.=> SBV a -> SBV b -> SBV c -> SBool
y SBV a
a SBV b
b SBV c
c

-- | Chaining lemmas that depend on four quantified variables. Overlapping version for 'SBool' that uses implication.
instance {-# OVERLAPPING #-} (SymVal a, SymVal b, SymVal c, SymVal d) => ChainLemma (SBV a -> SBV b -> SBV c -> SBV d -> [SBool]) (SBV a -> SBV b -> SBV c -> SBV d -> SBool) where
   makeSteps :: (SBV a -> SBV b -> SBV c -> SBV d -> [SBool])
-> [SBV a -> SBV b -> SBV c -> SBV d -> SBool]
makeSteps SBV a -> SBV b -> SBV c -> SBV d -> [SBool]
steps = [\SBV a
a SBV b
b SBV c
c SBV d
d -> SBV a -> SBV b -> SBV c -> SBV d -> [SBool]
steps SBV a
a SBV b
b SBV c
c SBV d
d [SBool] -> Int -> SBool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [SBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> SBV b -> SBV c -> SBV d -> [SBool]
steps SBV a
forall a. HasCallStack => a
undefined SBV b
forall a. HasCallStack => a
undefined SBV c
forall a. HasCallStack => a
undefined SBV d
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> SBV b -> SBV c -> SBV d -> [SBool])
-> (SBV a -> SBV b -> SBV c -> SBV d -> SBool)
-> (SBV a -> SBV b -> SBV c -> SBV d -> SBool)
-> SBool
makeInter SBV a -> SBV b -> SBV c -> SBV d -> [SBool]
_ SBV a -> SBV b -> SBV c -> SBV d -> SBool
x SBV a -> SBV b -> SBV c -> SBV d -> SBool
y = (Forall "a" a
 -> Forall "b" b -> Forall "c" c -> Forall "d" d -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a
  -> Forall "b" b -> Forall "c" c -> Forall "d" d -> SBool)
 -> SBool)
-> (Forall "a" a
    -> Forall "b" b -> Forall "c" c -> Forall "d" d -> SBool)
-> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) (Forall @"b" SBV b
b) (Forall @"c" SBV c
c) (Forall @"d" SBV d
d) -> SBV a -> SBV b -> SBV c -> SBV d -> SBool
x SBV a
a SBV b
b SBV c
c SBV d
d SBool -> SBool -> SBool
.=> SBV a -> SBV b -> SBV c -> SBV d -> SBool
y SBV a
a SBV b
b SBV c
c SBV d
d

-- | Chaining lemmas that depend on five quantified variables. Overlapping version for 'SBool' that uses implication.
instance {-# OVERLAPPING #-} (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e) => ChainLemma (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [SBool]) (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool) where
   makeSteps :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [SBool])
-> [SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool]
makeSteps SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [SBool]
steps = [\SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [SBool]
steps SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e [SBool] -> Int -> SBool
forall a. HasCallStack => [a] -> Int -> a
!! Int
i | Int
i <- [Int
0 .. [SBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [SBool]
steps SBV a
forall a. HasCallStack => a
undefined SBV b
forall a. HasCallStack => a
undefined SBV c
forall a. HasCallStack => a
undefined SBV d
forall a. HasCallStack => a
undefined SBV e
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
   makeInter :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [SBool])
-> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool)
-> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool)
-> SBool
makeInter SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> [SBool]
_ SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool
x SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool
y = (Forall "a" a
 -> Forall "b" b
 -> Forall "c" c
 -> Forall "d" d
 -> Forall "e" e
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "a" a
  -> Forall "b" b
  -> Forall "c" c
  -> Forall "d" d
  -> Forall "e" e
  -> SBool)
 -> SBool)
-> (Forall "a" a
    -> Forall "b" b
    -> Forall "c" c
    -> Forall "d" d
    -> Forall "e" e
    -> SBool)
-> SBool
forall a b. (a -> b) -> a -> b
$ \(Forall @"a" SBV a
a) (Forall @"b" SBV b
b) (Forall @"c" SBV c
c) (Forall @"d" SBV d
d) (Forall @"e" SBV e
e) -> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool
x SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e SBool -> SBool -> SBool
.=> SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBool
y SBV a
a SBV b
b SBV c
c SBV d
d SBV e
e