bikeshed: mp and mpr

Stream: mathlib4

[Jovan Gerbscheid]

What about .1 and .2 for Iff.mp and Iff.mpr? I think these are pretty widely used and are not that explicit about what's going on.

[Andrew Yang]

I personally prefer .mp and .mpr because of this exact reason.

[Jovan Gerbscheid]

Should we have a linter for this?

[Yaël Dillies]

What I hate about .mp and .mpr is that they are not the same length (+ "modus ponens reverse" is a made up name that no beginner ever guesses). The day you come up with a two characters replacement for .mpr, then sure.

[Jovan Gerbscheid]

.pm

[Johan Commelin]

podus monens!

[Jovan Gerbscheid]

On a more serious note, I think it is more natural to talk about the right and left direction of an Iff. So I would try either .r/.l or .rt/.lt

[Johan Commelin]

What is the t in rt/lt for? Is it to? Or is it the T in rightT and lefT?

[Jovan Gerbscheid]

The latter

[Yaël Dillies]

I prefer .r/.l over .rt/.lt

[Jovan Gerbscheid]

And I presume we would then also add Eq.r and Eq.l

[Jireh Loreaux]

It's not clear to me which way Iff.r/Iff.l are supposed to go.

[Jovan Gerbscheid]

In an ↔, I think it's pretty clear which implication is right (→) and which is left (←)

[Jireh Loreaux]

I'm saying it wasn't to me. I would call that forwards and backwards / reverse.

[Jireh Loreaux]

Obviously the correct solution here is «Iff.→» and «Iff.←» :laughter_tears:

[Jovan Gerbscheid]

I would say it isn't clear which direction Iff.mp goes either. I learned modus ponens as "given a → b and a, we can conclude b". So what does it mean on an ↔?

[Kenny Lau]

what about Iff.ltr and Iff.rtl?

[Jovan Gerbscheid]

Jireh Loreaux said:

Obviously the correct solution here is «Iff.→» and «Iff.←» :laughter_tears:

It seems to work :laughing:

def Iff.«→» (h : a ↔ b) : a → b := h.1

variable (h : a ↔ b)

#check h.«→»

[Markus Himmel]

Jireh Loreaux said:

Obviously the correct solution here is «Iff.→» and «Iff.←» :laughter_tears:

https://github.com/Ivan-Sergeyev/seymour/blob/main/Seymour/Basic/Basic.lean#L28

[Damiano Testa]

The difference between "working" and "reasonable" is prominent here.

[Robin Carlier]

Iff.pleaseBeTheDirectionINeed and Iff.theOtherDirection

[Kenny Lau]

what if we had a smart elaborator like ▸ that can figure out the direction by itself

[Jireh Loreaux]

Jovan Gerbscheid said:

I would say it isn't clear which direction Iff.mp goes either

Sure, agreed.

[Damiano Testa]

What I actually like about .mp and .mpr is that you can "try out .mp and if that doesn't work, just type r".

[Jovan Gerbscheid]

m + p + r and r + backspace + l are both 3 buttons

[Damiano Testa]

Once you have written .mp, it is only one more character to try out the other...

[Jovan Gerbscheid]

But writing .mp takes so many characters...

[Jireh Loreaux]

This is in core right? Why are we arguing about changing it? :laughing:

[Jovan Gerbscheid]

I want to add def Iff.r {p q : Prop} (h : p ↔ q) : p → q := h.1 to Mathlib.Init/Mathlib.Logic

[Jovan Gerbscheid]

And then we can talk to core later

[Jireh Loreaux]

(Just FYI, I'd be surprised if core wants to make that change.)

[Yaël Dillies]

Actually I think core should accept that change, on the basis that mp and mpr are made-up names that were never properly understood by beginners

[Jovan Gerbscheid]

(should this conversation be moved to a better named thread?)

[Markus Himmel]

Jovan Gerbscheid said:

I want to add def Iff.r {p q : Prop} (h : p ↔ q) : p → q := h.1 to Mathlib.Init/Mathlib.Logic

FWIW, if you showed me the name Iff.r and asked me what it is, I would guess "right-to-left" or "reverse" and therefore would expect the other direction.

[Markus Himmel]

I think if you really want one-symbol names, then 1 and 2 are pretty close to optimal.

[Jovan Gerbscheid]

I think the point here is not to have a name that everyone will understand/guess immediately. Instead the point is to have a name that everyone can understand after having seen it. And I think .r and .l is an improvement in this aspect. .mp also has the problem of excluding people that aren't as much into logic.

[Jovan Gerbscheid]

Markus Himmel said:

I think if you really want one-symbol names, then 1 and 2 are pretty close to optimal.

The second aim of the name is that if you read it, you know what you are reading. When I look at a random proof script, and see .1 I won't immediately know that it is Iff.mp. But if I see .r, I will. (appart from the fact that Setoid.r exists :upside_down: )

[Markus Himmel]

I don't know. The benefits seem quite marginal to me. I don't see us deprecating mp and mpr for this, and not deprecating them and having three ways to write each direction wouldn't really be an improvement either in my opinion.

[Eric Wieser]

A suggestion I made in the past was to add a coercion so that the options are h x and h.symm x

[Artie Khovanov]

That sounds incredibly unintuitive to me

[Jireh Loreaux]

That sounds like an absolute nightmare for teaching.

[Kevin Buzzard]

But it's so much more intuitive than all other suggestions above! I love it! The direction is completely unambiguous.

[Jovan Gerbscheid]

But with that option, how does one apply h.mp?

[Kevin Buzzard]

apply ⇑h

[Kevin Buzzard]

Now I've seen this option I can't unsee it :-)

[Kevin Buzzard]

(and just to be clear I totally agree with it being a nightmare for teaching! But I absolutely love it all the same)

[Edward van de Meent]

tbh i feel like this is about as ambiguous as all the other options

[Andrew Yang]

I think this will make h ambiguous (it either means A ↔ B or A → B)

[Edward van de Meent]

one might argue that since in the applied form h x, the argument is on the right, clearly x's type is the right hand side of h

[Kevin Buzzard]

Andrew Yang said:

I think this will make h ambiguous (it either means A ↔ B or A → B)

Just like how e : R ≃+* S is ambiguous (it either means R ≃+* S or R →+* S)?

[Kevin Buzzard]

I'm not pushing for it, I don't think it will fly, but I personally think it's much better than all this .mp nonsense

[Filippo A. E. Nuccio]

But why should we deprecate anything? This discussion clearly shows that some people love .mp /.mpr, some like them, some not so much, others hate it. Why not leaving things as they are, leaving the option of .mp and . 1?

[Kim Morrison]

Yeah, let's please not doing anything here. .mp and .mpr are never going away, and anything we add just fractures the conventions and introduces confusions. This boat has sailed.

[Notification Bot]

53 messages were moved here from #mathlib4 > Proposal: Triple by Johan Commelin.