Computing square roots (with well-founded recursion)

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 r0<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 s=2s' and r=4r'+r0
  2. Otherwise s=2s'+1 and r=r4'+r0-4s'-1
Build a function that uses this algorithm to compute the square root and is based on well-founded recursion. This function should have the following type. 
sqrt_nat : forall n:nat,
    {s : nat &  {r : nat | n = s * s + r /\ n < (s + 1) * (s + 1)}}

Solutions

  1. Follow this link
  2. An improvement by Ghas Shee, which allows to compute square roots within Coq (with Compute)


Yves Bertot
Last modified: Tue Jul 20 17:30:00 CEST 2022