Zulip Chat Archive

Stream: general

Topic: naming of injectivity lemmas


Scott Morrison (Jun 12 2020 at 01:32):

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 (Jun 12 2020 at 01:34):

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

Scott Morrison (Jun 12 2020 at 01:35):

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

Scott Morrison (Jun 12 2020 at 01:37):

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 (Jun 12 2020 at 01:38):

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 (Jun 12 2020 at 02:01):

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

Mario Carneiro (Jun 12 2020 at 02:03):

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 (Jun 12 2020 at 02:03):

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

Mario Carneiro (Jun 12 2020 at 02:04):

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

Mario Carneiro (Jun 12 2020 at 02:05):

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 (Jun 12 2020 at 02:05):

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 (Jun 12 2020 at 02:22):

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

Scott Morrison (Jun 12 2020 at 02:23):

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

Scott Morrison (Jun 12 2020 at 02:25):

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 (Jun 12 2020 at 02:26):

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

Scott Morrison (Jun 12 2020 at 02:26):

What is best?

Yury G. Kudryashov (Jun 12 2020 at 02:27):

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

Yury G. Kudryashov (Jun 12 2020 at 02:28):

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

Mario Carneiro (Jun 12 2020 at 02:42):

there are various reasons why you might want that syntactic form

Mario Carneiro (Jun 12 2020 at 02:42):

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

Mario Carneiro (Jun 12 2020 at 02:42):

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

Mario Carneiro (Jun 12 2020 at 02:44):

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 (Jun 12 2020 at 02:45):

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

Mario Carneiro (Jun 12 2020 at 02:46):

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 (Jun 12 2020 at 02:47):

I think X_injective yields better autocomplete

Scott Morrison (Jun 12 2020 at 02:47):

I like X_injective, too.

Mario Carneiro (Jun 12 2020 at 02:48):

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 (Jun 12 2020 at 02:48):

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

Scott Morrison (Jun 12 2020 at 02:48):

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

Mario Carneiro (Jun 12 2020 at 02:49):

the builtin ones for constructors are fine

Mario Carneiro (Jun 12 2020 at 02:49):

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

Scott Morrison (Jun 12 2020 at 02:49):

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 (Jun 12 2020 at 02:50):

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

Mario Carneiro (Jun 12 2020 at 02:51):

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 (Jun 12 2020 at 02:52):

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 (Jun 12 2020 at 02:53):

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 (Jun 12 2020 at 02:54):

yes

Mario Carneiro (Jun 12 2020 at 02:54):

as in, no multi step proofs

Mario Carneiro (Jun 12 2020 at 02:56):

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 (Jun 12 2020 at 02:56):

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 (Jun 12 2020 at 02:57):

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 (Jun 12 2020 at 02:57):

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

Scott Morrison (Jun 12 2020 at 02:58):

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

Mario Carneiro (Jun 12 2020 at 02:58):

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 (Jun 12 2020 at 02:58):

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 (Jun 12 2020 at 02:59):

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 (Jun 12 2020 at 02:59):

ah, okay

Patrick Massot (Jun 12 2020 at 07:37):

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

Scott Morrison (Jun 14 2020 at 04:28):

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 (Jun 14 2020 at 04:32):

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


Last updated: Dec 20 2023 at 11:08 UTC