eq_or_ne

Stream: general

[Benjamin Davidson]

Would these be a welcome addition? I find myself writing by_cases ha : a ≠ 0 pretty often, and these would be convenient if one wanted to use rcases or didn't want to have to rw not_not at ha. I think these would also be easier to find by "guessing the name and using the autocomplete tool."

import logic.basic

variables {α : Type*} (a b : α)

lemma eq_or_ne : a = b ∨ a ≠ b := em $ a = b

lemma ne_or_eq : a ≠ b ∨ a = b := (eq_or_ne a b).symm

lemma eq_zero_or_ne_zero [has_zero α] : a = 0 ∨ a ≠ 0 := eq_or_ne a 0

lemma ne_zero_or_eq_zero [has_zero α] : a ≠ 0 ∨ a = 0 := ne_or_eq a 0

[Adam Topaz]

Why not use by_cases a = 0?

[Benjamin Davidson]

I do, but sometimes I find that it's more convenient to deal with the ne case first (i.e. if it is the trivial one).

[Benjamin Davidson]

This is really nothing more than a question of "are they worth adding for the convenience," there's no brilliance to these lemmas at all.

[Adam Topaz]

I still would use by_cases a=0, swap

[Adam Topaz]

IMO I don't mediately see a use case for these, but perhaps someone else knows of a situation where they would be worth it

[Mario Carneiro]

I don't think it is worth it, except possibly (em p).swap if we don't already have it. The others are just substitution instances of lemmas with longer names

[Yaël Dillies]

What about defining by_cases_swap?

[Mario Carneiro]

I don't see any advantage to defining two tactics in a row as a composite tactic. Just use two tactics

[Mario Carneiro]

More tactics means more to learn. It is better to keep tactics orthogonal so they can be used compositionally

[Eric Wieser]

eq_or_ne would be nice because it would produce hypotheses that use a ≠ b instead of not (a = b)

[Patrick Massot]

One is a notation for the other so it doesn't change anything, right?

[Rémy Degenne]

you cannot do h.symm on h : not (a = b), but you can on h : a ≠ b. I very often write rw ← ne.def at h after a by_cases h : a = b, when a = b happens to be more convenient in the first case, but some lemma I want to use needs b ≠ a in the second case.

[Eric Wieser]

Right. It's not just notation, docs#ne is a type alias.

[Eric Wieser]

Although it's been discussed before that we should just teach by_cases to perform that rewrite automatically

[Ruben Van de Velde]

Also, you can do obtain (rfl|h) := eq_or_ne a b,, which by_cases can't (as far as I know)

[Benjamin Davidson]

Exactly, that's what I was referring to above when I mentioned rcases.

[Ruben Van de Velde]

Oh look, I didn't read :)

[Benjamin Davidson]

I'm glad to see we had the same train of thought :)

[Benjamin Davidson]

And the other aspect of convenience I had in mind is what Eric mentioned about having a ≠ b instead of ¬ a = b.

[Mario Carneiro]

you cannot do h.symm on h : not (a = b), but you can on h : a ≠ b.

You can do ne.symm h though, so this isn't a major inconvenience

[Rémy Degenne]

I did not realize that. Thanks for the tip, that will same me the rw line.

[Benjamin Davidson]

What is the verdict on this? I am fine following Mario's opinion, but there seems to have been some feedback in favor of adding eq_or_ne.

[Mario Carneiro]

It's fine to add it, I don't think it's particularly necessary but mathlib is not minimalist

[Benjamin Davidson]

Personally, since my original post, I have already had two circumstances where it would have been very convenient to have such a lemma to use with obtain/rcases.

[Eric Rodriguez]

sorry to necro this, but is there any reason we did this but _only_ for Prop?

[Eric Wieser]

docs#eq_or_ne - gosh, we really did do that.

[Mario Carneiro]

probably someone forgot to declare the variables and it picked up the variable declaration which is a Prop since it's logic.basic

[Eric Rodriguez]

#7865

[Benjamin Davidson]

I'm so sorry, that's exactly what happened - I didn't realize that a and b were declared as Prop. My bad, and thank you for catching and fixing this Eric.