normal form for 0 < (natural)

Stream: mathlib4

[Kevin Buzzard]

I am confused. An early lesson in formalisation that you learn is that there are many implementations of one mathematical specification. In other words, if someone asks on the Zulip "how do you prove [some mathematical statement written in human language or LaTeX]?" then a good response is "please can you write down the statement of what you want in Lean?", because there are many ways of saying the same thing.

For simple concepts the community has decided upon "simp normal forms". For example it's quite rare to see a > b in mathlib, because the normal form for this mathematical idea is b < a.

However, if n : Nat then the concept of being positive, or equivalently non-zero, has arguably no simp normal form, and a section of the style guide https://leanprover-community.github.io/contribute/style.html#normal-forms is specifically devoted to this issue, where the conclusion is that because it's easy to convert a < b to b ≠ a and less easy the other way around (because it's false in general if a isn't 0), we should have n ≠ 0 in hypotheses and 0 < n in conclusions.

With that in mind, let me present Ne.zero_lt:

import Mathlib

example (n : ℕ) (hn : 0 < n) : n ≠ 0 := hn.ne' -- easy

example (n : ℕ) (hn : n ≠ 0) : 0 < n := Nat.zero_lt_of_ne_zero hn -- the pain!

def Ne.zero_lt {n : ℕ} (hn : n ≠ 0) : 0 < n := Nat.zero_lt_of_ne_zero hn -- the fix

example (n : ℕ) (hn : n ≠ 0) : 0 < n := hn.zero_lt -- now easy!

As far as I can see, this completely blows a hole in the argument for our current funny convention, and we should just pick one rather than making things more complicated than they are.

What am I missing?

[Yaël Dillies]

Actually, we already have Ne.zero_lt in the form of docs#Ne.bot_lt

[Kevin Buzzard]

(I agree that's definitionally the same, and also not syntactically the same)

[Yaël Dillies]

Syntactic equality is not a very big deal here since you usually feed those hn.bot_lt to some lemma that has a 0 < n assumption.

[Yaël Dillies]

You can already see this pattern in mathlib quite a lot, btw!

[Yaël Dillies]

This is why I don't really follow that part of the style guide. Instead, I usually have one lemma with ≠ 0 assumptions and a ≠ 0 conclusion and the same lemma with 0 < assumptions and a 0 < conclusion.

[Yaël Dillies]

And same thing with ↔ lemmas.

[Damiano Testa]

Not necessarily a big deal, but this still does not work:

example (n : ℕ) (hn : ¬ n = 0) : 0 < n := hn.zero_lt
/-
invalid field notation, type is not of the form (C ...) where C is a constant
  hn
has type
  n = 0 → False
-/

[Yaël Dillies]

It is important to have both versions because you often want to interface those lemmas with lemmas from some other API which might write everything in terms of ≠ 0 (if it's algebraic) or 0 < (if it's order theoretic)

[Kevin Buzzard]

So you're saying that the current suggestion in the style guide is not what is happening anyway?