proof help

Stream: new members

[Devan Srinivasan]

I am very new to lean and very sorry if these are dumb questions. A deadline is swiftly approaching and I can't seem to crack this. I was wondering if any lean folks could help me better understand how to go about simplifying algebra.

for starters, why does this work?
example (x0: ℝ): x0^(3/2) = x0 := by simp
and how would i go about simplifying general algebra like x * sqrt(x) to x^(3/2). In larger expressions I sometimes have something like ( (...) * A ) / A yet the A's don't cancel out (I have hypothesis that A != 0). What should I do & where should I look? I did a little bit of natural number game but the ideas aren't extending well to my calculus proofs with real numbers. i looked at the auto generated docs, but couldn't find anything super helpful.

[Aaron Liu]

Devan Srinivasan said:

for starters, why does this work?
example (x0: ℝ): x0^(3/2) = x0 := by simp

It's natural number division, which rounds down.

[Aaron Liu]

3 / 2 = 1

[Aaron Liu]

You can use #loogle and #leansearch and other tools to help you find theorems. You can also try looking it up in the #docs or guessing the name of the theorem based on mathlib's #naming conventions.

[Devan Srinivasan]

I see...ok thank you so much this is very helpful.

[Devan Srinivasan]

Ok so in general, if I have like a * b * c / a, i would have to use some combination of associativity with multiplication and cancellation rule to simplify that right? there isn't just one tactic I can use to reduce expressions as much as possible?

[Aaron Liu]

The example you gave is docs#mul_div_cancel_right₀

[Aaron Liu]

Devan Srinivasan said:

Ok so in general, if I have like a * b * c / , i would have to use some combination of associativity with multiplication and cancellation rule to simplify that right? there isn't just one tactic I can use to reduce expressions as much as possible?

simp is close, but uses a somewhat conservative interpretation of "simple"

[Aaron Liu]

You can also give it your own theorems, like simp [← mul_assoc]

[Devan Srinivasan]

right ok. thank you very much Aaron!

[Maja Kądziołka]

some combo of field_simp and ring should handle the generalized "just do algebra to this"

[Michael Rothgang]

... except if you work with NNReal or ENNReal: these are not a field, and for them you need usually need to apply lemmas by hand.

[Yaël Dillies]

NNReal is a semifield, though. field_simp should handle it, no? I agree ENNReal is a different beast

[Michael Rothgang]

I haven't tried NNReal much - so my comment here may be wrong.

[Devan Srinivasan]

unless I am using them wrong, just typing
ring and field_simp [...] where ... is sometimes some hypothesis that denom != 0, it rarely simplifies all the way. almost always have to manually apply lemmas now

