derivative.hs

import Data.SBV

-- An attempt to prove that the derivative of x^2 is 2x, using the
-- epsilon-delta definition of limit (http://en.wikipedia.org/wiki/(%CE%B5,_%CE%B4)-definition_of_limit)
-- inspired by: http://stackoverflow.com/questions/16367703/using-z3py-online-to-prove-that-the-derivative-of-x2-is-2x
-- That is, we try to prove:
--   forall x. forall epsilon>0. exists delta>0. forall d.
--        (0 < abs d < delta ==> abs (((x+d)^2 - x^2) / d - 2x) < epsilon)
-- Alas, z3 returns unknown; which is not very surprising due to the need for quantifiers.
dx2 :: IO ThmResult
dx2 = prove $ do x       <- forall "x"
                 epsilon <- forall "epsilon"
                 delta   <- exists "delta"
                 d       <- forall "d"
                 constrain $ epsilon .> 0
                 let range = 0 .< abs d &&& abs d .< delta
                     limit = (f (x+d) - f x) / d - f' x
                 return $ delta .> 0 &&& (range ==> abs limit .< epsilon)
  where f, f' :: SReal -> SReal
        f  x = x*x
        f' x = 2*x