Data.SBV.Tools.NaturalInduction

Proof by induction over naturals.

Documentation

inductNat :: SymVal a => (SInteger -> (SBV a, SBV a)) -> IO ThmResult

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

inductNatWith :: SymVal a => SMTConfig -> (SInteger -> (SBV a, SBV a)) -> IO ThmResult

Perform natural induction over, using the given solver.