Zulip Chat Archive

Stream: general

Topic: naming of injectivity lemmas


view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 12 2020 at 01:34):

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

view this post on Zulip Scott Morrison (Jun 12 2020 at 01:35):

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

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:03):

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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:04):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jun 12 2020 at 02:22):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 12 2020 at 02:26):

What is best?

view this post on Zulip Yury G. Kudryashov (Jun 12 2020 at 02:27):

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

view this post on Zulip Yury G. Kudryashov (Jun 12 2020 at 02:28):

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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:42):

there are various reasons why you might want that syntactic form

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:42):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:45):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:47):

I think X_injective yields better autocomplete

view this post on Zulip Scott Morrison (Jun 12 2020 at 02:47):

I like X_injective, too.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:49):

the builtin ones for constructors are fine

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:49):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:54):

yes

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:54):

as in, no multi step proofs

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:57):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jun 12 2020 at 02:59):

ah, okay

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 13 2021 at 17:42 UTC