cancel_denoms exercise

Stream: metaprogramming / tactics

[Miroslav Olšák]

@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]

@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]

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

[Rob Lewis]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

@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]

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

[Rob Lewis]

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]

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]

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

[Rob Lewis]

For comparison, the current cancel_denoms results in

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

[Rob Lewis]

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]

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]

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

[Rob Lewis]

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]

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]

norm_num can't cancel that

[Mario Carneiro]

ring might

[Miroslav Olšák]

OK, I am not sure what it was.

[Miroslav Olšák]

I reused a lot of the original code.

[Mario Carneiro]

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]

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]

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

[Miroslav Olšák]

I don't see any tactic ring used there.

[Miroslav Olšák]

@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]

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]

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]

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]

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]

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

[Heather Macbeth]

The goal seems to be

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

[Rob Lewis]

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]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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]

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]

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

[Miroslav Olšák]

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]

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

[Miroslav Olšák]

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]

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

[Rob Lewis]

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]

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]

Any progress? Should I look into linarith?

[Rob Lewis]

Sorry. It's been a distracting week

[Rob Lewis]

I'll find time to look into this today.

[Rob Lewis]

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

[Rob Lewis]

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.