Should these surds be simplified with norm_num?

Stream: mathlib4

[Mr Proof]

I'm playing around with norm_num to see what it can do. It feels like there is a gap in it's knowledge when it comes to square roots. Here's my results:

import Mathlib

def q0: (2:Real)/3 = (4:Real)/6 := by norm_num /-works-/
def q1: ((√3)^2=3) := by norm_num /-works-/

def q2: (√9=3) := by norm_num /-doesn't work-/
def q3: (2*√3)^2 = 12 := by norm_num /-doesn't work (use ring_nf;simp;ring_nf)-/
def q4: ((3:Real)^((1:Real)/7))^7 = 3 := by norm_num /-doesn't work-/
def q5: ((3:Real)^7)^((1:Real)/7) = 3 := by norm_num /-doesn't work-/
def q6: ((√3)^3=3*√3) := by norm_num /- doesn't work-/
def q7: ((√3)^3=√27) := by norm_num /- doesn't work-/
def q8: ((√3+1)^2=2*√3+4) := by norm_num /- doesn't work (use ring_nf;simp;ring_nf)-/
def q9: √2 * √3 = √6 := by norm_num /- doesn't work (use  rw [<-Real.sqrt_mul];ring_nf;simp)-/
def q10: 1/√3 = √3/3 := by norm_num /- doesn't work-/

def q11: (1:Real)/2 - (1:Real)/3 = (1:Real)/6 := by norm_num /-works-/
def q12: 2^100000000/2^99999999 = 2:= by norm_num /-works (slowly - probably not using the easy method)-/

def q13: √3 < 2 :=by norm_num /- doesn't work-/

def q14: √3 < √4 :=by norm_num /- works -/
def q15: √3+1 < √3+2 :=by norm_num /- works -/
def q16: 2*√3 < 5*√3 :=by norm_num /- works -/

def q17: √3+1 < 2+√3  :=by norm_num; linarith /-works when include linarith -/

Do you think these should work with norm_num? Also q12 works but it is very slow suggesting it is not simplifying it using the easy shortcut of subtracting exponents.

[Eric Wieser]

norm_num unfortunately doesn't support surds, and making it do so (except in the case where the evaluation of the surd is rational) would be a substantial refactor

[Mr Proof]

It does support one case e.g sqrt(3)^2=3

Perhaps it should support (2*sqrt(3))^2=18 since that gives a rational?

[Eric Wieser]

I think that's just using simp

[Kyle Miller]

The concept of norm_num is to normalize numbers, and the only normal forms it has are natural number, integer, and rational number literals (as well as boolean literals to be able to decide certain properties, like Nat.Prime). These are all chosen to be data types that have an efficient run-time representation, since norm_num does computations using normalized numbers when generating its proofs.

If norm_num were to support surd expressions as well, then it would need a specification for a normal form for them, as well as an efficient way to calculate with them. At that point, it seems like working with general algebraic numbers (i.e., roots of arbitrary polynomials) would be the way to go, but that is much more complicated, and I'm not sure how that works for general rings. The norm_num tactic isn't only for Nat/Int/Rat/Real/Complex after all.

[Kyle Miller]

It makes sense that the following is slow, since norm_num works by recursively normalizing numbers. It will not use any global structure of an expression during its normalization.

def q12: 2^100000000/2^99999999 = 2:= by norm_num

Note that norm_num also interleaves simp, which can make understanding the capabilities of norm_num itself somewhat confusing. You can use the norm_num only tactic to make it not apply any simp lemmas.

[Mr Proof]

I see.
Still, I think it is missing a few cases where the answer is an integer.
But I see the problem.
In the case of where there is no nesting I don't think the normal form wouldn't be too hard? Just take all squares to the outside so you'd end up with a+b√2+c√3+d√5+e√6+f√7+g√11+... in that order.
But I can see that implementing that in Lean is probably very difficult.

Yes, for the q12, Mathematica does the same thing! Even though it should know better. Sometimes humans are just better I suppose.

Mind you, Chat GPT can solve that equation and it uses the exponent rule!

[Kyle Miller]

I think it is missing a few cases where the answer is an integer.

It's not a matter of whether the answer is an integer, but whether all the intermediate expressions have a normal form. It's possible to add new rules, but I think the design of norm_num is that it's only supposed to worry about normalized values. Making a rule about squaring a product of square roots isn't in norm_num's wheelhouse.

