Zulip Chat Archive
Stream: general
Topic: naming contest
Anne Baanen (Oct 16 2020 at 15:11):
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 (Oct 16 2020 at 15:24):
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 (Oct 16 2020 at 15:26):
Ah good point, I was thinking about how to describe "basis change" in Lean.
Anne Baanen (Oct 16 2020 at 15:26):
But we can do it one side at a time.
Anne Baanen (Oct 16 2020 at 15:27):
Still quite a long name :/
Gabriel Ebner (Oct 16 2020 at 16:09):
You could turn one of the underscores into a dot and put it in the is_basis
namespace.
Gabriel Ebner (Oct 16 2020 at 16:10):
Eric's version also looks like a good simp lemma.
Yury G. Kudryashov (Nov 07 2021 at 18:54):
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 tonull_measurable_set
;  the type tag for "
α
withmeasurable_set
=null_measurable_set
".
For the first two,null_measurable_set
andnull_measurable
look like obvious choices. What about the other two?
Sebastien Gouezel (Nov 07 2021 at 19:15):
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 Cauchylike integral formulas, so we need integrals there  and such spaces of operators are never secondcountable.
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 secondcountable 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 usecase 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 secondcountable).
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 (Nov 07 2021 at 19:19):
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 sigmaalgebra, 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 (Nov 07 2021 at 19:51):
In what generality null_measurable = ae_measurable
?
Yury G. Kudryashov (Nov 07 2021 at 19:53):
In any case, I think that we should have better API for null_measurable_set
s.
Sebastien Gouezel (Nov 07 2021 at 21:16):
Yury G. Kudryashov said:
In what generality
null_measurable = ae_measurable
?
I guess when the target space is secondcountable.
Sebastien Gouezel (Nov 07 2021 at 21:16):
Yury G. Kudryashov said:
In any case, I think that we should have better API for
null_measurable_set
s.
Yes, definitely!
Andrew Yang (Dec 02 2021 at 02:45):
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 (Dec 03 2021 at 11:01):
I'm going to add Prop
versions of docs#fintype and docs#encodable. How should I call them?
Johan Commelin (Dec 03 2021 at 11:17):
_root_.finite
and _root_.countable
?
Mario Carneiro (Dec 03 2021 at 11:23):
doesn't docs#countable already exist? guess not
Kevin Buzzard (Dec 03 2021 at 22:49):
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 (Dec 03 2021 at 23:36):
I already have _root_.countable
with some instances. I'll add glue code and PR it over weekend.
Yury G. Kudryashov (Feb 20 2022 at 04:06):
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 (Feb 20 2022 at 04:06):
(and now I see that I forgot to polish _root_.countable
)
Sebastien Gouezel (Feb 20 2022 at 09:32):
Looks good to me.
Eric Wieser (Mar 06 2022 at 16:47):
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 (Mar 06 2022 at 16:49):
/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 (Mar 06 2022 at 16:49):
cc @Anne Baanen, since I think you added this originally
Junyan Xu (Mar 18 2022 at 08:19):
/poll What should $V^G$ be called for a Grepresentation V? (Context)
 fixed_space
 invariants
