infinity in positivity?

Stream: maths

[Yury G. Kudryashov]

How hard would it be to add support for ≠ ∞ to positivity?

[Yury G. Kudryashov]

I see that it breaks a linear order on outputs.

[Yury G. Kudryashov]

Use case: docs4#ENNReal.div_pos_iff

[Heather Macbeth]

I agree that it would be nice to have a "syntactically obviously non-infinite" tactic doing the same style of reasoning as positivity does for "syntactically obvious positivity". It seems like a matter of taste whether we wrap this into positivity or make it a new tactic called "finiteness".

[Heather Macbeth]

(It would also be useful as an additional discharger for gcongr, since this is another side condition which comes up frequently on gcongr lemmas.)

[Yury G. Kudryashov]

Indeed, if finiteness is a new tactic, then positivity and finiteness plugins for ENNReal can call each other if they see a / b without breaking the linear order.

[Yury G. Kudryashov]

BTW, !4#5265. I can try to do it but I don't know whether it's better to add a new eval* or try to merge it into the existing one.

[Notification Bot]

This topic was moved here from #mathlib4 > infinity in positivity? by Heather Macbeth.

[Heather Macbeth]

@Yury G. Kudryashov @Mario Carneiro A related point: it would be nice to make positivity more automated, so that a certain class of lemmas can just be tagged @[positivity] rather than writing out a positivity extension as a mini-tactic. I've been really enjoying that @[gcongr] can do this.

[Heather Macbeth]

The class of lemmas could be something like: goal is of the form 0</≠0/0≤, and all Prop hypotheses are of the form 0</≠0/0≤ for free variables occuring in the goal expression.

[Yury G. Kudryashov]

I think that we should allow other hypotheses. The tactic should try to use assumption for them.

[Heather Macbeth]

Positivity doesn't do that currently.

[Yury G. Kudryashov]

E.g., gauge s x is positive if (hs : Absorbent ℝ s) (hb : Bounded s) (hx : x ≠ 0)

[Heather Macbeth]

But yes, it could.

[Yury G. Kudryashov]

Can we run aesop with a list of lemmas?

[Yury G. Kudryashov]

With a custom discharger for inequalities between numbers.

[Heather Macbeth]

Positivity is cleverer than aesop (within its domain), because it reasons bottom-up: if it can prove a term is 0≤ one way and 0< another way, it moves forward with the better one.

[Yury G. Kudryashov]

Is it done to avoid backtracking on goals like 0 < a + b?

[Yury G. Kudryashov]

About other types of assumptions: positivity plugins can do whatever they want. In particular, they can try to find Metric.Bounded s in assumptions.

[Heather Macbeth]

Oh sorry, you're right.

[Frédéric Dupuis]

I have also been missing this feature in positivity. Just using aesop as a discharger for goals it can't reduce further (possibly with a custom set of lemmas to keep it fast) would do wonders I think.

[Yury G. Kudryashov]

The problem is that positivity does not create these extra goals.

[Yury G. Kudryashov]

It goes from inside to outside and asks plugins what they can prove.

[Yury G. Kudryashov]

If someone rewrites positivity to leave less freedom to plugins (or make a generic plugin that runs all @[positivity] lemmas), then this new version should do something about extra goals.

[Heather Macbeth]

If I understand correctly, we have to choose between (A) non-opinionated positivity that tries multiple techniques on a subexpression (carrying forward the best result) and is finishing-only, vs (B) opinionated positivity that tried only one technique per subexpression, but is a useful non-finishing tactic. Current status is (A).

[Frédéric Dupuis]

My understanding is that it goes through the hypotheses in the current context after trying all the plugins, and I think replacing that pass with aesop should go quite far.

[Kevin Buzzard]

There's always the possibility of positivity!...("tries harder to close side goals")

[Yaël Dillies]

Let me remind you of #16632, which adds an extension to prove 0 ≤ a - b from a b ≤ a assumption in context.

[Mario Carneiro]

@Heather Macbeth yes we could do that. Are you up for another hacking session?

[Heather Macbeth]

Yes, let's do it!

[Heather Macbeth]

Yury G. Kudryashov said:

How hard would it be to add support for ≠ ∞ to positivity?

Reviving this old thread for later cross-reference: I implemented a prototype finiteness tactic for the PFR project, see
https://github.com/teorth/pfr/pull/20
and if it works well there we can move it to mathlib.