# Zulip Chat Archive

## 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

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

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 `def`

s 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