## Stream: maths

### Topic: Simplifying 0 < a * b etc

#### Yury G. Kudryashov (Oct 01 2020 at 18:40):

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 (Oct 01 2020 at 18:40):

(and similarly for 0 < a / b)

#### Johan Commelin (Oct 01 2020 at 21:32):

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

#### Johan Commelin (Oct 01 2020 at 21:32):

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

#### Yury G. Kudryashov (Oct 01 2020 at 22:42):

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 (Oct 02 2020 at 01:36):

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

#### Reid Barton (Oct 02 2020 at 01:38):

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 (Oct 02 2020 at 01:45):

Currently I use simp [h.not_lt].

#### Yury G. Kudryashov (Oct 02 2020 at 01:52):

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

#### Chris Hughes (Oct 02 2020 at 04:24):

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

#### Yury G. Kudryashov (Oct 02 2020 at 05:27):

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

#### Yury G. Kudryashov (Oct 02 2020 at 05:29):

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 (Oct 02 2020 at 06:01):

@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 (Oct 02 2020 at 06:01):

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

#### Mario Carneiro (Oct 02 2020 at 06:02):

you probably have to test to find out

#### Gabriel Ebner (Oct 02 2020 at 08:03):

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 (Oct 02 2020 at 08:29):

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

#### Gabriel Ebner (Oct 02 2020 at 08:31):

The only message Reid posted in this thread:

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

#### Johan Commelin (Oct 02 2020 at 08:32):

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

#### Yury G. Kudryashov (Oct 02 2020 at 12:14):

But what if a < 0, b < 0?

#### Gabriel Ebner (Oct 02 2020 at 12:15):

You need 2*2 simp lemmas.

#### Yury G. Kudryashov (Oct 02 2020 at 12:18):

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

#### Yury G. Kudryashov (Oct 02 2020 at 12:19):

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

#### Gabriel Ebner (Oct 02 2020 at 12:25):

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 (Oct 02 2020 at 12:25):

Note that there is caching.

#### Gabriel Ebner (Oct 02 2020 at 12:27):

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 (Oct 02 2020 at 12:33):

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

#### Yury G. Kudryashov (Oct 02 2020 at 12:33):

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

#### Yury G. Kudryashov (Oct 02 2020 at 12:34):

I'll just add them to simp calls explicitly.

#### Yury G. Kudryashov (Oct 02 2020 at 12:35):

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

#### Yury G. Kudryashov (Oct 02 2020 at 23:10):

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

Last updated: May 11 2021 at 16:22 UTC