Alternative to mono?

Stream: maths

[Geoffrey Irving]

As part of some work in complex analysis, I wrote a “bound” tactic to prove “obvious” inequalities: https://github.com/girving/ray/blob/main/src/tactics.lean#L70. Example use within calc: https://github.com/girving/ray/blob/main/src/hartogs.lean#L674.

I was new to mathlib and hadn’t noticed the mono tactic, but I think my version is better in some ways. In particular it knows that multiplication by terms which are obviously nonnegative is monotone, and it seems like neither mono or mono* know this.

(It’s also possible I’m just confused here: I’d love if mono actually does what I need.)

On the other hand, “bound” is a fixed list of lemmas rather than the standard attribute method, which is ugly, and it would also be ugly to introduce another attribute when mono also has a dedicated one.

Is there a good way to clean up bound into something that could be upstreamed?

[Johan Commelin]

Do you know about tactic#positivity ? Sounds like your bound is a mix of positivity and mono.

[Geoffrey Irving]

Neat, I didn’t know about positivity. Is there a good way to mix them together to simulate bound?

[Heather Macbeth]

@Geoffrey Irving I've written a similar tactic for teaching, see https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation.html#proving-inequalities
This was actually my motivation for writing the tactic positivity.

Something like `[apply_rules with mono_rules; try { positivity }] should work as a quick version of your tactic (I think you missed the option to tag a set of lemmas with an attribute and then run apply_rules with that attribute; this has the advantage of being extensible later).

[Heather Macbeth]

Also I have found that one wants to run apply_rules at the reducible level (rather than the default semireducible), otherwise it can e.g. eagerly compare a + b with 2 by interpreting 2 as 1 + 1.

[Heather Macbeth]

I would like to get something like this into mathlib eventually, but in the experimentation I've done, I've often encountered priority problems: multiple lemmas could apply (or, a lemma and a local hypothesis), and one wants to explicitly mark priorities among these (maybe giving local hypotheses top priority). So I'd like to implement a version of apply_rules with priorities first. And this should probably wait for Lean 4 ...

[Heather Macbeth]

And sometimes even a priority system wouldn't be good enough, one wants to manually describe how many levels down to make the comparison. I think it would be good to have a version of tactic#congrm 's syntax available for that use case.

[Geoffrey Irving]

Yes, priorities are one advantage of the manual list: the most important case is a^2 >= 0 vs. a^n >= 0. :)

I will try out your quick version! Thank you!

[Heather Macbeth]

If I remember correctly, you can still get "priorities" with an attribute by tagging the lemmas in the right order. That is,

attribute [mono_rules] lemma1 lemma2

vs

attribute [mono_rules] lemma2 lemma1

But obviously it's a hack either way :)

[Geoffrey Irving]

Ah, I see: and I can make a specialized bound_rules attribute that’s searched first but also use mono_rules. That should work well for now.

[Heather Macbeth]

Geoffrey Irving said:

the most important case is a^2 >= 0 vs. a^n >= 0. :)

By the way, positivity should deal with both of these for you, with somewhat smarter logic than a priority system. Likewise for anything of the form 0 ≤ A. The only lemmas you need to tag with your attribute are those of the form A ≤ B (like mul_le_mul, add_le_add, etc).