[Kyle Miller]

a+b√2+c√3+d√5+e√6+f√7+g√11+...

Then what happens if you take a square root of that? Should norm_num fail? Or do you use a more complicated representation?

[Kyle Miller]

Sometimes humans are just better I suppose.

Just because norm_num doesn't do it doesn't mean that you can't make a tactic that tries to be smart about simplifying. That said, a risk with adding too many rules is that, while they might make some things fast, they might slow the common case down, since it'll spend so much time trying to be smart rather than doing the arithmetic, which computers are good at.

By the way, it turns out that q12 is solved almost immediately by simp. It uses some faster proof-generating evaluation procedures I guess (docs#Nat.reducePow and docs#Nat.reduceDiv), which were added recently with the simprocs feature.

[Mr Proof]

I would imagine if we had sqrt(4*sqrt(3)+7) = 2+sqrt(3) it would be able to work out the RHS is positive and square both sides to get the answer. It never has to take any actual square roots. If the examples were more complicated it could just fail.

I'll look more into simp, that seems to be very good.

[Kyle Miller]

You could write a simproc to reduce √n where n is a non-square-free natural number.

[Kyle Miller]

it would be able to work out the RHS is positive and square both sides to get the answer

That's out of scope for norm_num, whose strategy for x = y is to normalize x and y and see that both sides are the same.

[Kyle Miller]

Here's a simproc for normalizing Real.sqrt of a natural number. Example:

#simp √12
-- 2 * √3

import Mathlib

open Lean Meta

theorem sqrt_reduce (nsqrt n' : Nat) : √(Nat.cast (nsqrt ^ 2 * n')) = nsqrt * √n' := by
  simp

simproc reduceSqrt (Real.sqrt _) := fun e => do
  let some (n, Rty) ← getOfNatValue? e.appArg! ``Real | return .continue
  if n == 0 || n == 1 || Squarefree n then return .continue
  let mut nsqrt := 1
  let mut n' := 1
  let mut n'' := n
  for p in Nat.factors n do
    let mut multiplicity := 0
    while n'' % p == 0 do
      n'' := n'' / p
      multiplicity := multiplicity + 1
    nsqrt := nsqrt * p ^ (multiplicity / 2)
    n' := n' * p ^ (multiplicity % 2)
  -- now `n'` is squarefree and `n = nsqrt^2 * n'`.
  -- pf1 is `OfNat.ofNat n = Nat.cast n`
  let pf1 ← mkEqSymm (← mkAppOptM ``Nat.cast_eq_ofNat #[Rty, toExpr n, none, none])
  -- pf2 is `√(OfNat.ofNat n) = √(Nat.cast n)`
  let pf2 ← mkCongrArg (.const ``Real.sqrt []) pf1
  -- pf3 is `√(Nat.cast (nsqrt ^ 2 * n')) = nsqrt * √n'`
  let pf3 ← mkAppM ``sqrt_reduce #[toExpr nsqrt, toExpr n']
  -- pf4 is `√(OfNat.ofNat n) = nsqrt * √n'`
  let pf4 ← mkEqTrans pf2 pf3
  let some (_, _, rhs) := (← inferType pf4).eq? | return .continue -- should not fail
  return .visit { expr := rhs, proof? := pf4 }

example : √12 = 2 * √3 := by simp

[Michael Stoll]

docs#Nat.sq_mul_squarefree should help with simplifying this.

[Kyle Miller]

@Michael Stoll Unless there's some trick I'm missing, that's just a theorem that numbers exist, not what the numbers are.

[Kyle Miller]

If Lean were more constructive, we could reduce the proof and extract the witnesses. Barring that, a more useful way to state that theorem would be with subtypes, since it would give the data of what exists.

[Michael Stoll]

You're right; I was missing that one actually needs the witnesses.
I guess it would make sense to add a function that produces the squarefree factorization of a natural number (in a computable way).

[Mr Proof]

@Kyle Miller

Combining your simplification function with linarith I can do easily:

example :  9 + √12 +   5 * √3  + √8 + √18 = 5 * √2 + 7 * √3  + 9:= by simp; linarith

That's pretty nice. :grinning: Not sure how many steps it would take without that function. (BTW putting the left hand side into Maxima automatically converts it to the RHS). Makes me wonder if simp should always call linarith at the end.

Some things that might be low hanging fruit: (These are two things Maxima does automatically)

• norm_num could order terms in sums in some kind of consistent order (alphabetical?) e.g. 2+√3 vs √3 +2 (this may be covered by linarith)
• As well as taking out squares a useful function would also be to automatically combine square roots e.g. √3 *√3 *√5 *√7 = 3 * √35. (Of course it is a matter of taste whether √5 *√7 or √35 is the "correct" normal form, but maxima goes with the second choice.)

These are just some ideas. When I get better at Lean hopefully I'll be able to write functions for these myself.

[Kyle Miller]

Again, norm_num isn't that sort of tactic (it's for evaluating numbers, not normalizing algebraic expressions), but these are certainly things that a tactic could do.

