[Haskell-cafe] puzzle: prove this floorSqrt correct

[Henning Thielemann]

On Thu, 12 Aug 2004, Remi Turk wrote:

> On Thu, Aug 12, 2004 at 09:01:03PM +0200, Henning Thielemann wrote:
> > 
> > On Thu, 12 Aug 2004, Remi Turk wrote:
> > > I usually (each time I urgently need to calculate primes ;)) use
> > > a simple intSqrt = floor . sqrt . fromIntegral
> > > (which will indeed give wrong answers for big numbers)
> > 
> > If I urgently need factors of an integer I check "factor*factor > n"
> > rather than "factor > intSqrt n". :-]
> 
> but you'll have to (^2) once every "iteration".
> The following code only has to sqrt once.

Right. Hm, but if you get a 'div' for free for every 'mod' (e.g. divMod)
you could also check "factor > n `div` factor" 

> Oh, the joy of premature optimization. Or even premature coding ;)
> 
> -- Will lie when given stupid questions
> isPrime 1   = False
> isPrime 2   = True
> isPrime n   = not $ any (n`isDivBy`) (2:[3,5..intSqrt n])
>     where
>         n `isDivBy` d   = n `rem` d == 0
>         intSqrt         = floor . sqrt . fromIntegral

If the numbers become too big, will 'fromIntegral' round down or up? If it
rounds down, then intSqrt might lead to a too small result.