How to get Lean to calculate square roots

Stream: new members

[Leo Shine]

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]

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

[Leo Shine]

Thanks

[Kevin Buzzard]

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

[Leo Shine]

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]

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]

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

[Leo Shine]

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]

This theorem will not be applicable to the real numbers.

[Kevin Buzzard]

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]

Here's a proof of your sorry:

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
  unfold quadrootplus quadrootminus -- these should never have been defs; make them `abbrev`s and then you can skip this line
  intro x
  ring_nf
  -- we didn't unfold `quaddisc` so we can now use this
  rw [hcansqrt]
  field_simp
  ring

[Leo Shine]

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]

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]

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_.)