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)}}

Solution

Follow this link

Yves Bertot
Last modified: Sun May 3 13:54:37 CEST 2015