naming contest

Stream: general

[Anne Baanen]

Any suggestions for a conciser name?

lemma is_basis_to_matrix_mul_linear_map_to_matrix_mul_is_basis_to_matrix
  (hb : is_basis b) (hb' : is_basis b') (hc : is_basis c) (hc' : is_basis c') :
  hc.to_matrix c' ⬝ linear_map.to_matrix hb' hc' f ⬝ hb'.to_matrix b = linear_map.to_matrix hb hc f := sorry

[Eric Wieser]

Can that be split into two lemmas?

lemma is_basis_to_matrix_mul_linear_map_to_matrix
  (hb : is_basis b) (hb' : is_basis b') (hc : is_basis c) (hc' : is_basis c') :
  hc.to_matrix c' ⬝ linear_map.to_matrix hb' hc' f = linear_map.to_matrix hb' hc f := sorry

and a similar linear_map_to_matrix_mul_is_basis_to_matrix?

Or am I missing something there?

[Anne Baanen]

Ah good point, I was thinking about how to describe "basis change" in Lean.

[Anne Baanen]

But we can do it one side at a time.

[Anne Baanen]

Still quite a long name :/

[Gabriel Ebner]

You could turn one of the underscores into a dot and put it in the is_basis namespace.

[Gabriel Ebner]

Eric's version also looks like a good simp lemma.

[Yury G. Kudryashov]

I'm going to review API around null_measurable, and I need 4 names:

• null measurable set;
• null measurable function;
• the measurable_space structure that corresponds to null_measurable_set;
• the type tag for "α with measurable_set = null_measurable_set".
  For the first two, null_measurable_set and null_measurable look like obvious choices. What about the other two?

[Sebastien Gouezel]

