Questions about my first lemma: `le_or_succ_le`

Stream: new members

[rzeta0]

Following on from a previous discussion, I'm now looking at implementing a version of le_or_succ_le in a library to go with the educational examples I'm developing.

I started writing and then compared it to a more expert example (see below):

theorem Nat.le_or_succ_le {a b: ℕ}: a ≤ b ∨ succ b ≤ a := by -- < -- my attempt

lemma le_or_succ_le (a b : ℕ) : a ≤ b ∨ b + 1 ≤ a := by -- < -- expert example

I have some questions:

• theorem or lemma, or doesn't it matter?
• Nat.le_or_succ or le_or_succ .. and why? is Nat a reserved namespace?
• succ b or b+1 ? ... in my environment succ causes an error
• variables declared as natural numbers inside round or curly brackets? H MacBeth's course uses curly brackets, and round brackets for hypotheses.

---

for convenience I've copied @Ruben Van de Velde's suggestion here:

Ruben Van de Velde said:

No opinion on whether it should be in mathlib, but it can be proved quite quickly:

import Mathlib.Data.Nat.Defs
lemma le_or_succ_le (a b : ℕ) : a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.succ_le]
  exact le_or_lt a b

[Shreyas Srinivas]

curly brackets are implicit parameters. When calling a declaration/theorem one usually doesn't have to provide them. Lean will try to synthesise these parameters from the context provided by the other parameters.

[rzeta0]

@Shreyas Srinivas when I changed the round brackets to curley ones, it didn't work:

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

So does having round brackets mean the definitions are necessarily explicit, and is this required when defining lemmas?

Also I'm not calling the theorem, I'm defining it? Are we talking about different things?

[Eric Wieser]

You need to be a lot more specific than "--<-- error" for us to diagnose. What does the error say?

[rzeta0]

@Eric Wieser

Here is the definition - using curly brackets:

lemma le_or_succ_le {a b: ℕ}: a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.succ_le]
  exact le_or_lt a b

Here is where it is used:

example {n : ℕ} : n^2 ≠ 2 := by
  have h := le_or_succ_le n 1     -- < see below for error
  obtain ha | hb := h
  · apply ne_of_lt
    calc
      n^2 ≤ (1)^2 := by rel [ha]
      _ < 2 := by norm_num
  · apply ne_of_gt
    calc
      n^2 ≥ (2)^2 := by rel [hb]
      _ > 2 := by norm_num

The error is as follows:

function expected at
  le_or_succ_le
term has type
  ?m.8274 ≤ ?m.8275 ∨ ?m.8275 + 1 ≤ ?m.8274

There is no error when using round brackets in the definition.

[rzeta0]

---

Also i'd appreciate comments on the 4 specific questions in the original post.

[Eric Wieser]

Ah, so the error was not in the code you posted early, but in the code you hadn't posted yet! It's helpful if you can makes your posts #mwe s, by also including the import lines.

[Eric Wieser]

rzeta0 said:

• theorem or lemma, or doesn't it matter?

they're the same once you import Mathlib.*

• Nat.le_or_succ or le_or_succ .. and why? is Nat a reserved namespace?

It should have the Nat. prefix, but this is implied if you write it in namespace Nat.

• succ b or b+1 ? ... in my environment succ causes an error

succ causes an error because you have to open Nat or write Nat.succ or already be inside namespace Nat

[rzeta0]

@Eric Wieser i'd welcome your insights on the curly bracket issue, if you have time.

I'll also try rewriting the definition using Nat..

[rzeta0]

out of interest, if I don't import Mathlib then I assume the difference between lemma and theorem is in Lean as a language?

[Shreyas Srinivas]

Lemma is a macro that compiles down to theorem. It's syntax sugar to separate small helper theorems from the rest. Currently it is defined in Mathlib.

[rzeta0]

So changing the definition to Nat. works if I then invoke the lemma with Nat.

I notice H MacBeth's course doesn't use Nat. before her own version of le_or_succ_le

But I'm worried that non-official shouldn't be using Nat. .. should Nat. be reserved for official lemmas/theorems?

[Eric Wieser]

rzeta0 said:

I notice H MacBeth's course doesn't use Nat. before her own version of le_or_succ_le

Can you link to this?

[Jireh Loreaux]

rzeta0 said:

I notice H MacBeth's course doesn't use Nat. before her own version of le_or_succ_le

My suspicion is that this is because, in the context of her course, there's no other type on which such a lemma makes sense. (In other words, Nat is the only type with a SuccOrder that appears in her course. Therefore, no namespace is required.)

On the other hand, in Mathlib, there is a general lemma that would make sense, and so the Nat-specific version should be namespaced.

[rzeta0]

Eric Wieser said:

rzeta0 said:

I notice H MacBeth's course doesn't use Nat. before her own version of le_or_succ_le

Can you link to this?

source: https://github.com/hrmacbeth/math2001/blob/main/Library/Theory/Comparison.lean

example code: https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure.html#sq-ne-two

copied here for convenience:

example {n : ℕ} : n ^ 2 ≠ 2 := by
  have hn := le_or_succ_le n 1   -- < --
  obtain hn | hn := hn
  apply ne_of_lt
  calc
    n ^ 2 ≤ 1 ^ 2 := by rel [hn]
    _ < 2 := by numbers
  sorry