[Haskell-cafe] puzzle: prove this floorSqrt correct

[Christian Sievers]

blaetterrascheln at web.de wrote:

> -- Here's the discrete version of Newton's method for finding
> -- the square root.  Does it always work?  Any literature?

I recently used, without range check,

sqrtInt n = help n where
            help x = let y = ((x + (n `div` x)) `div` 2)
                     in if y<x then help y else x

following p. 38f of Henri Cohen, A Course in Computational Algebraic Number
Theory, where a proof and a suggestion for improvement (choose a better start
value) is given.
Your version should be correct as well.

As far as I know, ghc uses gmp, so I wonder if there is access to functions
like mpz_sqrt or mpz_perfect_square_p.


All the best
Christian Sievers