Just for the record, I know that we need a refactor of the Bochner integral (and I'm planning to do it in a few months, when I have just a little bit of free time), for the following reason. Currently, our version only works when the target space is second countable (this is the setting in which every measurable function can be approximated by simple functions). However, there is a very important application of integral where this is not the case: if you consider a continuous linear operator on a Banach space, then its spectral projections are defined by Cauchy-like integral formulas, so we need integrals there -- and such spaces of operators are never second-countable.

The most general setting to define the integral of a function f is to assume that there is a measurable function g, taking its values in a second-countable subspace, and coinciding almost everywhere with f. (see https://en.wikipedia.org/wiki/Bochner_measurable_function). The name for this would probably be strongly_ae_measurable, or something like that. And it covers the use-case above of spectral projections. So I am planning to generalize the Bochner integral, replacing the ae_measurable assumption with strongly_ae_measurable (which coincides with ae_measurable when the target space is second-countable).

This does not really answer your questions, but I think this is something to keep in mind for any measure theory API review.

[Sebastien Gouezel]

As for your questions, null_measurable_set is great. null_measurable is ok for the function (but in the end it is equivalent to ae_measurable, so I am not so sure we need the two names). Then, you could go with measurable_space_completion μ for the completed sigma-algebra, and is_complete_measurable_space μ for the fact that all null measurable sets are measurable (as in https://en.wikipedia.org/wiki/Complete_measure)

[Yury G. Kudryashov]

In what generality null_measurable = ae_measurable?

[Yury G. Kudryashov]

In any case, I think that we should have better API for null_measurable_sets.

[Sebastien Gouezel]

Yury G. Kudryashov said:

In what generality null_measurable = ae_measurable?

I guess when the target space is second-countable.

[Sebastien Gouezel]

Yury G. Kudryashov said:

In any case, I think that we should have better API for null_measurable_sets.

Yes, definitely!

[Andrew Yang]

What should the pasting law for pullbacks be called?
In particular

variables {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ X₂) (g₁ : X₂ ⟶ X₃) (f₂ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃)
variables (i₁ : X₁ ⟶ Y₁) (i₂ : X₂ ⟶ Y₂) (i₃ : X₃ ⟶ Y₃)
variables (h₁ : i₁ ≫ f₂ = f₁ ≫ i₂) (h₂ : i₂ ≫ g₂ = g₁ ≫ i₃)

def pasting_law (H : is_limit (pullback_cone.mk _ _ h₂)) :
  is_limit (pullback_cone.mk _ _ (show i₁ ≫ f₂ ≫ g₂ = (f₁ ≫ g₁) ≫ i₃,
    by rw [← category.assoc, h₁, category.assoc, h₂, category.assoc])) ≃
  is_limit (pullback_cone.mk _ _ h₁) := sorry

And the implications in both directions that will be proved before this.

[Yury G. Kudryashov]

I'm going to add Prop versions of docs#fintype and docs#encodable. How should I call them?

[Johan Commelin]

_root_.finite and _root_.countable?

[Mario Carneiro]

doesn't docs#countable already exist? guess not

[Kevin Buzzard]

Funnily enough an undergraduate and I wrote _root_.countable at Xena on Thursday but it's on the student's laptop and I don't know their name :-)

[Yury G. Kudryashov]

I already have _root_.countable with some instances. I'll add glue code and PR it over week-end.

[Yury G. Kudryashov]

I'm going to formalize a few versions of the Phragmén–Lindelöf principle. Mathlib naming convention leads to very long names. What do you think about names like phragmen_lindelof.(shape), where (shape) is one of sector, first/second/third/fourth_quadrant etc?

[Yury G. Kudryashov]

(and now I see that I forgot to polish _root_.countable)

[Sebastien Gouezel]

Looks good to me.

[Eric Wieser]

What should the additive version of div_inv_monoid be called? docs#sub_neg_monoid exists, but @[to_additive] thinks it should be called sub_neg_add_monoid, as demonstrated by docs#function.injective.sub_neg_add_monoid.

[Eric Wieser]

/poll With or without add_?

• sub_neg_monoid, keeping the existing class name and fixing to_additive to match
• sub_neg_add_monoid, changing the existing class name and leaving to_additive alone

[Eric Wieser]

cc @Anne Baanen, since I think you added this originally

[Junyan Xu]

/poll What should $V^G$ be called for a G-representation V? (Context)

• fixed_space
• invariants

[Junyan Xu]

Context: https://github.com/leanprover-community/mathlib/pull/11207/files#diff-92d45ccdf14ad18f844dc7d0faddeae9c2089a7205c7ef33aad57f674ec8b61e

[Kevin Buzzard]

cohomology.H 0 G V ;-) (this is not a correct answer -- there should probably just be an isomorphism...)

[Reid Barton]

invariants seems good also because the dual guy is called the coinvariants (what else?)

[Yury G. Kudryashov]

How should I call the following lemmas?

import data.set.finite

open set
variables {α β ι : Type*} [fintype ι] {π : ι → Type*}

example {s : set (α × β)} : finite s ↔ finite (prod.fst '' s) ∧ finite (prod.snd '' s) :=
⟨λ h, ⟨h.image _, h.image _⟩,
  λ h, (h.1.prod h.2).subset $ λ x h, ⟨mem_image_of_mem _ h, mem_image_of_mem _ h⟩⟩

example {s : set (Π i, π i)} : finite s ↔ ∀ i, finite (eval i '' s) :=
⟨λ h i, h.image _, λ h, (finite.pi h).subset $ subset_pi_eval_image _ _⟩

[Yury G. Kudryashov]

Probably, the name of the first lemma should include finite and prod. There is also a reasonable lemma

example {s : set α} {t : set β} : finite (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ finite s ∧ finite t

[Eric Wieser]

set.finite_of_prod_iff, using the rule "of refers to the type of arguments"?

[Yaël Dillies]

I would name the third one set.prod_finite_iff.

[Floris van Doorn]

of sounds weird to me, since it's the type we're talking about.
I like set.finite_prod_iff for both the first and the third one, and I'm not sure how to best disambiguate them. Both of them are follow the example of existing names. E.g. docs#measurable_pi_iff , docs#measurable_prod for the first one, and docs#set.finite_union / docs#filter.tendsto_prod_iff for the other one (we seem to be quite inconsistent about whether to append iff to a name).

[Eric Wieser]

Well, when we usually use of for proofs, it also refers to the type

[Eric Wieser]

I think we also sometimes use docs#of_fintype in names, which is referring to a non-Prop type

[Yury G. Kudryashov]

In #13619 I swap LHS with RHS and describe the new LHS in the name. Not sure if it is a good solution.

[Yury G. Kudryashov]

How should I call the following definition?

def name_me (f : α → β → γ) : option α → option β → option γ
| none none := none
| none (some b) := none
| (some a) none := none
| (some a) (some b) := some (f a b)

Equivalently, name_me f o₁ o₂ = o₁.bind (λ a, o₂.map (f a)).

[Yaël Dillies]

This already exists

[Yury G. Kudryashov]

How is it called?

[Yaël Dillies]

Ah no, I thought it was docs#option.lift_or_get but it doesn't do the same thing when one of the arguments is none.

[Kyle Miller]

example {α β γ : Type*} (f : α → β → γ) (x : option α) (y : option β) :
  name_me f x y = f <$> x <*> y :=
begin
  cases x; cases y; refl,
end

[Yaël Dillies]

What does docs#with_top.has_add do?

[Kyle Miller]

This is what applicative functors let you do in a generalized way for any number of arguments (keep adding <*>).

[Yaël Dillies]

Yeah that's what it does.

[Eric Wieser]

Note the f <$> x <*> y version only works when α β γ are in the same universe

[Yaël Dillies]

A good name would be option.map\2 but indeed you can just write it out monadically.

[Yury G. Kudryashov]

Yes, I wanted to prove some lemmas about this combinator, then use it for (+) and (*) on with_top.

[Yaël Dillies]

Yeah... but if we perform the functor refactor we talked about, that wouldn't be a problem anymore.

[Eric Wieser]

it was never clear to me whether that refactor would actually work

[Kyle Miller]

monadically

(n.b. this uses the weaker notion of an applicative functor, no need for monads)

[Yaël Dillies]

What are you fearing? I thought about it and couldn't see anything wrong.

[Eric Wieser]

Typeclass search not handling out_params well enough

[Yaël Dillies]

Yury, Yakov already wanted to do that, and it turns out that this is not a good global instance because sometimes you want the top element to not do anything

[Yaël Dillies]

Let me dig out the PR...

[Yury G. Kudryashov]

We already have docs#with_top.has_add and docs#with_top.mul_zero_class

[Yaël Dillies]

Ah right, it was subtraction. #8889

[Mauricio Collares]

I'd expect something close to Haskell's naming (liftA\2)

[Anne Baanen]

For the name, I would follow Haskell and use some variant of lift2

[Yaël Dillies]

Yeah so 0 * top = 0, not 0 * top = top.

[Yury G. Kudryashov]

Yes, lift₂ will be used for the else branch.

[Violeta Hernández]

We currently have two duplicate theorems docs#set.insert_nonempty and docs#set.nonempty_insert. My PR #14884 is meant to ditch one in favor of the other, but I was asked to do a poll to see which one is preferred.

[Violeta Hernández]

Consider that:

• we also have lemmas docs#set.univ_nonempty and docs#set.singleton_nonempty
• insert_nonempty is currently the most used of the two (though not by a huge margin)

[Violeta Hernández]

/poll What name should we use?

• insert_nonempty
• nonempty_insert

[Kyle Miller]

This is the old debate about whether the naming for p x is x_p when p is a Prop-valued predicate that is amenable to dot notation, and, as far as I know, we haven't reached consensus about this yet. It would be nice to have #naming prescribe something.

[Kyle Miller]

Maybe this is a decision that can be made per predicate and documented in the predicate's docstring. It seems (though I haven't measured) that set.nonempty most often uses the *_nonempty convention.

[Violeta Hernández]

I also think this decision should be made on a per-predicate basis. I'd be somewhat annoyed if I had to rename e.g. one_to_game to to_game_one (example from one of my PRs). No doubt there's a similar situation going the other way (though I'm awful at coming up with examples for things like this).

[Eric Wieser]

Just to relink the old thread on this type of naming issue: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.23naming.20and.20dot.20notation/near/246520191

[Eric Wieser]

For what it's worth, I'd expect it to be called to_game_one to match all the coe_one lemmas we have

[Violeta Hernández]

Unfortunate but understandable

[Stuart Presnell]

#15061 adds two recursion principles for P : ℕ → ℕ → Sort* for which I'm looking for naming suggestions:

• strong_sub_recursion: if for all a b : ℕ we can extend P from the rectangle strictly below (a,b) to P a b, then we have P n m for all n m : ℕ.
  This was originally proved and named by @Chris Birkbeck in #14828 (which is now closed)

• pincer_recursion: if we have P i 0 and P 0 i for all i : ℕ, and for any x y : ℕ we can extend P from (x,y+1) and (x+1,y) to (x+1,y+1), then we have P n m for all n m : ℕ.
  pincer_recursion is just a name I made up for this. Does anyone know if this is already known by another name? Or can anyone suggest a better name for this?

[Stuart Presnell]

Another naming question: #15072 defines multichoose which (by contrast with choose) counts the number of multisets of cardinality k from a type of cardinality n, or equivalently the number of ways to select k items (up to permutation) from n items with replacement. (This is another step toward getting @Huỳnh Trần Khanh's #11162 "stars and bars" tidied up and finalised.)

Some reviewers have suggested that the name multichoose (which I took from #11162) is a problem because it wrongly suggests multinomial coefficients. The alternative name multicombination has been suggested. Does anyone have a strong preference for either of these names, or another suggestion?

[Kyle Miller]

According to https://mathworld.wolfram.com/Multichoose.html multichoose should be fine for this.

[Kyle Miller]

Another way to justify the name is that where choose is choosing things singly, multichoose is choosing things with multiplicity.

[Kyle Miller]

In the doc string, it'd be good to mention that multichoose is also known as counting multicombinations (and have multicombination in the module doc's tags), if you haven't already.

[Kyle Miller]

May as well put in a hint that this is not the multinomial coefficient, too.

[Kyle Miller]

As a counterpoint, https://www.rdocumentation.org/packages/iterpc/versions/0.4.2/topics/multichoose is the multinomial coefficient, but this library seems to be unique in calling it that. "Multichoose" seems to be this PR's multichoose everywhere else.

[Eric Wieser]

Maybe add a reference to Wolfram for the naming in the docstring, just to be extra safe?

[Violeta Hernández]

Yeah, if the docs make it clear enough that this name is used elsewhere and not the multinomial coefficient, then I completely support it

[Violeta Hernández]

We have docs#cardinal.mk_set_le_aleph_0 and docs#cardinal.lt_aleph_0_iff_set_finite. These are very similar statements but have very different names.

[Violeta Hernández]

The only other related lemma with a similar name to the former is docs#cardinal.mk_subtype_le_aleph_0, while there's a few other lemmas about finite sets with similar names to the latter, such as docs#cardinal.lt_aleph_0_iff_finite and docs#cardinal.lt_aleph_0_of_finite.

[Violeta Hernández]

I would much prefer to be consistent, particularly since we'll be adding a bunch more very similar lemmas now that we have our new docs#countable typeclass. So I might as well put it up to vote.

[Violeta Hernández]

/poll Which scheme should we prefer for these lemmas?

• mk_set_le_aleph_0
• lt_aleph_0_iff_set_finite
• other (suggest)

[Violeta Hernández]

I marginally prefer the lt_aleph_0_iff_set_finite scheme, since it allows us to clearly distinguish between the iff versions and the one sided versions of these lemmas.

[Yury G. Kudryashov]

We have duplicate definitions: docs#equiv.nat_prod_nat_equiv_nat vs docs#nat.mkpair_equiv.

[Yury G. Kudryashov]

/poll Which name should stay in mathlib?
equiv.nat_prod_nat_equiv_nat
nat.mkpair_equiv
I don't care

[Yury G. Kudryashov]

I want to remove one of the names, no matter which one.

[Yury G. Kudryashov]

See #15509 and #15510 for PRs implementing different options.

[Junyan Xu]

There are many possible equivalences between ℕ × ℕ and ℕ, and the name equiv.nat_prod_nat_equiv_nat doesn't specify which one it is. Since the to_fun and inv_fun are already named docs#nat.mkpair and docs#nat.unpair, it's better to include (at least one of) these in the name.

[Yury G. Kudryashov]

It looks like nat.mkpair_equiv wins.

[Jireh Loreaux]

In case anyone didn't see the poll hidden in the other thread and wants to vote (about nondiscrete normed field), please read the summary post immediately prior to the poll: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/hypotheses.20for.20a.20field.20property/near/290408091

[Jireh Loreaux]

I think the naming for continuous_linear_map.lmul and friends is weird. It doesn't match the non-continuous version (which had some recent changes in #15310). Before #15310, continuous_linear_map.lmul was defined in terms of algebra.lmul (and I'm fairly certain that the "l" is for "linear", because the docstring used to call it a bilinear map, even though it was an algebra hom), and I believe this is why it was named as such.

In any case, we used to have algebra.lmul_left and algebra.lmul_right (now named linear_map.mul_left and linear_map.mul_right), but continuous_linear_map.lmul_right does not correspond to linear_map.mul_right and continuous_linear_map.lmul_left doesn't even exist. So, I think the things in the continuous_linear_map namespace should be renamed appropriately. My feeling is:

1. continuous_linear_map.lmul → continuous_linear_map.mul
2. continuous_linear_map.lmul_right → continuous_linear_map.mul_flip (or just delete this if it's not frequently used; it's literally defined as (continuous_linear_map.mul _ _).flip)
3. continuous_linear_map.lmul_left_right → continuous_linear_map.mul_mul

[Jireh Loreaux]

I think maybe people missed this yesterday.

[Jireh Loreaux]

In #16161 I am making equiv_like extend fun_like, and to do so we must rename the current coe_injective' field to something else. Currently in the PR it has been renamed to coe_inv_injective' (the type is ∀ e g : E, coe e = coe g → inv e = inv g → e = g). However, @Anne Baanen mentioned that this seems wrong, but can't think of anything better. Hence poll:

[Jireh Loreaux]

/poll the field equiv_like.coe_injective' should be renamed to:
coe_inv_injective'
ext'
eq_of_coe_eq_of_inv_eq

[Oliver Nash]

I completely agree with Anne's remark here so I don't love coe_inv_injective' but it is definitely the least bad of the various possibilities I can think of.

[Praneeth Kolichala]

Here, I defined polynomial time functions using the native datatype ptree ("plain binary tree"). This is because mathlib's mkpair encoding causes exponential blowup in e.g. the encoding of lists. At some point, I will try porting this to mathlib. In addition, the entire computability library should, I believe, be refactored to use this datatype, because it is the most direct representation of what we actually want to represent -- namely tree structures. I've already discussed this a bit with @Mario Carneiro .

What should this data structure be called:

inductive ptree
| nil
| node (left : ptree) (right : ptree)

[Praneeth Kolichala]

/poll What to call a plain binary tree
ptree
plain_tree
binary_tree

[Yaël Dillies]

I assume this is the same as tree unit?

[Praneeth Kolichala]

Yaël Dillies said:

I assume this is the same as tree unit?

Yes, I think so

[Junyan Xu]

You could also use docs#free_magma unit right?

[Bolton Bailey]

I don't like binary_tree because it implies that tree isn't binary.

[Bolton Bailey]

In fact, it's a bit unfortunate that we have both docs#bin_tree and docs#tree and the difference isn't that one is binary and the other is not the difference is in how leaves are represented. Edit: I guess this is due to the former being in core