Flipping an inequality

Stream: Is there code for X?

[Labyrinth]

Hi, newbie here.

I have a rather simple question: How to turn a goal of the form b \ge a to a goal of the form a \le b?

I've seen that b \ge a is an abbreviation for a \le b, so I thought the following would work (from Glimpse of Lean):

def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

lemma id_le_extraction' : extraction φ → ∀ n, n ≤ φ n := by
  intro hyp n
  induction n with
  | zero => exact Nat.zero_le (φ 0)
  | succ n ih => exact Nat.succ_le_of_lt (by
      calc n ≤ φ n := ih
        _    < φ (n + 1) := by apply hyp; exact lt_add_one n)

lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N := by
  intro hyp N N'
  use max N N'
  constructor
  calc
    N' ≤    max N N'  := Nat.le_max_right N N'
    _  ≤ φ (max N N') := id_le_extraction' hyp (max N N')

However, before even being able to finish the proof, I got an error.
Even more confusingly, it says

'calc' expression has type
  N' ≤ φ (max N N') : Prop
but is expected to have type
  max N N' ≥ N' : Prop

And I have no clue why the max N N' ≥ N' : Prop is "expected".

Any help?

[Labyrinth]

PS: I know that I can do the calc the "other way around" to comply with the inequality in the goal, but I still want to know how to flip the inequality and why it's giving me that error message.

[Labyrinth]

Update: I figured it out, and turns out I'm just terrible at reading... How do I delete an entire topic? lol...

[Kenny Lau]

@Labyrinth btw the idiomatic answer is that \ge is not supported and you should use \le everywhere.

[Labyrinth]

@Kenny Lau Not supported? By what? Lean 4 Web seems to understand it fine

[Kenny Lau]

it means "just don't use it at all"

[Kenny Lau]

not supported by the wealth of theorems that are in mathlib

[Jireh Loreaux]

Kenny, that's not really accurate. Just because our style guidelines say "prefer ≤ to ≥" doesn't mean the latter is "not supported" or you "shouldn't use it".

[Jireh Loreaux]

In fact, ∃ n ≥ N is exactly one of the cases that we use throughout Mathlib.

[Labyrinth]

@Kenny Lau Is it that bad? I can only believe you - I haven't done much in Lean yet to contradict anyone, but shouldn't defining it as an abbreviation for le work just fine?

[Jireh Loreaux]

In fact, a ≥ b is already an abbreviation for b ≤ a, so you should be able to use them (almost) interchangeably everywhere.

[Kenny Lau]

my answer to that would be, abbrev isn't as strong as I would like it to be, it doesn't actually behave as abbreviation everywhere, Lean still actually treats them as different objects

[Kenny Lau]

I would like to see notation everywhere basically

[Labyrinth]

What's the difference between abbrev and notation?

[Jireh Loreaux]

sure, but it's almost the same, and there's no need to confuse new users by saying they should never write ≥.

[Robin Arnez]

Yeah, working with a ≥ b is totally fine but mathlib prefers the spelling b ≤ a. In other words, you can use all of mathlib's API just as well with ≥ with maybe ge_iff_le sometimes but this is simply not done in mathlib

[Weiyi Wang]

To answer one of the original question, you can do this to explicitly flip the inequality

rw [ge_iff_le]

[Jireh Loreaux]

notation is syntactically equal to the original, while abbrev is reducibly definitionally equal to the original.

[Labyrinth]

Is there any situation in which the difference matters?

[Robin Arnez]

Well, when you have an abbrev, you will still see the name (or the notation) of the abbrev and not of the underlying definition. With syntax, writing it either way has literally no noticeable difference

[Robin Arnez]

This sometimes matters for e.g. rw because rw works more on a basis of "syntactical" equality

[Labyrinth]

Well, when you have an abbrev, you will still see the name (or the notation) of the abbrev and not of the underlying definition. With syntax, writing it either way has literally no noticeable difference

So, it affects the "goal view" or whatever it's called(?)

[Jireh Loreaux]

yes, but it's a small-ish difference which I would ignore while you're still learning. Basically, notation is for providing notation (e.g., M →* N for MonoidHom M N) whereas abbrev is for defining two things which are the same under the hood, but you like to have a different name for it, e.g., StrongDual 𝕜 E is an abbreviation for E →L[𝕜] 𝕜 (which itself is notation for ContinuousLinearMap (RingHom.id 𝕜) E E).

[Labyrinth]

Understood. Thanks!

[Kenny Lau]

Labyrinth said:

Is there any situation in which the difference matters?

yes, abbrev creates a new object that Lean unfolds most of the time, and notation means that it's just a shorthand and to Lean they are always the same object

[Kenny Lau]

I think I would still like to insist on the point that mathlib "basically always" prefers <= over >=

[Jireh Loreaux]

Kenny, if Labyrinth were writing a PR, then this would be a relevant comment, but for a new user not trying to contribute to Mathlib at the moment, it's just noise. But sure, you're correct that Mathlib almost always prefers ≤.

[Kenny Lau]

it's relevant if they are trying to use theorems in lean / mathlib and not finding the theorems they want for >= and only finding the <= theorems

[Kenny Lau]

they still basically have to use ge_iff_le to turn every >= into <=

[Jireh Loreaux]

Sure, for finding lemmas it's helpful to know. I take back what I said about your "basically always" comment, as I was conflating it with your earlier comment that ≥ is "not supported" or "shoudn't be used".

[Labyrinth]

Unrelated side note: I love Lean (<insert image of original "I Love Lean!!!" meme but edited to have Lean 4 on top of the drink>). I was trying to use Rocq not long ago, and I could not find proper documentation or tutorials for beginners. The entry barrier was just too strong and academic. Lean 4 has been really easy to pick up, and in just an hour or two I got more progress than in several hours of trying to make Rocq work

[Jason Reed]

I had a pre-edit comment here about thinking that local hypotheses of > or \ge were useful for grw, but I think I've talked myself out of it. It seems like ← suffices to manipulate either side of an inequality in either a hypothesis or goal, even if all goals in sight are < or \le.

import Mathlib

example (a b c : ℝ) : True := by
  have k : a < b := by sorry
  have h : b < c := by sorry
  grw [h] at k
  -- now k : a < c
  sorry

example (a b c : ℝ) : True := by
  have k : a < b := by sorry
  have h : c < a := by sorry
  grw [← h] at k
  -- now k : c < b
  sorry

example (a b c : ℝ) : a < b := by
  have h : a < c := by sorry
  grw [h]
  -- now goal is c < b
  sorry

example (a b c : ℝ) : a < b := by
  have h : c < b := by sorry
  grw [← h]
  -- now goal is a < c
  sorry

Although maybe it is still worth drawing attention to grw as a situation where a < b and b > a are not interchangeable, as the former implies trying to generalized-rewrite a to b and the latter b to a.