Performance issues with norm_num in rationals

Stream: mathlib4

[Sebastian Zimmer]

I'm working on a tactic which automatically derives rational approximations to real expressions in order to prove inequalities. I've managed to make finding the approximation quite fast, but creating the final proof term is still slow for complicated expressions.

My current implementation strategy involves using the norm_num tactic to automatically prove many terms like (24 : ℚ) / 17 * (24 / 17) ≤ 2 / 1. Proving these kind of expressions takes tens of milliseconds even with small numbers, which adds up since I need to prove so many terms of this kind (that is, terms computed in ℚ involving relatively small numbers of literals all of reasonable size). I would have expected it to be much faster.

I have a few questions about this:
1) Why can't I just use decide to prove this kind of result? The kernel seems capable of computing with natural numbers and integers, so why can't it do rational numbers? It's just an integer and a natural after all.

2) Is there some kind of normal form I can write rationals in that makes NormNum faster at deriving their value? I've noticed that it indirectly special cases expressions for which expr.rat? works, which implies I should put the rational into the form Div.div a b but this doesn't actually seem to work at all.

3) Should I then try to avoid entirely arithmetic with rationals inside the final proof terms? I think it would be possible but it would probably complicate the code a lot.

[Aaron Liu]

decide does work here, and for this example seems to be consistently faster than norm_num

import Mathlib

#time -- 15~20 ms on the web server
example : (24 : ℚ) / 17 * (24 / 17) ≤ 2 / 1 := by decide +kernel

[Sebastian Zimmer]

What does +kernel do? I haven't seen that before

[Aaron Liu]

It means to skip elaboration and just check with the kernel, this is slower to fail but works on more statements.

[Sebastian Zimmer]

Ah I see. Why does the elaborator fail but the kernel succeed? Transparency settings?

[Aaron Liu]

Since the kernel ignores transparency, it doesn't get stuck on Rat.mul and Rat.inv, which are irreducible.

[Sebastian Zimmer]

What's the reason for those being irreducible?

The code just says

This definition is `@[irreducible]` because you don't
want to unfold it
```

[Mario Carneiro]

if you have concrete expressions to check (e.g. a sum of two rationals) as part of a tactic, I recommend using norm_num's backend functions instead of using by norm_num, which is really the equivalent of simp with a norm-num simpproc

[Mario Carneiro]

a very simple thing you can do to reduce the impact of using the global simp set is to use norm_num1 instead of norm_num, which still uses simp but only in a bare minimum way to find subterms to rewrite

[Mario Carneiro]

the backend functions have no ability to look into subterms, but they are perfect when the problem to solve is already set up to have the right shape for norm_num's consumption

[Mario Carneiro]

I suspect that used properly, norm_num can beat kernel reduction when it comes to Rat arithmetic. But I haven't tested this

[Mario Carneiro]

But generally if you have the ability to massage the goal into an optimal form for computation it's usually easier to just go to Nat arithmetic, and there kernel computation definitely outperforms norm_num (and norm_num knows this and uses the kernel for such goals)

[Sebastian Zimmer]

But generally if you have the ability to massage the goal into an optimal form for computation it's usually easier to just go to Nat arithmetic, and there kernel computation definitely outperforms norm_num (and norm_num knows this and uses the kernel for such goals)

I'm sure that would be possible, but I want my final tactic to be easily extensible and stating/proving bounds and approximations is hard enough without having to write everything in terms of integer/natural arithmetic.

[Mario Carneiro]

That depends on what you mean by "everything"

[Mario Carneiro]

you should be able to structure most lemmas in the form number crunching assertion -> thing I want

[Mario Carneiro]

Most of norm_num's own lemmas are in this form

[Mario Carneiro]

2) Is there some kind of normal form I can write rationals in that makes NormNum faster at deriving their value? I've noticed that it indirectly special cases expressions for which expr.rat? works, which implies I should put the rational into the form Div.div a b but this doesn't actually seem to work at all.

The normal form NormNum actually uses is subproofs like IsRat x a b where x is a term in an arbitrary type, and a is an Int numeral and b is a Nat numeral, which mean something like x = a/b

[Mario Carneiro]

The lowest level interface norm_num provides that can add two rational numbers is docs#Mathlib.Meta.NormNum.evalAdd.core, which you can call with two IsRat values to get another one. There are functions to convert to and from NormNum.Result if you have an equality or just a number which is a division and which you assert (but don't need to prove) is in lowest terms