ge_max_iff

Stream: mathlib4

[Patrick Massot]

Speaking of teaching files and max, I also always have

lemma ge_max_iff {α : Type*} [LinearOrder α] {p q r : α} : r ≥ max p q  ↔ r ≥ p ∧ r ≥ q :=
  max_le_iff

it order to allow rewriting of N ≥ max N₁ N₂ in all my elementary analysis exercises. Should we add this? The issue is that it begins a path full of lemma duplication.

[Sébastien Gouëzel]

I don't think we should add this. There's a reason why all lemmas are written with le in mathlib, to avoid duplication.

[Floris van Doorn]

My first instinct is that we don't want this in Mathlib.

But it might be nice to collect things that make Lean more beginner-friendly. We could make a Teaching folder inside Mathlib? Or a Teaching repo depending on Mathlib?

[Violeta Hernández]

I don't think there's much didactic value here either, "stick to one comparison operator" is a pretty reasonable convention that shouldn't be confusing to anyone past elementary school.

[Patrick Massot]

Did you attend any course in real analysis already? The combination ∃ N, ∀ n ≥ N, ... is pretty common there. And ∃ N, ∀ N ≤ n, ... doesn’t work so well.

[Eric Wieser]

Isn't rw [max_le_iff] supposed to work even on ≥ because it's reducible? (indeed it does not actually work)

[Patrick Massot]

It certainly does not work, other we wouldn’t be having this conversation.

[Violeta Hernández]

Patrick Massot said:

Did you attend any course in real analysis already? The combination ∃ N, ∀ n ≥ N, ... is pretty common there. And ∃ N, ∀ N ≤ n, ... doesn’t work so well.

I have, and I agree that this notation is convenient with pen and paper (indeed I often find myself writing ε > 0 out of habit). But the entire point Lean is that you have to write down things in full detail, so I don't think that doing the mental switch to writing ∃ N, ∀ n, N ≤ n → ... is complicated or unexpected.

[Peter Nelson]

Violeta Hernández said:

Patrick Massot said:

Did you attend any course in real analysis already? The combination ∃ N, ∀ n ≥ N, ... is pretty common there. And ∃ N, ∀ N ≤ n, ... doesn’t work so well.

I have, and I agree that this notation is convenient with pen and paper (indeed I often find myself writing ε > 0 out of habit). But the entire point Lean is that you have to write down things in full detail, so I don't think that doing the mental switch to writing ∃ N, ∀ n, N ≤ n → ... is complicated or unexpected.

A reality check : the notations > and ≥ are not just 'convenient' - they are part of normal mathematics, and nothing about them is lacking detail. Of course everyone knows they can be completely avoided if you really want to to, and for various reasons that's actually a good idea when formalizing.

But we're the weird ones for avoiding them! These considerations matter when teaching.

[Ruben Van de Velde]

Fun fact: you can redefine ∀ n ≥ N such that it uses le internally, but my change to do that wasn't accepted

[Jovan Gerbscheid]

Should rw be changed so that it can rewrite this? I could imagine some tag @[reduce_in_rewrite] that specifies that rw indexing should treat the head GE.ge as if it were LE.le.

[Patrick Massot]

That would be great.

[Eric Wieser]

Should rw just always unfold reducible definitions?

[Jovan Gerbscheid]

The issue is that it can't run whnf on the sub-expressions, because it may contain bound variables.

But instead it could check whether the head constant is reducible, and if its definition is an application of another constant, then replace it with that.