sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.SBV.Tools.NaturalInduction

Description

Proof by induction over naturals.

Synopsis

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

# Documentation

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

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 Source #

Perform natural induction over, using the given solver.