n ≠ 0 vs 0 < n

Stream: general

[Johan Commelin]

Do we have a convention on whether we assume n ≠ 0 or 0 < n in statements (for n : nat)? Should we have a linter for this?

[Floris van Doorn]

I would also like to standardize this and similar things (like n ≠ 0 vs 0 < n in ennreal or n ≠ \top vs n < \top in ennreal).

[Chris Hughes]

The convention is 0 < n but I would prefer n ne 0

[Floris van Doorn]

My vote would be to use inequalities as default: they are more easily usable. For example n ≠ 0 and n \le m doesn't immediately give m ≠ 0, but replace ne 0 by inequalities and it's one step.
(inequalities are sometimes 1 step longer to prove, but I think "immediate usability" is more useful).

[Floris van Doorn]

Why would you prefer \ne, @Chris Hughes?

[Chris Hughes]

It's usually easier to prove ne 0, assume h : n = 0, simp * at * works quite a lot. It's also more consistent with types other than nat, where a nonzero assumption is more common than positivity, so it's easier to prove a casted nat is nonzero if you already have n ne 0

[Chris Hughes]

example (n m : ℕ) (hn : n ≠ 0) (hm : n ≤ m) : m ≠ 0 := λ h, by simp * at *

[Chris Hughes]

I think assumptions like a * b \ne 0 are more common ways to prove nonzero-ness than transitivity of le or lt

[Johan Commelin]

Before writing this post I was also intuitively leaning towards ≠... I think unconsciously for reasons similar to the ones that Chris has listed.

[Floris van Doorn]

Ok, that's fair. I'm fine with switching to "not equal" as default.

[Johan Commelin]

@Floris van Doorn How hard is it to write a linter for this?

[Floris van Doorn]

It's not hard.
So the linter complains whenever you have an assumption of the form 0 < _ in nat. That's easy. I think we want to allow other cases, like an iff containing 0 < _?

[Johan Commelin]

I don't know if we want that...

[Johan Commelin]

I think that apart from some cases that we explicitly nolint, we should strive to then keep 0 < _ out of assumptions, and conclusions.

[Floris van Doorn]

ok, it's also easy to check for any occurrence of 0 < _ in nat.

[Floris van Doorn]

Let's first get to a consensus though, few people have chimed in so far.

[Johan Commelin]

Let's ping some people with opinions: @Mario Carneiro @Patrick Massot @Sebastien Gouezel @Simon Hudon @Gabriel Ebner

[Johan Commelin]

@Kenny Lau @Scott Morrison @Kevin Buzzard @Reid Barton

[Johan Commelin]

Lol... I could almost as well have just used @maintainers :face_palm:

[Kenny Lau]

first let's remove all the n > 0 instances in core

[Kenny Lau]

For n ≠ 0, like this message (you can like both).

[Kenny Lau]

For 0 < n, like this message (you can like both).

[Kevin Buzzard]

I love that ne is a function: you can just apply it when you're showing simple term mode stuff to mathematicians or explaining definitional equality. The more ne the better

[Reid Barton]

I don't see much point in a lint rule because it will be unavoidable to use both anyways.

[Reid Barton]

I'd rather just write whatever is more natural/convenient locally, which I guess is the status quo.

[Scott Morrison]

A lint rule seems excessive, except for the fact that it would be really nice to be much more consistent/principled about this choice, and from experience it may take a linting rule to push us to achieve this. :-)

[Yaël Dillies]

I'm about to change some occurrences of n ≠ 0 as hypotheses to 0 < n (where n : ℕ) eg in data.multiset.erase_dup. Is everybody fine with that?

[Johan Commelin]

If the diff has a net negative size, then I would find it hard to object.

[Floris van Doorn]

There was a 10-to-1 vote in favor of n ≠ 0 compared to 0 < n earlier in this thread, so I think not everybody is fine with that.

[Johan Commelin]

Good point. I've just changed my vote to no vote

[Sebastien Gouezel]

The convention we have settled on in ennreal (with respect to top) is that in assumptions we should favor a \ne top, and in conclusions we should favor a < top. The reason being that it is very easy to go from the strict inequality to non-equality, so if you have strict inequality in the context it is trivial to apply a lemma using non-equality.

[Yaël Dillies]

Well, I'm mostly removing some nat.pos_of_ne_zero hn where hn : n ≠ 0. So it does sound like I'm going in the right direction.

[Yaël Dillies]

Also, the style guide indicates that 0 < n is the favored form.

[Yaël Dillies]

To be fair, if everything was using n ≠ 0 this wouldn't happen.

[Johan Commelin]

Would it be evil to have

section

variables {α : Type*}

lemma ne.bot_lt [order_bot α] {a : α} (h : a ≠ ⊥) : ⊥ < a :=
bot_lt_iff_ne_bot.mpr h

lemma ne.bot_lt' [order_bot α] {a : α} (h : ⊥ ≠ a) : ⊥ < a :=
h.symm.bot_lt

lemma ne.lt_top [order_top α] {a : α} (h : a ≠ ⊤) : a < ⊤ :=
lt_top_iff_ne_top.mpr h

lemma ne.lt_top' [order_top α] {a : α} (h : ⊤ ≠ a) : a < ⊤ :=
h.symm.lt_top

end

[Sebastien Gouezel]

It wouldn't be evil at all, but it would still be longer to type than h.ne to go from h : a < top to a \ne top (or h.ne' for the other non-equality) :-)

[Johan Commelin]

Completely agreed. So I think your rule of thumb "inputs use \ne, outputs use <" is a very good one. But we will still need to move from \ne to < occasionaly.

[Sebastien Gouezel]

Does everyone agree that I update the style guide to mention this rule of thumb?

[Yaël Dillies]

I would first see how often n ≠ 0 and 0 < n are used, because in my experience I encountered 0 < n much more.

[Eric Rodriguez]

I've seen both, and I've made an active effort to write an API that uses n ≠ 0 as inputs and 0 < n as outputs as much as possible

[Ruben Van de Velde]

The question isn't so much what exists now, but what's most useful going forward. There seemed to be a fair amount of support for ne in hypotheses upthread, at least.

[Johan Commelin]

#8935 has the dot-notation lemmas from above

[Sebastien Gouezel]

I have updated the style guide, see the paragraph Normal forms at the end of https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/contribute/style.md#normal-forms