Stream: metaprogramming / tactics

Topic: cancel_denoms exercise

Miroslav Olšák (Oct 22 2020 at 12:51):

@Rob Lewis As I am trying to learn Lean tactics, I sort of did the cancel_denoms exercise:
cancel_denoms.lean
Would you like to integrate it to mathlib? Notes:

• I defined lcm and gcd for rational numbers there. If you agree it is a reasonable definition, it could belong somewhere else.
• It is still handling numerical values only. Handling general expression would be chalenging, I would need some sort of the least common multiple for polynomial expressions.
• It is not a conservative extension -- some cases are handled a bit differently.

Rob Lewis (Oct 22 2020 at 19:31):

@Miroslav Olšák An improved cancel_denoms would be great to have in mathlib. It's only expected to handle numerical values, polynomial denominators are indeed much harder. Do the linarith tests pass using your cancel_denoms in place of the existing one? That would be a very good sign.

Rob Lewis (Oct 22 2020 at 19:31):

I'm on vacation and won't be able to look at this until next week at the earliest.

Rob Lewis (Oct 22 2020 at 19:32):

But if you make a PR I'll review when I have time, or of course I don't mind if others review first!

Miroslav Olšák (Oct 22 2020 at 21:20):

I am not sure how to perform the tests. Where are they? And if I just replace the file cancel_denoms.lean in the mathlib directory by mine, will Lean reload it? (as far as I understand, mathlib is somehow precompiled)

Miroslav Olšák (Oct 22 2020 at 21:20):

I hope that my version will work but there still could be some issues with zeroes, and it is also probably slower as it is handling fractions generally as expr / expr, and uses rational numbers instead of naturals.

Miroslav Olšák (Oct 22 2020 at 21:20):

I can wait when you will have time. But help from someone else is also welcome.

Bryan Gin-ge Chen (Oct 22 2020 at 21:22):

You can run the linarith tests locally by running lean test/linarith.lean.

You can also push your edits to a branch on the mathlib repo (do you need access?) and then the CI will run all the tests for you.

Miroslav Olšák (Oct 23 2020 at 08:26):

OK, so it is not as easy to pass the tests. First it turned out that the function derive is actually necessary, so I implemented it again, and now it does not work for some reason. Could it be because I leave too much mess in the expression which is cleaned up by norm_num in the interactive version?
Current version: cancel_denoms.lean

Rob Lewis (Oct 26 2020 at 18:31):

@Miroslav Olšák I've sent you an invite to the mathlib repository. Instead of sharing lean files here, it's much easier to discuss/comment on a git branch. https://github.com/leanprover-community/mathlib/tree/cancel-denoms-mirefek

Rob Lewis (Oct 26 2020 at 18:32):

