Int version of Nat.succ_le ?

Stream: new members

[rzeta0]

I can't seem to find an Int version of Nat.succ_le.

Is it the case there isn't one?

Or am I missing a trick where Nat.succ_le can be used for integers by flipping negative integers to positive, applying the lemma, and then flipping back to negative, switching the direction of the inequality?

[Damiano Testa]

You could try

import Mathlib

example (n m : Int) : n + 1 ≤ m ↔ n < m := by
  exact?

[rzeta0]

thank Damiano - is this the recommended way of searching for lemmas? To use exact? where you think there might exist a relevant lemma?

[Damiano Testa]

I use this method fairly often, although I usually first try to guess the name of the lemma and see if autocompletion is kind enough to tell me what the lemma is.

[rzeta0]

your suggestion found Int.add_one_le_iff

but it also found Nat.add_one_le_iff .. which looks exactly like Nat.succ_le .. is there a difference? The signature suggest there is no difference.

[Damiano Testa]

It looks like they are definitionally equivalent:

example : @Nat.add_one_le_iff = @Nat.succ_le := rfl

[rzeta0]

given the reluctance of mathlib maintainers to add requested lemmas, should I assume these two exist just as an accident of history, and there is no valid intentional reason for them to both exist?

(my beginner brain tells me succ is more axiomatic than +1)

[Damiano Testa]

I think that rw would not be able to use these two lemmas interchangeably.

[rzeta0]

interesting - why is that?

I just tried it and it seems to work:

import Mathlib.Tactic

lemma Nat.le_or_succ_le (a b: ℕ): a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.succ_le] --<----------
  exact le_or_lt a b

lemma Nat.le_or_succ_le' (a b: ℕ): a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.add_one_le_iff] --<----------
  exact le_or_lt a b

so I assume you mean something different?

[Kevin Buzzard]

Oh I'm surprised about this. This is all about different kinds of equality in Lean (see https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/Part_B/equality.html ). I had imagined that a + 1 and Nat.succ a were definitionally, but not syntactically, equal, and my mental model is that rw works up to syntactic equality so the top one would fail.

[Damiano Testa]

Actually, I meant exactly what you tried and I am also surprised that it works.

[Damiano Testa]

Maybe this is the recent switch to using +1 more aggressively than Nat.succ that makes it work in this case?