Nat.lt_succ and Nat.lt_succ_iff coincide

Stream: batteries

[Sven Manthe]

I realized that both Nat.lt_succ and Nat.lt_succ_iff denote the theorem m < succ n ↔ m ≤ n. Is this intended? (I'd expect something like m<succ m as Nat.lt_succ, with Nat.lt_succ_iff unchanged)

[Yakov Pechersky]

docs#Nat.lt_succ_self

[Sven Manthe]

Thanks. (I'll leave this open for a while since I still am not sure if it is intended to have this lemma twice in batteries)

[Ruben Van de Velde]

It looks like Std had lt_succ_iff, then @Mario Carneiro renamed it to lt_succ in https://github.com/leanprover-community/batteries/commit/23f8577169c049e6eb472a0354c11b9b934b4282 and @Kim Morrison added lt_succ_iff back in https://github.com/leanprover-community/batteries/commit/a88cd10b11dc5741c7be3c06a2a8e798dc07fdcf , and then they got upstreamed to core together in https://github.com/leanprover/lean4/pull/3391

[Ruben Van de Velde]

I'd say we should pick one and deprecate the other

[Yaël Dillies]

Personally I agree with Sven and always am mildly annoyed that Nat.lt_succ is not n < succ n

[Ruben Van de Velde]

If it was still in batteries, I guess one could make a PR. Does core require an rfc or something?

[Sven Manthe]

/poll What should Nat.lt_succ be?
As currently, an alias for Nat.lt_succ_iff
An alias for Nat.lt_succ_self
Just deprecated

[Yaël Dillies]

I also thik we should just not have Nat.lt_succ_self (but only Nat.lt_succ). We don't have Nat.le_succ_self

[François G. Dorais]

I think Nat.lt_succ_iff is also bad, it should be Nat.lt_succ_iff_le. Saving extra three characters is not worth the ambiguity.

[Kim Morrison]

Proposal:

• Nat.lt_add_one: n < n + 1
• Nat.lt_succ : n < succ n (but hope it is rarely used? investigate later whether it could even be deprecated in terms of Nat.lt_add_one)
• Nat.lt_succ_self becomes a deprecated alias for Nat.lt_succ
• Nat.lt_add_one_iff_le : n < m + 1 \iff n \le m
• Nat.lt_succ_iff_le (as above)
• Nat.lt_suff_iff becomes a deprecated alias.

[Ruben Van de Velde]

What ambiguity, though? What else would be on the right hand side?

Also, do we have the same lemmas for Int or some typeclass that should match?

[Yaël Dillies]

Note that docs#Nat.lt_succ_iff goes together with docs#Nat.succ_le_iff and docs#Order.lt_succ_iff, docs#Order.succ_le_iff