By the way, you can use ring in place of linarith for that. There's also ring_nf for putting sum/product expressions into a normal form.

[Mr Proof]

Thanks. I like to explore the edge cases so I know what lean can do. (Yes ring_nf is what I was looking for to expand out expressions!) I got another conundrum:

example: (√3+2)^2 =  4 + (√3)^2 + 4 * √3  := by ring_nf /-works-/

example: (√3)^2  = 3 := by simp /-works-/

example: (√3+2)^2 =  7 + 4 * √3  := by ring_nf;simp /-doesn't work-/

I kind of feel like the third example should work. But it doesn't understand example: (√3)^2+ 1 = 4 := by simp for example fails. i.e. it doesn't simplify the square of a square-root when it's in the middle of an expression :worried:

[Kyle Miller]

I was mostly responding to the "low-hanging fruit" comment. If you're not careful, it's tempting to make every tactic a full general theorem prover!

[Kyle Miller]

For your examples, do simp first before ring

[Mr Proof]

That true .:grinning_face_with_smiling_eyes:. For my the low hanging fruit comment, that is mostly about expressions you can type into maxima that automatically get put in a normal form.

Aha! Success! Just had to call it twice on the second example:

example: 1+(√3)^2=4 := by simp;ring_nf

example: (√3+2)^2 =  7 + 4 * √3  := by ring_nf;simp;ring_nf

Wonder if it's possible to write a meta-tactic that alternately calls simp and ring_nf until it can't simplify any more. Assuming that wouldn't loop forever. I would call it ring_simp

My final challenge for today:

example: (√3+√2)^2 =  5 + 2*√6 := by ring_nf;simp;ring_nf;simp

The final unsolved goal is: √3 * √2 = √6

[Kyle Miller]

maxima

I've wanted to make a mathematica/maxima-style evaluator tactic before, along with a suite of tactics like collect/expand/etc. I've written this sort of thing in Python before, but the fun of tactics is that in addition to doing the manipulations you need to generate proofs that the manipulations are correct.

Since you have this CAS background, I suppose it's worth mentioning that simp has very little in common with Simplify[...], confusingly. The simp tactic is more like //. (ReplaceRepeated[...]) with a list of global rewrite rules. And, as you can see, with simprocs they can be programmatic rewrite rules. So, while it might be called "simplify", it's only a simplification if the set of rewrite rules is constructed suitably.

[Mr Proof]

Yes, I actually think it's a good idea to mirror CAS type behaviour in Lean, since then you could use it like a CAS and have it prove all your steps as you go along. I think it would make it more accessible.

OK solved my last problem for today. But it's not pretty:

example: (√3+√2)^2 =  5 + 2*√6 := by ring_nf;simp;rw [<-Real.sqrt_mul];ring_nf;simp

[Kim Morrison]

Kyle Miller said:

simp has very little in common with Simplify[...], confusingly

@Kyle Miller, I agree with your analogy with ReplaceRepeated. Is there any public description of what Simplify is actually doing? Despite at times knowing a lot about Mathematica internals, this was always a black box to me.

[Kyle Miller]

All I know is that it tries transforming the expression using many different approaches and then returns the simplest one according to some complexity measure. You can set the transformers using the TransformationFunctions and the complexity measure using the ComplexityFunction options.

[Kyle Miller]

Hmm... looking into it more, it seems that Simplify/FullSimplify is also like ReplaceRepeated, but it nondeterministically does transformations and returns the simplest one it comes across. The thing I couldn't find is how it determines how long to try to simplify, or if there are heuristics on how complicated it's willing to make an expression.