Computing square roots

Given a natural number x, we want to compute the pair of numbers s and r such that s * s ≤ x < (S+1)*(s+1) and x=s*s+r.

. Let x=4*q+r0 with r<4. If s' and r' are the result for computing the square root of q, then there are two possibilities:
  1. If 4*r'+r0 <4*s'+1 then either s=2s' and r=4r'+r0
  2. Otherwise s=2s'+1 and r=r4'+r0-4s'-1
Build a function with bounded recursion that uses this algorithme to compute the square root. Prove that it is correct and then use it to obtain a function with the following type:
sqrt_nat : forall n:nat,
    {s : nat &  {r : nat | n = s * s + r /\ n < (s + 1) * (s + 1)}}


Follow this link

Going home
Yves Bertot
Last modified: Tue May 20 15:26:16 MEST 2003