feat(tactic/positivity): Extension for subtraction

[YaelDillies]

A best effort positivity extension for a - b. It looks for a proof of a ≤ b/a < b in context.

---

[hrmacbeth]

I don't really like this feature; I think it muddies the waters, making the tactic's behaviour less human-predictable. @digama0 thoughts?

[YaelDillies]

This allows me to prove 0 < min (1 / (2 * ⌈4/ε⌉₊^3)) ((1 - ε/4) * (ε/(16 * bound (ε/8) ⌈4/ε⌉₊))^3) in one go, rather than doing mul_pos (by positivity) (mul_nonneg (sub_nonneg_of_le h) $ by positivity) or have := sub_nonneg_of_le h, positivity.

The more general problem is that I can't insert manually non-positivity proofs inside a positivity search. A solution there would be to let positivity take additional proofs to add to the context before doing the search (which is better than haves before the positivity invokation because they don't clutter the context). But I need to do such a "find an assumption" in many more places:

• a - b with b ≤ a/b < a
• s.card with s.nonempty
• specific SRL quantities that I've gathered in a local positivity extension

The point is that the general solution is a general improvement, but we can do better on a case-by-case basis.

[hrmacbeth]

I guess we have different aesthetics, then, because a line of haves before a big tactic use has never bothered me. But if this is not to your taste, I'd prefer the solution of letting polyrith positivity take a list of extra terms which might be useful.

Mario also suggested this.

[digama0]

Also, the have's don't clutter the context since positivity is a closing tactic. They only appear in the subgoal leading to the positivity application if you scope it right.

[digama0]

Personally, I think it is okay to have specifically a - b nonnegativity subgoals closed by a <= b in the context, that seems like something that might still qualify as a zero step proof on paper. But all those other things Yael mentioned are definitely out of scope.

Yael, it is specifically part of the design of the tactic that you are supposed to supply proofs to it with have. But linarith is precedent for the pattern of using tac [a, b, c] as shorthand for have := a, have := b, have := c, tac so that doesn't seem unreasonable to support.

@hrmacbeth You said polyrith above, but I guess you mean positivity? polyrith actually already supports composed terms instead of intermediate have, it just looks a little weird since you have to write 2 * (h1 a b) + (h2 (h3 b c)).

[YaelDillies]

Also, the have's don't clutter the context since positivity is a closing tactic. They only appear in the subgoal leading to the positivity application if you scope it right.

I know, but I maintain my claim.

There's more to the story though. Those non-positivity goals could be satisfied using other partial structural decision procedures (like positivity). This is typically the case of finset.nonempty, hence the TODO in #16637.

My full dream is to have these decision procedures call each other, possibly in loops (so long as at least one of the procedures along the loop recursed on the structure of the expr). For example this would allow to prove 2 ≤ s.card → 3 ≤ t.card → 0 < (s ×ˢ t).card, which is quite typical of the zero step goals we get in combinatorics.

This is reminiscent of Aesop's architecture and any work towards this will make it easier to port the already existing decision procedures (positivity, norm_num extensions, ...) to the Aesop framework.

[digama0]

I get it. That's not what this tactic is for though. This is specifically intended to be a tactic with defined scope and not a kitchen sink tactic, so we always have to be vigilant against scope creep. For example you could argue that maybe ring should also try split in case it's faced with a conjunction of ring equalities, but then where do you stop? Everything you could do is a little bit helpful and a makes the tactic a little harder to predict.

[hrmacbeth]

@hrmacbeth You said polyrith above, but I guess you mean positivity?

Indeed, sorry for the confusion!

[hrmacbeth]

By the way, @YaelDillies, I wonder if there's a bit of code smell in your encountering a goal of

0 < min (1 / (2 * ⌈4/ε⌉₊^3)) ((1 - ε/4) * (ε/(16 * bound (ε/8) ⌈4/ε⌉₊))^3)

I'd typically use the archimedean principle to get something like, "there exists a natural number n, such that 4 ≤ n * ε."

[YaelDillies]

The point is to provide an explicit bound for the triangle removal lemma. Note that the bound appearing in the expression is the bound in Szemerédi's regularity lemma and is also explicit. In combinatorics at least we care about explicitness of bounds, and in particular here there was a long-standing question of whether the known bound for SRL was stupidly too big or not, and Tim Gowers proved that surprisingly it is not.

[Vierkantor]

One argument which I'm not sure is in favour of this PR or not, is that simpa can already solve 0 < a - b given b < a using sub_pos.

[YaelDillies]

That doesn't help when it's needed within an expression. For example, just a day after I opened this PR, James encountered a goal of 0 < (a - c)/(b - c) for a < c, b < c (to prove that convex functions are continuous).

[Vierkantor]

This PR has been sitting open for a while, can we come to a conclusion? As I understand it, the objection is that positivity should have a well-defined, bounded scope and this falls outside of that scope. is that right? If so, we should establish an explicit way to determine what is in scope.

[mcdoll]

That doesn't help when it's needed within an expression. For example, just a day after I opened this PR, James encountered a goal of 0 < (a - c)/(b - c) for a < c, b < c (to prove that convex functions are continuous).

I am not really qualified to comment here, but I think this is not a goal you want to use positivity on. Also I think the PR makes positivity harder to describe and less predictable.

[YaelDillies]

The alternative is to write div_pos (sub_pos_of_lt h1) (sub_pos_of_lt h2), which is precisely the kind of proofs that you would want to make disappear with positivity.

A middle ground would be to run the assumption call in this extension only on proofs that are explicitly provided to positivity (as in linarith [hyp0, hyp1]), but this is not yet implemented for positivity.

[YaelDillies]

Closing in favor of leanprover-community/mathlib4#2427