(I haven't made a PR yet. You should do that so you get the credit for it.)

Rob Lewis (Oct 26 2020 at 18:33):

Indeed, derive is necessary and isn't strong enough in your version. You can see in the first failing linarith test what's going on:

import tactic.linarith

set_option trace.linarith true
example (A B : ℚ) (h : 0 < A * B) : 0 < A*B/8 :=
begin
linarith
end


Rob Lewis (Oct 26 2020 at 18:33):

After the cancel_denoms preprocessing, you're left with

Preprocessing: cancel denominators
[1 * (1 * (1 * A) * (1 * B)) / (1 / 8 * 8) ≤ 0, -(A * B) < 0]


Rob Lewis (Oct 26 2020 at 18:34):

The 1*s shouldn't really matter, but the denominator isn't cancelled, and that does matter.

Rob Lewis (Oct 26 2020 at 18:35):

For comparison, the current cancel_denoms results in

Preprocessing: cancel denominators
[1 * A * (1 * B) ≤ 0, -(A * B) < 0]


Rob Lewis (Oct 26 2020 at 18:37):

linarith might be smart enough to deal with a / 1 left over, off the top of my head I'm not sure. But I guess it doesn't like the / (1/8 * 8).

Rob Lewis (Oct 26 2020 at 18:39):

I haven't looked carefully at the diff between the old version and yours yet. Do you have an idea how you might fix this? If not, I'll look more closely.

Rob Lewis (Oct 26 2020 at 18:40):

If you do, you can push your changes directly to the branch branch#cancel-denoms-mirefek

Rob Lewis (Oct 26 2020 at 18:42):

Github will try to build every commit that gets pushed. So you'll see a red X there as long as things are failing to build, including the tests. In this case, though, it's maybe easier to build the linarith test file locally. There aren't many imports between the test file and cancel_denoms.lean

Miroslav Olšák (Oct 26 2020 at 18:52):

I think I can fix it. I was just lazy, so if the norm_num actually canceled the mess, I didn't care so much.

Mario Carneiro (Oct 26 2020 at 18:53):

norm_num can't cancel that

Mario Carneiro (Oct 26 2020 at 18:53):

ring might

Miroslav Olšák (Oct 26 2020 at 18:53):

OK, I am not sure what it was.

Miroslav Olšák (Oct 26 2020 at 18:54):

I reused a lot of the original code.

Mario Carneiro (Oct 26 2020 at 18:54):

ring won't be able to fix that the lhs is apparently 64 times larger than rob's version? Does that matter?

Miroslav Olšák (Oct 26 2020 at 18:57):

I will look at the github repository, and fix the issues, hopefully this week. I was not sure how much I have to care about the special cases as long as it was somehow miraculously working on the basic examples I tried.

Miroslav Olšák (Oct 26 2020 at 18:59):

But if someone knows why the interactive version contrary to derive reduces the expression, I would appreciate knowing it.

Miroslav Olšák (Oct 26 2020 at 19:00):

I don't see any tactic ring used there.

Miroslav Olšák (Oct 29 2020 at 12:04):

@Rob Lewis I pushed a version which already passes the linarith tests. On the other hand, they are about 2.5 times slower than with the original version, I am not exactly sure what to do about it.

Miroslav Olšák (Oct 29 2020 at 12:52):

I received a message from Github that "continuous integration: Some jobs were not successful": https://github.com/leanprover-community/mathlib/actions/runs/335756434
What does it mean?

Jannis Limperg (Oct 29 2020 at 13:06):

Whenever you push to a branch on the mathlib repository, Github tries to build and lint the commit you pushed. This process failed, so your changes have broken something in mathlib. You can click on "Lint style" and "Build mathlib" on the left and it'll show you exactly what errors were found. You don't have to fix them immediately, but they should be fixed when you make a PR.

Miroslav Olšák (Oct 29 2020 at 14:58):

OK, one error is easily fixable "too long lines", and the other is the linarith tactic failing somewhere (in particular gromov_hausdorff.lean). Would it be possible to figure out from it where the cancel_denom does not work properly?

Heather Macbeth (Oct 29 2020 at 15:01):

Yes, it should be line 531:

/home/runner/work/mathlib/mathlib/src/topology/metric_space/gromov_hausdorff.lean:531:30: error: linarith failed to find a contradiction


Heather Macbeth (Oct 29 2020 at 15:02):

https://github.com/leanprover-community/mathlib/blob/d510a637b9d1d1cb72acb1f847694281f0c61051/src/topology/metric_space/gromov_hausdorff.lean#L531

Heather Macbeth (Oct 29 2020 at 15:03):

The goal seems to be

ε₂ ≤ 2 * (ε₂/2 + δ)


Rob Lewis (Oct 29 2020 at 16:27):

You can use set_option trace.linarith true to get some information about what linarith is doing. In particular it will print the hypotheses before and after denominator cancellation.

Rob Lewis (Oct 29 2020 at 16:27):

For the efficiency problem, I'll take a look. set_option profiler true often gives useful information here.

Rob Lewis (Oct 29 2020 at 18:38):

The pattern you use here and above, where you try to apply a bunch of different lemmas to see which one works, can be expensive. It's better if you can identify which lemma is the right one based on the values you have access to, and apply it directly.

Rob Lewis (Oct 29 2020 at 18:38):

I'm not sure that this is what's causing the slowdown though.

Rob Lewis (Oct 29 2020 at 18:39):

Your version is spending a lot more time in various places, including in norm_num.

Rob Lewis (Oct 29 2020 at 18:39):

Part of this is because it's doing more than the old version is. But on problems that the old version solves too, I wouldn't expect it to be doing too much more, not enough to see this kind of slowdown.

Rob Lewis (Oct 29 2020 at 18:40):

https://github.com/leanprover-community/mathlib/blob/cancel-denoms-mirefek/src/tactic/cancel_denoms.lean#L158 is wrong, this check only works if the original problem is over rat. A simpler check is guard (v = 1).

Rob Lewis (Oct 29 2020 at 18:41):

This simplifies one call to norm_num but not by a huge amount.

Miroslav Olšák (Oct 30 2020 at 08:55):

Sure, I am aware of many places where some optimization could be added (I should try the profiler to see which is the bottleneck now).

Miroslav Olšák (Oct 30 2020 at 08:55):

Now, I am rather planning to figure out the problem with gromov_hausdorf.lean.

Miroslav Olšák (Oct 30 2020 at 09:18):

I don't get the problem with gromov_hausdorf.lean. When I enabled debug prints for linarith, I got

Preprocessing: make comparisons with zero
[-δ < 0, dist xα xs - ε₁ ≤ 0, -ε₂ ≤ 0, 2 * (ε₂ / 2 + δ) - ε₂ < 0]
Preprocessing: cancel denominators
[2 * (ε₂ / 2 + δ) - ε₂ < 0, -ε₂ ≤ 0, dist xα xs - ε₁ ≤ 0, -δ < 0]


But when I test derive on my own, like this:

meta def test_derive (e : expr) : tactic unit :=
do
(n, pf) ← cancel_factors.derive e,
tp ← tactic.infer_type pf,
tactic.trace n,
tactic.trace tp

constants x y : ℚ
run_cmd test_derive (2 * (x / 2 + y) - x)


It behaves well:

1
1 * (2 * (x / 2 + y) - x) = 1 * (x + 2 * y) - x


Miroslav Olšák (Oct 30 2020 at 09:19):

Maybe linarith does not use the simplification when the factor is 1?

Rob Lewis (Oct 30 2020 at 15:59):

Hmm. There is something odd going on here. Didn't manage to locate it immediately. I'll take a closer look later today when I have the time.

Rob Lewis (Oct 30 2020 at 15:59):

Miroslav Olšák said:

Maybe linarith does not use the simplification when the factor is 1?

It's something to do with this, yes, but not as obviously as you might expect.

Miroslav Olšák (Nov 06 2020 at 14:13):

Any progress? Should I look into linarith?

Rob Lewis (Nov 06 2020 at 14:22):

Sorry. It's been a distracting week

Rob Lewis (Nov 06 2020 at 14:22):

I'll find time to look into this today.

Rob Lewis (Nov 06 2020 at 17:53):

@Miroslav Olšák sorry for the delay. I pushed a fix to the branch.

Rob Lewis (Nov 06 2020 at 17:57):

The issue was with expressions that can be cancelled without a new factor, like 2 * (x / 2 + y). cancel_denoms needs to do some work here, and the old version unnecessarily multiplied the whole thing by 2. When the new one produces a factor of 1 there's an extra step needed to make sure that 1*` appears (or doesn't appear) in the right place.

Last updated: May 09 2021 at 22:13 UTC