## Stream: general

### Topic: eq_or_ne

#### Benjamin Davidson (May 02 2021 at 03:44):

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 (May 02 2021 at 03:48):

Why not use by_cases a = 0?

#### Benjamin Davidson (May 02 2021 at 03:51):

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 (May 02 2021 at 03:54):

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 (May 02 2021 at 03:54):

I still would use by_cases a=0, swap

#### Adam Topaz (May 02 2021 at 03:55):

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 (May 02 2021 at 05:56):

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 (May 02 2021 at 07:02):

What about defining by_cases_swap?

#### Mario Carneiro (May 02 2021 at 07:23):

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

#### Mario Carneiro (May 02 2021 at 07:24):

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

#### Eric Wieser (May 02 2021 at 08:05):

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

#### Patrick Massot (May 02 2021 at 08:06):

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

#### Rémy Degenne (May 02 2021 at 08:15):

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 (May 02 2021 at 08:25):

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

#### Eric Wieser (May 02 2021 at 08:26):

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

#### Ruben Van de Velde (May 02 2021 at 09:41):

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

#### Benjamin Davidson (May 02 2021 at 10:17):

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

#### Ruben Van de Velde (May 02 2021 at 10:18):

Oh look, I didn't read :)

#### Benjamin Davidson (May 02 2021 at 10:19):

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

#### Benjamin Davidson (May 02 2021 at 10:21):

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

#### Mario Carneiro (May 02 2021 at 11:36):

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 (May 02 2021 at 12:38):

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

#### Benjamin Davidson (May 09 2021 at 04:43):

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 (May 09 2021 at 04:44):

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

#### Benjamin Davidson (May 09 2021 at 04:45):

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 (Jun 09 2021 at 22:58):

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

#### Eric Wieser (Jun 09 2021 at 23:54):

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

#### Mario Carneiro (Jun 10 2021 at 00:01):

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

#7865

#### Benjamin Davidson (Jun 10 2021 at 05:00):

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.

Last updated: Dec 20 2023 at 11:08 UTC