Simplifying `0 < a * b` etc

Stream: maths

[Yury G. Kudryashov]

I'm going to add lemmas simplifying 0 < a * b to 0 < a ∧0 < b ∨ a < 0 ∧ b < 0, and similarly for other inequalities. Please respond here if you have any objections.

[Yury G. Kudryashov]

(and similarly for 0 < a / b)

[Johan Commelin]

@Yury G. Kudryashov will they be in the default simp set?

[Johan Commelin]

I'm not sure I like that idea... (but maybe I can get used to it)

[Yury G. Kudryashov]

Yes, I was going to add them to the default simp set. My argument is that the inequalities become simpler, and Lean can simp out bad cases.

[Yury G. Kudryashov]

Created #4359. Let's see if the proofs outside of algebra/ordered* become harder or easier.

[Reid Barton]

Is it true that when simp would make further progress, it could also use a lemma like ... (h : 0 < a) : 0 < a * b <-> 0 < b?

[Yury G. Kudryashov]

Currently I use simp [h.not_lt].

[Yury G. Kudryashov]

I definitely want these lemmas but I don't insist on tagging them with @[simp]. We can always drop this part of the PR.

[Yury G. Kudryashov]

#4359 is ready for review.

[Chris Hughes]

Would it be a good idea to have simp lemmas like (h : a < b) : b < a <-> false?

[Yury G. Kudryashov]

How deep will simp go while searching for h : a < b? Will it create a loop?

[Yury G. Kudryashov]

I mean, it would be nice to have simp add a ≤ b, ¬(b < a), ¬(b ≤ a) whenever it has a < b but I don't know how much will it slow down simp.

[Johan Commelin]

@Yury G. Kudryashov The diff is much smaller than I expected :smiley:
@Mario Carneiro @Gabriel Ebner are these simp lemmas a good idea?

[Mario Carneiro]

I don't know, my thought is the same as Yury's

[Mario Carneiro]

you probably have to test to find out

[Gabriel Ebner]

I don't think these are good simp lemmas. What happens if somebody calls simp on 0 < a*b*c*d*e*f*h?
In general I'm skeptical of conditional simp lemmas (they cause invisible search and it's hard to figure out what extra lemmas you need to add to trigger them), but in this case Reid's proposal looks like the lesser evil.

[Johan Commelin]

Which proposal by Reid are you referring to? @Gabriel Ebner

[Gabriel Ebner]

The only message Reid posted in this thread:

use a lemma like ... (h : 0 < a) : 0 < a * b <-> 0 < b

[Johan Commelin]

Oops, I didn't scroll back enough... stupid tiny screens :face_palm:

[Yury G. Kudryashov]

But what if a < 0, b < 0?

[Gabriel Ebner]

You need 2*2 simp lemmas.

[Yury G. Kudryashov]

But in the case 0 < a * b * c * d this will create a huge search.

[Yury G. Kudryashov]

And what about 0 ≤ a * b? My PR simplifies it to a formula with non-strict inequalities.

[Gabriel Ebner]

Yury G. Kudryashov said:

But in the case 0 < a * b * c * d this will create a huge search.

The simp lemmas in #4359 will make this formula exponentially larger.
Reid's proposal would only call the simplifier on 0 < a, a < 0, 0 < a*b, a*b < 0, 0 < a*b*c, a*b*c < 0, 0 < a*b*c*d, and a*b*c*d < 0 (as well as the subterms 0, a, b, c, d, a*b, a*b*c, and a*b*c*d).

[Gabriel Ebner]

Note that there is caching.

[Gabriel Ebner]

Yury G. Kudryashov said:

And what about 0 ≤ a * b? My PR simplifies it to a formula with non-strict inequalities.

mul_nonneg_iff rewrites one non-strict ≤ to four non-strict ≤, am I missing something?

[Yury G. Kudryashov]

Yes (with the hope that some of those 4 inequalities can be simplified to true or false.

[Yury G. Kudryashov]

OK, let me remove @[simp] from these lemmas.

[Yury G. Kudryashov]

I'll just add them to simp calls explicitly.

[Yury G. Kudryashov]

We can decide whether to add the conditional iffs to @[simp] later.

[Yury G. Kudryashov]

Done, fixed build failures. #4359 is ready for review