## Stream: maths

### Topic: nat.sqrt in lean

#### Anas Himmi (Mar 29 2020 at 01:03):

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 (Mar 29 2020 at 01:04):

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


#### Anas Himmi (Mar 29 2020 at 01:10):

thank you!

Last updated: May 12 2021 at 08:14 UTC