Zulip Chat Archive

Stream: maths

Topic: Simplifying `0 < a * b` etc


view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 01 2020 at 18:40):

(and similarly for 0 < a / b)

view this post on Zulip Johan Commelin (Oct 01 2020 at 21:32):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 21:32):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 01:45):

Currently I use simp [h.not_lt].

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 04:15):

#4359 is ready for review.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 02 2020 at 06:01):

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

view this post on Zulip Mario Carneiro (Oct 02 2020 at 06:02):

you probably have to test to find out

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 02 2020 at 08:29):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 02 2020 at 08:32):

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

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 12:14):

But what if a < 0, b < 0?

view this post on Zulip Gabriel Ebner (Oct 02 2020 at 12:15):

You need 2*2 simp lemmas.

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 12:18):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Gabriel Ebner (Oct 02 2020 at 12:25):

Note that there is caching.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 12:33):

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

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 12:34):

I'll just add them to simp calls explicitly.

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 12:35):

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

view this post on Zulip 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