Zulip Chat Archive

Stream: maths

Topic: nat.sqrt in lean


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 01:10):

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

view this post on Zulip Anas Himmi (Mar 29 2020 at 01:10):

thank you!


Last updated: May 12 2021 at 08:14 UTC