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

Remi Turk buran at xs4all.nl
Fri Aug 13 04:50:16 EDT 2004

```On Fri, Aug 13, 2004 at 10:23:36AM +0200, Henning Thielemann wrote:
> On Thu, 12 Aug 2004, Remi Turk wrote:
> > On Thu, Aug 12, 2004 at 09:01:03PM +0200, Henning Thielemann wrote:
> > > 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"
Correct.
Though I consider the version below to be quite readable, and I
don't see how to check for "factor > n `div` factor" without
uglifying the implementation. (for merely a constant-time win.)

> > 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.

what I was originally typing...
] fromIntegral doesn't round, it'll have a type like Integer -> Double
] floor rounds down, and AFAICS that can't give wrong results as
] for all x: (intSqrt n + 1) ^ 2 > n
] Although intSqrt might be better renamed as floorSqrt.

Of course, it should really be
] for all x: (intSqrt n + 1) * 2 > n
which is plain wrong, so I guess you're just completely correct
and it should be:
ceilSqrt = ceiling . sqrt . fromIntegral

And this is all getting rather off-topic I'm afraid ;)

Greetings,
Remi

--
Nobody can be exactly like me. Even I have trouble doing it.
```