Hypotheses/conclusions for strictly positive natural numbers

Stream: maths

[Antoine Chambert-Loir]

For a natural number $n$, it is equivalent that $0<n$ or that $n\neq 0$. But what is the good way to state it in Lean ?
I had convinced myself that for n : ℕ, it was better to state n ≠ 0 in hypotheses and 0< n in conclusions, because of way simp works, but if I browse at some of mathlib, it seems that it is the other way round!

[Yaël Dillies]

This is mostly historical, but also sometimes it's convenient to use 0 < n. I would say that a blanket suggestion of using n ≠ 0 unless you know what you're doing is best.

[Yaël Dillies]

In particular, the problem with the approach of having n ≠ 0 in hypotheses and 0 < n in conclusions is that you need to permanently weaken using lt.ne' when constructing a nontrivial proof term.

[Riccardo Brasca]

Have you considered using pnat directly? It's not always a good idea (you can end up with a lot of coercions), but sometimes it works very well.

[Johan Commelin]

@Yaël Dillies I thought we had actually decided to settle on exactly that. \ne in assumptions and < in conclusions.

[Johan Commelin]

There is a discussion about this somewhere on zulip

[Yaël Dillies]

Yes, and I've come to believe it actually is a bad decision :grinning:

[Yaël Dillies]

How many lemmas are actually stated like that? I suspect not many.

[Johan Commelin]

But that's because of historical inertia

[Yaël Dillies]

To me, this decision makes sense when the n in the hypothesis is considered an index (as in cyclotomic polynomials for example), but it doesn't when the function we're proving positivity of is considered an operation on naturals (as is multiplication for example).

[Yaël Dillies]

This is a philosophical difference, but it seems to follow usage.

[Antoine Chambert-Loir]

In my case, the n is like an index. Such as in docs#one_lt_zpow that proves 0 < n → 1 < a ^ n.

[Yaël Dillies]

Then that should be n ≠ 0, yes.

[Yaël Dillies]

I suspect that eventually we won't care much anymore as #16529 will make positivity solve both types of goals seamlessly (so no big term mode proofs for those obligations anymore).

[Alex J. Best]

Johan Commelin said:

Yaël Dillies I thought we had actually decided to settle on exactly that. \ne in assumptions and < in conclusions.

I thought this too, but it does make library search "weaker" compared to just picking one and sticking with it right? This is the big problem I have with the convention, maybe this is less of an issue for measure theory (where the convention was first settled on iirc)

[Sebastien Gouezel]

Indeed, we have been consistently using the convention in measure theory, and it is quite convenient. So I'd say that in new lemmas one should also use the convention, but I doubt anyone will refactor the whole library to make it consistent.
As for library_search, it should be possible to tweak it for this kind of situation (just like it has been tweaked to recognize lemmas when sides are swapped, for instance). It is a weakness of library_search, not of the convention.

[Eric Wieser]

Can we record this convention somewhere?

[Andrew Yang]

I think this is mentioned here in the style guide.

[Antoine Chambert-Loir]

To refactor the library, I wonder whether one can grep all files that do not follow the convention.
(In my ongoing work with @María Inés de Frutos Fernández on divided powers, we can refactor all cases that we fall on…)

[Alex J. Best]

One could do that with lean metaprogramming fairly easily, and it would be far more accurate than grep. Definitely worth doing at least to see the scale of the problem.
And yes Sebastian you are right of course this can be fixed on the side of library search, I'm just sad because I've just been bitten by this too many times and ended up reproving obvious things because I didn't remember to follow the convention

[Alex J. Best]

Maybe the only question is: for which types should library search do this extra step? Do we have already have a zero_eq_bot type typeclass that can be found for assumptions of the form 0 < n and turn them into n \ne 0?

[Yaël Dillies]

0 < n → n ≠ 0 holds for all preorders with a zero

[Alex J. Best]

What is a preorder with a zero?

[Yaël Dillies]

[preorder α] [has_zero α] :grinning:

[Alex J. Best]

Surely I can just call whatever I want "zero" in a preorder

[Alex J. Best]

Right, I guess I don't understand what you mean then

[Alex J. Best]

What about rat?

[Yaël Dillies]

a < b → a ≠ b in all preorders. It's the other direction that's harder.

[Alex J. Best]

Oh wait I'm thinking backwards!

[Alex J. Best]

Ok so should we just do this for every < hypothesis? Add the \ne to the assumption list in library search?

[Yaël Dillies]

In both directions, I assume yes. We want to get a ≠ b and b ≠ a from a < b

[Scott Morrison]

Alex J. Best said:

Ok so should we just do this for every < hypothesis? Add the `≠ to the assumption list in library search?

This would actually be very easy to implement in library search. Library search tries to close subsidiary goals using solve_by_elim, and you can pass solve_by_elim additional lemmas to use.

[Scott Morrison]

Just adding ne_of_lt or whatever it is called might suffice.