naming of injectivity lemmas

Stream: general

[Scott Morrison]

I'd like to bring a bit of order to the naming of injectivity lemmas. Currently in mathlib lemmas with names ending in _inj come in three flavours

1. f x = f y → x = y
2. f x = f y ↔ x = y
3. injective f

There are also lemmas automatically generated for constructors of inductive types, which are of type 1, but with names ending .inj.
There are also some lemmas in mathlib of type 2, but with names ending _inj_iff.

[Scott Morrison]

And also lemmas of type 3 with injective in the name!

[Scott Morrison]

also a few stragglers, like type 2 lemmas with LHS and RHS reversed...

[Scott Morrison]

Proposals, in descending order of appeal to me:

1. all iff lemmas get renamed to use inj_iff
2. where possible change _inj to .inj and _inj_iff to .inj_iff
3. rename all injective lemmas to use the full word injective in the name (alternatively, change them all to just inj, and not distinguish types 1 and 2)

[Scott Morrison]

Proposal 2 to appealing because:

• it would match the automatically generated .inj lemmas for constructors
• it would make it easier for library_search to discard these lemmas (which are rarely useful), without having to process strings (which is too slow).

[Mario Carneiro]

The naming convention here is supposed to use inj exclusively for (1) or (2) and injective for (3)

[Mario Carneiro]

Probably we are being inconsistent about use of inj_iff but I would prefer to use inj_iff iff both versions (1) and (2) exist

[Mario Carneiro]

if only (2) exists then there is no problem and we can use inj

[Mario Carneiro]

I think most instances of (1) are inherited from core

[Mario Carneiro]

It seems odd to throw these theorems out though. They don't appear to be any less useful than any other basic algebra lemmas

[Mario Carneiro]

It's true that they aren't well suited for backwards reasoning but that shouldn't be a problem for library_search which is only looking for one step proofs in any case

[Scott Morrison]

I wasn't proposing throwing anything out, just renaming.

[Scott Morrison]

Maybe I will start with the low hanging fruit: using injective in the name if and only if the conclusion has injective.

[Scott Morrison]

To clarify the "no throwing out" agenda, my preference would be that every iff injectivity lemma was renamed to to contain inj_iff, for consistency, and that typically (always?) the corresponding unidirectional inj lemma exists as well.

[Scott Morrison]

Regarding injective lemmas, we seem to be very inconsistent between X_injective, injective_X, and sometimes also X.injective.

[Scott Morrison]

What is best?

[Yury G. Kudryashov]

Why not reformulate f x = f y → x = y as injective f?

[Yury G. Kudryashov]

It's almost the same (injective uses {{x y}})

[Mario Carneiro]

there are various reasons why you might want that syntactic form

[Mario Carneiro]

for one thing, if f would be a lambda then this doesn't come out very cleanly

[Mario Carneiro]

for example a + b = a + c -> b = c

[Mario Carneiro]

To clarify the "no throwing out" agenda, my preference would be that every iff injectivity lemma was renamed to to contain inj_iff, for consistency, and that typically (always?) the corresponding unidirectional inj lemma exists as well.

I'm arguing for the opposite of this: get rid of the unidirectional lemmas and call all the iff statements inj

[Mario Carneiro]

I'm not sure what the argument for the unidirectional versions is

[Mario Carneiro]

Scott Morrison said:

Regarding injective lemmas, we seem to be very inconsistent between X_injective, injective_X, and sometimes also X.injective.

I have a preference for X_injective, but I recognize that the symbol reading convention would have us name it injective_X

[Mario Carneiro]

I think X_injective yields better autocomplete

[Scott Morrison]

I like X_injective, too.

[Mario Carneiro]

Scott Morrison said:

I wasn't proposing throwing anything out, just renaming.

I mean throwing out of the strike zone of library_search

[Mario Carneiro]

isn't that what you are proposing? You want a way to filter these lemmas by name

[Scott Morrison]

Okay --- getting rid of unidirectional lemmas sounds like a great idea, except for the fact that inductive types build these automatically.

[Mario Carneiro]

the builtin ones for constructors are fine

[Mario Carneiro]

they are well namespaced and required for some automatic constructions so we can't touch them

[Scott Morrison]

Ah, I see. Yes. I've just never seen an useful case where you want library_search to find an inj lemma, and the problem is that they always apply on any eq goal, and then solve_by_elim wastes time on the subsequent goals.

[Scott Morrison]

I tried dropping all .inj lemmas (which you can do without processing strings), and it slightly speeds up the test file.

[Mario Carneiro]

I would prefer something a bit more agnostic. For example, if application of the lemma yields a subgoal with metavariables, then all goals must be achievable by assumption

[Scott Morrison]

So it seems we are converging on the following:

1. lemmas should have injective in the name iff they have injective in the conclusion
2. X_injective is preferable to injective_X.
3. Dropping unidirectional inj lemmas in favour of bidirectional ones.

[Scott Morrison]

Mario Carneiro said:

I would prefer something a bit more agnostic. For example, if application of the lemma yields a subgoal with metavariables, then all goals must be achievable by assumption

Here you're saying in particular "by assumption" as opposed to solve_by_elim?

[Mario Carneiro]

yes

[Mario Carneiro]

as in, no multi step proofs

[Mario Carneiro]

You might have to do something slightly more complicated than straight assumption since you may have to try different assumptions in order to make the other hypotheses work

[Scott Morrison]

but you're only wanting this restriction if there is a subgoal with metavariables? I don't think I'm understanding the motivation here.

[Mario Carneiro]

The right way to test f x = f y -> x = y against the current goal is to match f x = f y against the hypothesis and then match the goal

[Mario Carneiro]

i.e. it is a forward reasoning step not backward

[Scott Morrison]

yes --- that's why I was thinking injectivity lemmas are generally outside the purview of library_search

[Mario Carneiro]

but since library_search is set up to do backward reasoning, the nearest approximation to this is to switch to forward reasoning mode if it looks like backward reasoning isn't going so well

[Scott Morrison]

most of the bidirectional inj lemmas should probably be @[simp], and you shouldn't be resorting to library_search until after simp is done.

[Mario Carneiro]

true, but I'm imagining a situation where the user has actually typed theorem foo (h : f x = f y) : x = y := by library_search

[Scott Morrison]

ah, okay

[Patrick Massot]

Whatever you decide and refactor here, it would be nice to remember to add it to the naming convention guide.

[Scott Morrison]

I haven't actually got very far on the mathlib refactor, but I've recorded the ideas here in https://github.com/leanprover-community/leanprover-community.github.io/pull/60.

[Bryan Gin-ge Chen]

It looks like that file could use some general cleanup. There's some duplication within the file and also with https://leanprover-community.github.io/contribute/style.html