-----------------------------------------------------------------------------
-- |
-- 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:
--   k      =        11 :: Integer
--   P(0)   =     (0,0) :: (Integer, Integer)
--   P(k)   = (506,506) :: (Integer, Integer)
--   P(k+1) =   (650,0) :: (Integer, 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
                        k <- String -> Symbolic SInteger
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"k"
                        let 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  = 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 = 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   = 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   = 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  = 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
                        constrain $ k .>= 0
                        constrain pk
                        pure $ p0 .&& pk1

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