## Stream: new members

### Topic: How to get Lean to calculate square roots

#### Leo Shine (Oct 30 2023 at 16:35):

I created a version of the quadratic formula using Lean and I'm trying to use it but, when it gets to the point of using it, I seem to have to manually tell it that (9:ℝ) = 3 *3 am I missing something that makes this sort of calculation happen automatically

MWE below

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic

theorem quadFormula {F : Type*} [Field F] (b c: F) ( hnotorder2: 2 ≠ (0:F)) (asqrt:F→ F)
(hcansqrt: (asqrt (b^2 - 4 * c) ) ^ 2 = b^2 - 4*c ) : ∀ x:F, x^2 + b*x + c = (x - (-b + asqrt (b^2 - 4 * c)) /2) * (x - (-b - asqrt (b^2 - 4 * c)) /2)
:= sorry

example: ∀x:ℝ, x^2 + 5* x + 4 = (x+4) * (x + 1) :=
by
intro x
rw [quadFormula 5 4 _ Real.sqrt _]
norm_num
have : (9:ℝ) = 3 *3 := by norm_num
rw[this]
norm_num
ring
repeat norm_num


#### Ruben Van de Velde (Oct 30 2023 at 16:38):

No, I don't think you're missing anything

Thanks

#### Kevin Buzzard (Oct 30 2023 at 17:00):

example: ∀x:ℝ, x^2 + 5* x + 4 = (x+4) * (x + 1) := by
intro x
ring


#### Leo Shine (Oct 30 2023 at 17:06):

Haha yes, but I was trying to see what it was like to try to use my version of the quadratic formula, I guess the fact that ring is so powerful might be why this doesn't matter that much in practice

#### Kevin Buzzard (Oct 30 2023 at 17:08):

Right -- instead of doing what you're doing the way you're doing it, you could make two functions plusroot and minusroot which give you the two roots with the + and - sign on the sqrt, and then prove that your quadratic factors as (x-plusroot)(x-minusroot). Then it would not be possible to use ring.

#### Kevin Buzzard (Oct 30 2023 at 17:09):

The functions wouldn't need to assume b^2-4ac>=0, but this assumption would be in the theorem.

#### Leo Shine (Oct 30 2023 at 17:25):

Like this?

import Mathlib.Algebra.BigOperators.Ring
import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic

def quaddisc {F : Type*} [Field F] (b c: F) := b^2 - 4 * c
def quadrootplus {F : Type*} [Field F] (b c: F) (asqrt:F→ F) :=
(-b + asqrt (quaddisc b c)) /2
def quadrootminus {F : Type*} [Field F] (b c: F) (asqrt:F→ F) :=
(-b - asqrt (quaddisc b c)) /2

theorem quadFormula {F : Type*} [Field F] (b c: F) ( hnotchar2: 2 ≠ (0:F)) (asqrt:F→ F)
(hcansqrt: asqrt (quaddisc b c ) ^ 2 = b^2 - 4*c ) : ∀ x:F, x^2 + b*x + c = (x - (quadrootplus b c asqrt) ) * (x - (quadrootminus b c asqrt))
:= by
sorry


#### Kevin Buzzard (Oct 30 2023 at 19:59):

This theorem will not be applicable to the real numbers.

#### Kevin Buzzard (Oct 30 2023 at 20:03):

Oh OK, more precisely I mean that if you feed in numbers where disc<0 then you can't fill in an input proof, but maybe that's what you want.

#### Kevin Buzzard (Oct 30 2023 at 20:20):

Here's a proof of your sorry:

#### Leo Shine (Oct 30 2023 at 21:24):

Ah cool that's a lot simpler than my one (for example doesn't need to prove facts like 4 != 0) and I didn't know about abbrev's

#### Kevin Buzzard (Oct 31 2023 at 13:11):

Lean does not unfold defs by default, whereas for your two roots you want them to be printed as quadrootplus and quadrootminus so you don't have to have the formula leaking out everywhere in your goals and hypotheses, however you really want the computer to just see the underlying definitions, so then you don't have to keep telling it to unfold them. And this is what abbrev does. It's taking advantage of the subtle difference between "what the computer tells you it's looking at" and "what the computer is actually looking at".

#### Kevin Buzzard (Oct 31 2023 at 13:12):

Leo Shine said:

Ah cool that's a lot simpler than my one (for example doesn't need to prove facts like 4 != 0) and I didn't know about abbrev's

Of course I _did_ need to prove 4!=0 somehow, but I let field_simp do it for me (that tactic knows that product of nonzero things is nonzero; I didn't actually prove 4!=0, I proved that 2*2!=0, which is the same _numbers_ but a different _term_.)

Last updated: Dec 20 2023 at 11:08 UTC