field_simp does however usually simplify the work I have to do, but never finish it :(

[Kevin Buzzard]

Can you show us a #mwe example where these tactics are not doing as much as you would hope?

[Devan Srinivasan]

sure. in proving that this derivative: ln(x0 + sqrt(x0^2 + 1)) = 1/sqrt(x0^2 + 1)
after applying differentiation rules, and applying field_simp all that remains is to prove:
⊢ (2 * √(x0 ^ 2 + 1) + 2 * x0) * √(x0 ^ 2 + 1) / ((x0 + √(x0 ^ 2 + 1)) * (2 * √(x0 ^ 2 + 1))) = 1

i know this looks gross, but it is just:
[(2A + 2x)(A)] / [(x+A)(2A)] = 1 where A = √(x0^2 + 1) which is trivial to prove (factor out 2 in numerator and cancel everything)

ring does not work, but it does work when I add the hypothesis that x0 > 0. x0 is a real number. I have not really studied abstract algebra -- but from what I briefly researched, are the reals not a semiring? why doesn't ring work here? the denominator can never be zero anyways either.

also idk how minimal this example is, but it was the simplest I have in my problem set.

[Aaron Liu]

The problem might be that 0 / 0 = 0

[Devan Srinivasan]

Ok I have found a simpler example without division:
example (x0: ℝ): (√(1 - x0) * (2 * √x0)) = (2 * √(x0 - x0 ^ 2)) := by sorry
to prove something like this would I have to do the factoring and all by myself? I am entirely fine if the answer is yes (and expect it is) but just want to make sure I am using the best tactics where available :D

[Devan Srinivasan]

sorry Aaron to , how could a 0/0 occur in the first example?

[Kevin Buzzard]

A #mwe is fully-compiling code in triple-backticks where I can just click the button and the code opens in a website and works first time.

[Kevin Buzzard]

Like this

import Mathlib

example (x0: ℝ): (√(1 - x0) * (2 * √x0)) = (2 * √(x0 - x0 ^ 2)) := by
  sorry

That's the best way to ask a question here :-)

[Kevin Buzzard]

yeah, field_simp and ring won't do that because square roots are not in their remit. Here you have to apply lemmas.

[Devan Srinivasan]

sorry, i didn't read the #mwe page fully that is my bad. here you go:

import Mathlib

example (x0 : ℝ) : √(1 - x0) * (2 * √x0) = 2 * √(x0 - x0 ^ 2) := by
  sorry

example (x0 : ℝ): (2 * √(x0 + 1) + 2 * x0) * √(x0 + 1) / ((x0 + √(x0 + 1)) * (2 * √(x0 + 1))) = 1 := by
  sorry

how would I go about proving either of these?

[Devan Srinivasan]

oh i missed your last reply. Ok thanks, so lemmas it is!

[Kevin Buzzard]

Are you sure these theorems are correct when 1 - x0 < 0 or x0 < 0? the square root of a negative number is undefined mathematically so will be "random" in Lean, and you didn't put any bounds on x0

[Aaron Liu]

The first one is always true, because mathlib chose the default value of 0 for the square root of a negative.

The second one is false, becuase for x0 ≤ -1 you get 0 / 0 = 1 (but it is true if you assume -1 < x0 ∧ x0 ≠ (1 - √5) / 2)

[Devan Srinivasan]

you're both right, those were examples I quickly concocted to try and keep it simpler. they are indeed not correct without bounds. my original problem remains proving:

import Mathlib
example (x0: ℝ): (2 * √(x0 ^ 2 + 1) + 2 * x0) * √(x0 ^ 2 + 1) / ((x0 + √(x0 ^ 2 + 1)) * (2 * √(x0 ^ 2 + 1))) = 1 := by sorry

i believe this equality is always true yet ring does not simplify. I suppose some of my problems stem from lack of precision in my formalization work.

[Aaron Liu]

ring only works on statements true in any commutative ring, so it doesn't know about square roots, which are specific to the real numbers.

[Devan Srinivasan]

ok. so to prove this is what Kevin was previously addressing, I'd have to rearrange term by term then apply some cancellation lemmas right?

[Aaron Liu]

You can leave the term-rearranging to ring, and just specify what you want it to rearrange to.

[Aaron Liu]

example:

import Mathlib

example (x0: ℝ): (√(1 - x0) * (2 * √x0)) = (2 * √(x0 - x0 ^ 2)) := calc
  _ = 2 * (√(x0) * √(1-x0)) := by ring
  _ = 2 * √(x0*(1-x0)) := by
    obtain hx0 | hx0 := le_total x0 0
    · have : x0 * (1 - x0) ≤ 0 :=
        mul_nonpos_of_nonpos_of_nonneg hx0 (by linarith)
      simp [Real.sqrt_eq_zero_of_nonpos, hx0, this]
    · rw [Real.sqrt_mul hx0]
  _ = _ := by ring_nf

[Devan Srinivasan]

woah ok I did not know i can do that...super helpful!

[Maja Kądziołka]

does ring handle rpow, maybe? I think I remember having some success with it but maybe that was normal pow, with natural exponent

[Kevin Buzzard]

I think only natural powers. A more general power is not a ring operation (i.e would not make sense for a general commutative ring, which is what the tactic deals with).

[Notification Bot]

This topic was moved here from #mathlib4 > proof help by Patrick Massot.