Re: [Haskell-cafe] puzzle: prove this floorSqrt correct

blaetterrascheln@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