nat.sqrt in lean

Stream: maths

[Anas Himmi]

hi, i'm trying to understand the nat.sqrt function i know what is does but cant' figure out how the algorithm actually works. can someone explain it to me please? here is the code in the library

[Anas Himmi]

theorem sqrt_aux_dec {b} (h : b ≠ 0) : shiftr b 2 < b :=
begin
  simp [shiftr_eq_div_pow],
  apply (nat.div_lt_iff_lt_mul' (dec_trivial : 0 < 4)).2,
  have := nat.mul_lt_mul_of_pos_left
    (dec_trivial : 1 < 4) (nat.pos_of_ne_zero h),
  rwa mul_one at this
end

def sqrt_aux : ℕ → ℕ → ℕ → ℕ
| b r n := if b0 : b = 0 then r else
  let b' := shiftr b 2 in
  have b' < b, from sqrt_aux_dec b0,
  match (n - (r + b : ℕ) : ℤ) with
  | (n' : ℕ) := sqrt_aux b' (div2 r + b) n'
  | _ := sqrt_aux b' (div2 r) n
  end

/-- `sqrt n` is the square root of a natural number `n`. If `n` is not a
  perfect square, it returns the largest `k:ℕ` such that `k*k ≤ n`. -/
def sqrt (n : ℕ) : ℕ :=
match size n with
| 0      := 0
| succ s := sqrt_aux (shiftl 1 (bit0 (div2 s))) 0 n
end

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/noob.20question%28s%29/near/187073046

[Anas Himmi]

thank you!