Zulip Chat Archive

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

Eric Rodriguez (Jun 10 2021 at 00:10):

#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