Junyan Xu (Mar 18 2022 at 08:33):
Kevin Buzzard (Mar 18 2022 at 08:35):
cohomology.H 0 G V
;) (this is not a correct answer  there should probably just be an isomorphism...)
Reid Barton (Mar 18 2022 at 10:19):
invariants seems good also because the dual guy is called the coinvariants (what else?)
Yury G. Kudryashov (Apr 21 2022 at 22:39):
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 (Apr 21 2022 at 23:34):
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 (Apr 22 2022 at 05:58):
set.finite_of_prod_iff
, using the rule "of
refers to the type of arguments"?
Yaël Dillies (Apr 22 2022 at 07:31):
I would name the third one set.prod_finite_iff
.
Floris van Doorn (Apr 22 2022 at 11:15):
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 (Apr 22 2022 at 11:37):
Well, when we usually use of
for proofs, it also refers to the type
Eric Wieser (Apr 22 2022 at 11:37):
I think we also sometimes use docs#of_fintype in names, which is referring to a nonProp
type
Yury G. Kudryashov (Apr 23 2022 at 00:39):
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 (May 16 2022 at 15:58):
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 (May 16 2022 at 15:59):
This already exists
Yury G. Kudryashov (May 16 2022 at 15:59):
How is it called?
Yaël Dillies (May 16 2022 at 16:02):
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 (May 16 2022 at 16:02):
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 (May 16 2022 at 16:03):
What does docs#with_top.has_add do?
Kyle Miller (May 16 2022 at 16:03):
This is what applicative functors let you do in a generalized way for any number of arguments (keep adding <*>
).
Yaël Dillies (May 16 2022 at 16:03):
Yeah that's what it does.
Eric Wieser (May 16 2022 at 16:04):
Note the f <$> x <*> y
version only works when α β γ
are in the same universe
Yaël Dillies (May 16 2022 at 16:04):
A good name would be option.map\2
but indeed you can just write it out monadically.
Yury G. Kudryashov (May 16 2022 at 16:05):
Yes, I wanted to prove some lemmas about this combinator, then use it for (+)
and (*)
on with_top
.
Yaël Dillies (May 16 2022 at 16:05):
Yeah... but if we perform the functor refactor we talked about, that wouldn't be a problem anymore.
Eric Wieser (May 16 2022 at 16:05):
it was never clear to me whether that refactor would actually work
Kyle Miller (May 16 2022 at 16:06):
monadically
(n.b. this uses the weaker notion of an applicative functor, no need for monads)
Yaël Dillies (May 16 2022 at 16:06):
What are you fearing? I thought about it and couldn't see anything wrong.
Eric Wieser (May 16 2022 at 16:06):
Typeclass search not handling out_param
s well enough
Yaël Dillies (May 16 2022 at 16:06):
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 (May 16 2022 at 16:07):
Let me dig out the PR...
Yury G. Kudryashov (May 16 2022 at 16:07):
We already have docs#with_top.has_add and docs#with_top.mul_zero_class
Yaël Dillies (May 16 2022 at 16:09):
Ah right, it was subtraction. #8889
Mauricio Collares (May 16 2022 at 16:10):
I'd expect something close to Haskell's naming (liftA\2
)
Anne Baanen (May 16 2022 at 16:10):
For the name, I would follow Haskell and use some variant of lift2
Yaël Dillies (May 16 2022 at 16:11):
Yeah so 0 * top = 0
, not 0 * top = top
.
Yury G. Kudryashov (May 16 2022 at 16:12):
Yes, lift₂
will be used for the else
branch.
Violeta Hernández (Jun 22 2022 at 04:41):
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 (Jun 22 2022 at 04:42):
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 (Jun 22 2022 at 04:43):
/poll What name should we use?
 insert_nonempty
 nonempty_insert
Kyle Miller (Jun 22 2022 at 04:47):
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 (Jun 22 2022 at 04:50):
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 (Jun 22 2022 at 04:53):
I also think this decision should be made on a perpredicate 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 (Jun 22 2022 at 11:58):
Just to relink the old thread on this type of naming issue: https://leanprover.zulipchat.com/#narrow/stream/113488general/topic/.23naming.20and.20dot.20notation/near/246520191
Eric Wieser (Jun 22 2022 at 11:59):
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 (Jun 22 2022 at 12:39):
Unfortunate but understandable
Stuart Presnell (Jul 02 2022 at 09:01):
#15061 adds two recursion principles for P : ℕ → ℕ → Sort*
for which I'm looking for naming suggestions:

strong_sub_recursion
: if for alla b : ℕ
we can extendP
from the rectangle strictly below(a,b)
toP a b
, then we haveP n m
for alln m : ℕ
.
This was originally proved and named by @Chris Birkbeck in #14828 (which is now closed) 
pincer_recursion
: if we haveP i 0
andP 0 i
for alli : ℕ
, and for anyx y : ℕ
we can extendP
from(x,y+1)
and(x+1,y)
to(x+1,y+1)
, then we haveP n m
for alln 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 (Jul 03 2022 at 18:19):
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 (Jul 03 2022 at 18:25):
According to https://mathworld.wolfram.com/Multichoose.html multichoose should be fine for this.
Kyle Miller (Jul 03 2022 at 18:27):
Another way to justify the name is that where choose
is choosing things singly, multichoose
is choosing things with multiplicity.
Kyle Miller (Jul 03 2022 at 18:27):
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 (Jul 03 2022 at 18:29):
May as well put in a hint that this is not the multinomial coefficient, too.
Kyle Miller (Jul 03 2022 at 18:34):
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 (Jul 03 2022 at 18:47):
Maybe add a reference to Wolfram for the naming in the docstring, just to be extra safe?
Violeta Hernández (Jul 04 2022 at 00:13):
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 (Jul 17 2022 at 23:12):
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 (Jul 17 2022 at 23:14):
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 (Jul 17 2022 at 23:16):
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 (Jul 17 2022 at 23:17):
/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 (Jul 17 2022 at 23:18):
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 (Jul 19 2022 at 02:26):
We have duplicate definitions: docs#equiv.nat_prod_nat_equiv_nat vs docs#nat.mkpair_equiv.
Yury G. Kudryashov (Jul 19 2022 at 02:26):
/poll Which name should stay in mathlib
?
equiv.nat_prod_nat_equiv_nat
nat.mkpair_equiv
I don't care
Yury G. Kudryashov (Jul 19 2022 at 02:27):
I want to remove one of the names, no matter which one.
Yury G. Kudryashov (Jul 19 2022 at 02:34):
See #15509 and #15510 for PRs implementing different options.
Junyan Xu (Jul 19 2022 at 02:39):
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 (Jul 19 2022 at 12:16):
It looks like nat.mkpair_equiv
wins.
Jireh Loreaux (Jul 22 2022 at 14:47):
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/116395maths/topic/hypotheses.20for.20a.20field.20property/near/290408091
Jireh Loreaux (Aug 04 2022 at 20:10):
I think the naming for continuous_linear_map.lmul
and friends is weird. It doesn't match the noncontinuous 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:
continuous_linear_map.lmul
→continuous_linear_map.mul
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
)continuous_linear_map.lmul_left_right
→continuous_linear_map.mul_mul
Jireh Loreaux (Aug 05 2022 at 16:58):
I think maybe people missed this yesterday.
Jireh Loreaux (Aug 22 2022 at 16:12):
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 (Aug 22 2022 at 16:13):
/poll the field equiv_like.coe_injective'
should be renamed to:
coe_inv_injective'
ext'
eq_of_coe_eq_of_inv_eq
Oliver Nash (Aug 22 2022 at 19:27):
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 (Sep 01 2022 at 18:41):
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 (Sep 01 2022 at 18:43):
/poll What to call a plain binary tree
ptree
plain_tree
binary_tree
Yaël Dillies (Sep 01 2022 at 20:51):
I assume this is the same as tree unit
?
Praneeth Kolichala (Sep 01 2022 at 20:57):
Yaël Dillies said:
I assume this is the same as
tree unit
?
Yes, I think so
Junyan Xu (Sep 01 2022 at 22:01):
You could also use docs#free_magma unit
right?
Bolton Bailey (Sep 02 2022 at 02:26):
I don't like binary_tree
because it implies that tree
isn't binary.
Bolton Bailey (Sep 02 2022 at 02:28):
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
Last updated: Aug 03 2023 at 10:10 UTC