is_regular.inj

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is something like the lemma below already in mathlib?

import algebra.regular.basic

lemma is_left_regular.inj {α} [has_mul α] {a : α} (hx : is_left_regular a) {b c : α} :
  a * b = a * c ↔ b = c :=
⟨λ h, hx h, congr_arg _⟩

I know that I was the one who defined regular elements, but at the time, I had a much more limited understanding of Lean.

If the lemma above (and its various sided/additive forms) is not in mathlib, should I PR it?

Thanks!

[Damiano Testa]

(Side comment: now that dot-notation works better, is_left_regular can be defined as

def is_left_regular (c : R) := ((*) c).injective

:smile: )

[Damiano Testa]

I PRed in the end. The deciding factor was that I could not wait to shorten the definitions of regular using dot-notation! :upside_down:

#16312

[Eric Wieser]

Since when did lean support that new dot notation?

[Alex J. Best]

3.47 (5 days ago) I believe, thanks to @Kyle Miller

[Kyle Miller]

And for mathlib, today!

#16315 is a small PR to add dot notation for modus tollens (function.mt and function.mtr)

[Junyan Xu]

What's the point of function.mt given it could never save a character (edit: see below for an example showing this is false)? And should function.mtr simply be mtr for consistency?

[Damiano Testa]

It could save characters, if you avoid needing parentheses.

[Kyle Miller]

@Junyan Xu I don't think saving keystrokes should be a primary consideration in most cases, especially if the difference is only a handful of keystrokes, or in this case none at all.

Here are a few reasons that come to mind justifying function.mt:

• Perhaps function.mt should replace mt entirely, since a two-letter function name is polluting the global namespace (it's plausible mt could be a local).
• Dot notation is familiar with iff, and this makes implications behave similarly (though iff uses h.not.symm or h.not.mpr for its modus tollens).
• h1.mt h2 has different parsing rules from mt h1 h2, and one might like the aesthetics of dot notation more. I like it because I think of modus tollens as a transformation of the implication.

[Eric Wieser]

It would be cool if dot notation on Prop → Prop tried docs#implies as the namespace first

[Eric Wieser]

implies.mt feels like a much less weird name

[Junyan Xu]

I think the other two are good points, but I can't make sense of

Dot notation is familiar with iff, and this makes implications behave similarly (though iff uses h.not.symm or h.not.mpr for its modus tollens).

Can you explain? What does it have to do with iff?

Damiano Testa said:

It could save characters, if you avoid needing parentheses.

Can you give an example? If it's not a single name you'd need to enclose it in () to write .mt right?

[Damiano Testa]

I meant something like f (mt g) can now be spelled f g.mt: 6 chars instead of 8! :upside_down:

[Damiano Testa]

Actually, more than decreased number of characters, I think that this can be slightly more readable. At least, it is good to have the option!

[Junyan Xu]

Nice! I think I never encountered unapplied mt _ so I didn't realize that's a possibility.

[Junyan Xu]

Regarding iff: I think it makes sense to introduce a coercion from iff to implies (maybe an equiv_like instance; I don't think we have these currently), analogous to the equiv.to_fun cocercion.

[Kyle Miller]

@Junyan Xu It has to do with iff since we already interact with iff using dot notation frequently, and so it makes things more consistent if implications can use dot notation for similar tasks.

[Kyle Miller]

Junyan Xu said:

Regarding iff: I think it makes sense to introduce a coercion from iff to implies (I don't think we have this currently), analogous to the equiv.to_fun cocercion.

This idea comes up every once in a while (I think @Eric Wieser and I were the last to propose it), but there is relatively strong opposition.

If I remember correctly, it would be acceptable (or rather, it wouldn't immediately be unacceptable) if it were hidden behind a locale, since then it wouldn't lead to students being confused about implications vs iffs.

[Junyan Xu]

So IIUC, you mean that we use dot notations .mp, .mpr (which are, specifically, structure projections) to get implies/function from iff, so it's natural to concatenate dot notations after .mp(r) which necessitates more dot notations for implies/function. I agree this is also a good point!

[Kyle Miller]

Eric Wieser said:

It would be cool if dot notation on Prop → Prop tried docs#implies as the namespace first

Yes, it would be. This might have to wait until the mathlib port is complete to simplify coordinating changes to Lean 3 and 4, but if Lean 4 adopts this feature, I'll happily backport it to Lean 3.

Here's a general version I was thinking about before for namespaces:

• If it's a non-dependent Prop-valued pi, then implies, otherwise
• If it's a dependent Prop-valued pi, then forall, otherwise
• If it's a non-dependent pi, then function, otherwise
• If it's a dependent pi, then pi.

This also defines the search order if the name in that namespace does not exist. In particular, it's a diamond, and these are the possible search orders:

• implies, forall, function, pi
• forall, pi
• function, pi
• pi

[Kyle Miller]

It might not be necessary to have all four. (For example, perhaps forall and implies could be merged.)

[Kevin Buzzard]

I am torn between "this is a super-cool feature" and "this will be really confusing for newcomers"