English
The square root function on natural numbers is Primrec'.
Русский
Квадратный корень по натуральным числам является Primrec'.
LaTeX
$$$\mathrm{sqrt} : \ Primrec'\ 1\ (fun v => v.head.sqrt)$$$
Lean4
theorem sqrt : @Primrec' 1 fun v => v.head.sqrt :=
by
suffices H : ∀ n : ℕ, n.sqrt = n.rec 0 fun x y => if x.succ < y.succ * y.succ then y else y.succ
by
simp only [H, succ_eq_add_one]
have :=
@prec' 1 _ _
(fun v => by
have x := v.head; have y := v.tail.head
exact if x.succ < y.succ * y.succ then y else y.succ)
head (const 0) ?_
· exact this
have x1 : @Primrec' 3 fun v => v.head.succ := succ.comp₁ _ head
have y1 : @Primrec' 3 fun v => v.tail.head.succ := succ.comp₁ _ (tail head)
exact if_lt x1 (mul.comp₂ _ y1 y1) (tail head) y1
introv ; symm
induction n with
| zero => simp
| succ n IH =>
dsimp; rw [IH]; split_ifs with h
· exact le_antisymm (Nat.sqrt_le_sqrt (Nat.le_succ _)) (Nat.lt_succ_iff.1 <| Nat.sqrt_lt.2 h)
· exact Nat.eq_sqrt.2 ⟨not_lt.1 h, Nat.sqrt_lt.1 <| Nat.lt_succ_iff.2 <| Nat.sqrt_succ_le_succ_sqrt _⟩
