    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tools.NaturalInduction
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Proof by induction over naturals.
    -----------------------------------------------------------------------------

    module Data.SBV.Tools.NaturalInduction (
               inductNat
             , inductNatWith
           ) where

    import Data.SBV
    import Data.SBV.Tuple

    ---------------------------------------------------------------------
    -- * Induction over natural numbers
    ---------------------------------------------------------------------

    -- | Perform natural induction over the given function, which returns left and
    -- right hand-sides to be proven equal. Uses 'defaultSMTCfg'. That is,
    -- given @f x = (lhs x, rhs x)@, we inductively establish that @lhs@ and
    -- @rhs@ agree on @0@, @1@, ... @n@, i.e., for all non-negative integers.
    --
    -- >>> import Data.SBV
    -- >>> import Data.SBV.Tools.NaturalInduction
    -- >>> let sumToN        :: SInteger -> SInteger = smtFunction "sumToN"        $ \x -> ite (x .<= 0) 0 (x   + sumToN        (x-1))
    -- >>> let sumSquaresToN :: SInteger -> SInteger = smtFunction "sumSquaresToN" $ \x -> ite (x .<= 0) 0 (x*x + sumSquaresToN (x-1))
    -- >>> inductNat $ \n -> (sumToN n, (n*(n+1)) `sEDiv` 2)
    -- Q.E.D.
    -- >>> inductNat $ \n -> (sumSquaresToN n, (n*(n+1)*(2*n+1)) `sEDiv` 6)
    -- Q.E.D.
    -- >>> inductNat $ \n -> (sumSquaresToN n, ite (n .== 12) 0 ((n*(n+1)*(2*n+1)) `sEDiv` 6))
    -- Falsifiable. Counter-example:
    --   P(0)   =     (0,0) :: (Integer, Integer)
    --   P(k)   = (506,506) :: (Integer, Integer)
    --   P(k+1) =   (650,0) :: (Integer, Integer)
    --   k      =        11 :: Integer
    inductNat :: SymVal a => (SInteger -> (SBV a, SBV a)) -> IO ThmResult
    inductNat :: forall a. SymVal a => (SInteger -> (SBV a, SBV a)) -> IO ThmResult
    inductNat = SMTConfig -> (SInteger -> (SBV a, SBV a)) -> IO ThmResult
    forall a.
    SymVal a =>
    SMTConfig -> (SInteger -> (SBV a, SBV a)) -> IO ThmResult
    inductNatWith SMTConfig
    defaultSMTCfg

    -- | Perform natural induction over, using the given solver.
    inductNatWith :: SymVal a => SMTConfig -> (SInteger -> (SBV a, SBV a)) -> IO ThmResult
    inductNatWith :: forall a.
    SymVal a =>
    SMTConfig -> (SInteger -> (SBV a, SBV a)) -> IO ThmResult
    inductNatWith SMTConfig
    cfg SInteger -> (SBV a, SBV a)
    p = SMTConfig -> SymbolicT IO SBool -> IO ThmResult
    forall a. Provable a => SMTConfig -> a -> IO ThmResult
    proveWith SMTConfig
    cfg (SymbolicT IO SBool -> IO ThmResult)
    -> SymbolicT IO SBool -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ do
                            SInteger
    k <- String -> Symbolic SInteger
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "k"
                            let at0 :: SBV (a, a)
    at0  = String -> SBV (a, a) -> SBV (a, a)
    forall a. SymVal a => String -> SBV a -> SBV a
    observe String
    "P(0)"   ((SBV a, SBV a) -> SBV (a, a)
    forall tup a. Tuple tup a => a -> SBV tup
    tuple (SInteger -> (SBV a, SBV a)
    p SInteger
    0))
                                atk :: SBV (a, a)
    atk  = String -> SBV (a, a) -> SBV (a, a)
    forall a. SymVal a => String -> SBV a -> SBV a
    observe String
    "P(k)"   ((SBV a, SBV a) -> SBV (a, a)
    forall tup a. Tuple tup a => a -> SBV tup
    tuple (SInteger -> (SBV a, SBV a)
    p SInteger
    k))
                                atk1 :: SBV (a, a)
    atk1 = String -> SBV (a, a) -> SBV (a, a)
    forall a. SymVal a => String -> SBV a -> SBV a
    observe String
    "P(k+1)" ((SBV a, SBV a) -> SBV (a, a)
    forall tup a. Tuple tup a => a -> SBV tup
    tuple (SInteger -> (SBV a, SBV a)
    p (SInteger
    kSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +SInteger
    1)))
                                p0 :: SBool
    p0   = SBV (a, a)
    at0SBV (a, a) -> (SBV (a, a) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, a) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1  SBV a -> SBV a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV (a, a)
    at0SBV (a, a) -> (SBV (a, a) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, a) -> SBV a
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2
                                pk :: SBool
    pk   = SBV (a, a)
    atkSBV (a, a) -> (SBV (a, a) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, a) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1  SBV a -> SBV a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV (a, a)
    atkSBV (a, a) -> (SBV (a, a) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, a) -> SBV a
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2
                                pk1 :: SBool
    pk1  = SBV (a, a)
    atk1SBV (a, a) -> (SBV (a, a) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, a) -> SBV a
    forall b a. HasField "_1" b a => SBV a -> SBV b
    _1 SBV a -> SBV a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBV (a, a)
    atk1SBV (a, a) -> (SBV (a, a) -> SBV a) -> SBV a
    forall a b. a -> (a -> b) -> b
    ^.SBV (a, a) -> SBV a
    forall b a. HasField "_2" b a => SBV a -> SBV b
    _2
                            SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    k SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    0
                            SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain SBool
    pk
                            SBool -> SymbolicT IO SBool
    forall a. a -> SymbolicT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SBool
    p0 SBool -> SBool -> SBool
    .&& SBool
    pk1

    {- HLint ignore module "Redundant ^." -}