rfc: theorem names

Stream: lean4

[Daniel Selsam]

There is a proposal for theorem names at https://github.com/leanprover/lean4/issues/402 The proposal is snake case but with camelCase for the components:

• nat_add_zero
• axiom_of_choice
• eq_punit
• runCatch_pure
• seqLeft_eq_bind

Note that types (e.g. Nat, Eq) become lowercase. The known downside is that it cannot distinguish between e.g. Or and or, but this may acceptable in light of how bad the alternatives seem. If anybody sees any critical problems with this proposal, please share them in the GitHub issue.

[Mario Carneiro]

Why nat_add_zero instead of Nat.add_zero?

[Mario Carneiro]

specifically, why is it no longer in the Nat namespace?

[Mario Carneiro]

When you say "types became lowercase", do you mean Nat becomes nat like in lean 3? Or is this only for theorem names, not the actual type names?

[Daniel Selsam]

Mario Carneiro said:

Why nat_add_zero instead of Nat.add_zero?

I just translated what happened to be in Init to the proposed style. Nat.add_zero is consistent with the proposal.

[Daniel Selsam]

Whatever comes between the _ would be camelCase.

[Mario Carneiro]

So types, modules, and namespaces are all PascalCase?

[Daniel Selsam]

Yes, and file names.

[Mario Carneiro]

There will be a number of specific naming conflicts to resolve, no matter what the convention is. I guess the RFC isn't the appropriate place for this, although it might influence the choice

[Mario Carneiro]

I'm broadly supportive of the plan though

[Daniel Selsam]

It would be helpful to find other examples of the Or_True/or_true clash, besides just Prop/Bool.

[Mario Carneiro]

Are we using Title_Snake_Case anywhere?

[Daniel Selsam]

i.e. names that appear both uppercase as types and lowercase as values/functions

[Daniel Selsam]

No, we are not using Title_Snake_Case anywhere. That is option (2) in the GitHub issue. It has very little support AFAICT, in part because of the issue I mentioned: connectives (and, or) and verbs (eq) are awkward capitalized.

[Mario Carneiro]

when you say Or_True then are you referring to the theorem p \/ True = True?

[Daniel Selsam]

Yes, and or_true is p || true = true.

[Mario Carneiro]

That looks like Bool.or_true

[Mario Carneiro]

and I think something similar to this can avoid most of the name clashes about Prop/Bool

[Mario Carneiro]

we could also go back to tt/ff

[Daniel Selsam]

I agree that Bool.or_true is a fine solution for that particular clash.

[Mario Carneiro]

The fact that true is blue and True isn't seems like it implicitly prefers true, which probably isn't the right default for mathematics

[Mario Carneiro]

Well, maybe we can get by if we just use ⊤ and ⊥ for true and false, although those symbols are currently in use for lattices

[Daniel Selsam]

Daniel Selsam said:

i.e. names that appear both uppercase as types and lowercase as values/functions

Here is one possible clash:

inductive EvalsTo (p : Program) (v : Value) : Prop
def evalsTo (p : Program) (n : Nat) : Option Value

theorem evalsTo_of_evalsTo

[Mario Carneiro]

I would just use EvalsTo in the theorem name if there is a name clash like that

[Mario Carneiro]

I think it's fine to just use that as a backup plan

[Mario Carneiro]

there are quite a few backup plans in the mathlib naming convention

[Mario Carneiro]

What about lowercasing Prop-valued types?

[Daniel Selsam]

Mario Carneiro said:

The fact that true is blue and True isn't seems like it implicitly prefers true, which probably isn't the right default for mathematics

Neither are blue for me. Is that a VSCode thing? What does blue mean?

[Mario Carneiro]

keyword I guess

[Mario Carneiro]

even though it's not a keyword

[Daniel Selsam]

Could be easy to just make True and true blue then

[Mario Carneiro]

true is apparently in the constant.language.lean4 textmate scope

[Mario Carneiro]

which is blue in my theme

[Daniel Selsam]

Mario Carneiro said:

What about lowercasing Prop-valued types?

You mean Prop-valued inductive types?

[Mario Carneiro]

defs too, although I guess most of them are inductive

[Mario Carneiro]

someone pointed out earlier that propositions often feel more like functions than types

[Mario Carneiro]

Would it be alright to take a poll? I think this is the sort of thing that deserves a decent size poll

[Daniel Selsam]

Poll how?

[Mario Carneiro]

zulip has a poll system

[Mario Carneiro]

it might not get enough people though

[Scott Morrison]

(there may be more lurkers on this stream than you realise :-)

[Mac]

Here is a copy of my comment on the issue:

I personally prefer option 2, but option 3 is fine as well. However, since the major problem with 2 is ugly verbs, I would suggest mixing 2 and 3. That is, I would preserve the original casing for nouns and use lower camelCase for verbs (i.e. Foo_and_Bar_iff_Rig instead of foo_and_bar_iff_rig and PUnit.eq_PUnit instead of PUnit.eq_punit). I would then have the namespace a given theorem is in dictate the meaning of verbs. That is, Bool.or_true means Bool or and root Foo_and_Bar_iff_Rig means Prop And and Iff.

I agree with @Mario Carneiro that namespace can help resolve some of the clashes. I, however, would also like to see casing preserved at least for nouns.

[Andrew Kent]

FWIW, I am biased towards more predictable and case preserving of names/types/etc, so I guess (2)?. (3) is not bad though and perhaps with namespaces adding additional clarity at times it would be quite nice.

W.r.t. not liking (2), I don't think I fully understand the objections. So far I've seen

• it is not aesthetically pleasing (I guess it just doesn't bother me in what I've seen so far :shrug: ), and
• "Option 2 ... does not abide by the rule that only values in Sort should be capitalized" mentioned by @Sebastian Ullrich in the GH issue -- do these structures/classes in Prop also count as not abiding by this rule:

structure Iff (a b : Prop) : Prop where
  intro :: (mp : a → b) (mpr : b → a)

class inductive Nonempty (α : Sort u) : Prop where
  | intro (val : α) : Nonempty α

class Subsingleton (α : Sort u) : Prop where
  intro :: allEq : (a b : α) → a = b

structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
  refl  : ∀ x, r x x
  symm  : ∀ {x y}, r x y → r y x
  trans : ∀ {x y z}, r x y → r y z → r x z

Or am I misunderstanding the naming rule w.r.t. values in Sort and Prop?

[Sebastian Ullrich]

What part do you mean, the class/structure names?

[Sebastian Ullrich]

Recall that Prop == Sort 0 :)

[Andrew Kent]

Yes, the structure/class names was what I was referring to. I suppose I don't have an intuition clicking in my head yet for when the aforementioned rule that (2) violates applies in practice as I'm skimming Lean files and how option 2 relates.

[Sebastian Ullrich]

Said otherwise, the rule is that declarations that are types (not just Types but also Props) should be capitalized. Ne_Eq is not a type.

[Andrew Kent]

I guess my vote is for (3) then :+1:

[Daniel Selsam]

There seems to be consensus for (3). Anyone have any lingering concerns/suggestions before we merge?

[Mario Carneiro]

I've mentioned this in private messages (and briefly above), but just to put it out there more formally and gauge interest: I'd like to propose a variant of (3) in which types that are propositions (i.e. of type Prop or ... -> Prop, but not necessarily types defeq to that like Set A) are lowercase camel-cased, including in particular eq, or, and, true, false.

• We can tell at a glance whether a type is a type or a prop, which is important information due to the effects of proof irrelevance. Currently mathlib indicates this inconsistently using the is_ prefix.
• It avoids the issue with eq in theorems being capitalized differently than the type Eq.
• It doesn't differ significantly from the current Haskell-ish convention for programming uses, where all the data types are actual types and so get the uppercase camel case style. In particular Nat, Int and such are still capitalized.
• This does lead to a clash with Bool.true. Personally I'd be fine with returning to Bool.tt but I don't think this is a particularly important issue and would hate for the whole naming convention to get blocked for a reason like this.

We can use this post as a :+1: :-1: mini-poll, where :-1: means option (3) as originally written.

[Daniel Selsam]

Based on other off-channel discussions, I think tt/ff is widely considered unacceptable for programming and a non-starter. At some point, you proposed weird names for Prop true/false and always using notation for them.

[Daniel Selsam]

FWIW I don't think your first two points are that strong, since (a) you still don't know at a glance due to defeq, and (b) we will still have e.g. Nat referred to as nat in proof names. Also, this proposal would break the namespace/filename symmetry, since presumably filenames will still be capitalized but here there would be lowercase namespaces, e.g. prime.

[Mario Carneiro]

If Bool.tt isn't acceptable, using True for the prop is close enough for me. We might be able to use top and bot symbols but I expect that these will be overloaded for lattices, so for core lean just True and False for the props should do.

(a) you still don't know at a glance due to defeq

I still don't really follow this point. Just because two types are defeq doesn't mean they act the same; in lean 3 it makes quite a difference and there are many redefinitions of quot.mk for particular quotient types specifically so that they have a different syntactic type. The only thing that matters is the syntactic type, and for the edge cases we can leave it as a judgment call beyond the broad strokes of the naming convention.

[Floris van Doorn]

@Mario Carneiro: When using option (3) it doesn't matter that much whether Eq is capitalized or not, right? We don't write Eq, since we use the infix notation =. And in all theorem names ..._eq... will not be capitalized.
So the main differences I see will be namespace Eq vs namespace eq and if we have to refer to a full name for some reason (Eq.refl vs eq.refl).
If those are the main changes, I don't really care that much about this distinction. Maybe some full names are more common (Or.elim?) though.

[Mario Carneiro]

(b) we will still have e.g. Nat referred to as nat in proof names.

It's pretty rare for Nat to show up in the name of a theorem; it usually appears in the namespace of the theorem when the theorem is about a definition in the Nat namespace. I consider the exceptions rare enough to be acceptable.

@Floris van Doorn Yes, the main place this shows up is in things like Or.inl and Eq.symm, although I think it will become more common as we start to get deeper into mathlib and encounter predicates and relations and prop-classes that have no notation

[Daniel Selsam]

Here is another argument in favor of @Mario Carneiro's proposal: many functions returning Prop are decidable and used in programming in lieu of Bools. Currently we have an exception in the naming conventions for these, e.g. isValidChar.

[Daniel Selsam]

FWIW I don't think eq.refl vs Eq.refl matters much though, and would probably rather Eq.refl for uniformity (e.g. making all namespaces and filenames PascalCase)

[Mario Carneiro]

If the type is called eq I think we should make the theorems eq.refl as well, because otherwise we will end up with inconsistency when using dot notation (unless the mechanism for dot notation is changed so that it doesn't depend on naming in this way). Note that it is already not the case that all namespaces are uppercase - internal definitions will use the name of the main definition with an additional name segment like Namespace.mainDef.internalDef

[Mario Carneiro]

Regarding file names, I don't think we need to change anything - file/module names have never been related in any direct way to type names

[Daniel Selsam]

To clarify: I didn't mean eq together with Eq.refl, they should definitely agree.

[Mario Carneiro]

I'm not really sure whether project names (e.g. in the repo name and/or the name = ... in the toml) need to be capitalized though. Personally I would like these to be lowercase and unrelated to lean module names, but I'm not sure if leanpkg wants some agreement here

[Mario Carneiro]

Note that it is already not the case that all namespaces are uppercase - internal definitions will use the name of the main definition with an additional name segment like Namespace.mainDef.internalDef

While these are namespaces in the technical sense, I think we should distinguish between these uses of namespaces for grouping vs namespaces for indicating that one definition/theorem is about the one with the parent name. The former kind of namespace is somewhat rare in mathlib but there are some like category_theory and these should be pascal case, and the latter kind of namespace should just follow the casing of the parent definition

[Floris van Doorn]

Daniel Selsam said:

Here is another argument in favor of Mario Carneiro's proposal: many functions returning Prop are decidable and used in programming in lieu of Bools. Currently we have an exception in the naming conventions for these, e.g. isValidChar.

I think that is a pretty strong argument in favor of Mario's proposal. And this exception could be drawn much further (True is definitely decidable, and And preserves decidability). In that case it seems simplest to make all propositions camelCase.

[Mario Carneiro]

Another solution to True/true that just occurred to me: we can have a notation true with a type-dependent elaborator that elaborates to True when the target type is Prop and Bool.true or its coercion otherwise. Lean 3 already makes it fairly transparent to use true for tt or vice versa, but the coercion that sneaks in bothers me and so I try to always use the right one. A type dependent elaborator would let me use true always with a good conscience

[Daniel Selsam]

Floris van Doorn said:

Daniel Selsam said:

Here is another argument in favor of Mario Carneiro's proposal: many functions returning Prop are decidable and used in programming in lieu of Bools. Currently we have an exception in the naming conventions for these, e.g. isValidChar.

I think that is a pretty strong argument in favor of Mario's proposal. And this exception could be drawn much further (True is definitely decidable, and And preserves decidability). In that case it seems simplest to make all propositions camelCase.

Do you also agree with Mario's proposal that this should only extend to identifiers that syntactically return Prop and not to ones that return e.g. Sets? So it would be "bad style" to declare isValidChar : Set Nat and then use it as a boolean?

[Mario Carneiro]

It's already bad style in mathlib to write isValidChar x if isValidChar : Set Nat. You would instead have validChars : Set Nat and x \in validChars to express that. (EDIT: validChars should be lowercase because it's not a type)

[Mario Carneiro]

I don't know if we have a linter for that but we should

[Daniel Selsam]

Huh? I thought you were specifically proposing ValidChars : Set Nat, i.e. you only camelCase things that syntactically return Prop.

[Mario Carneiro]

:thinking: That last example has me wondering whether we need another exception to the rule to capitalize things of type Set A since they are "like" types even though they aren't, technically.

[Mario Carneiro]

@Daniel Selsam The rule is to capitalize things of type Sort u or Type u but not Prop or OtherType. Absent another exception that means that sets should be lowercase

[Daniel Selsam]

Wasn't that exception in your proposal?

I'd like to propose a variant of (3) in which types that are propositions (i.e. of type Prop or ... -> Prop, but not necessarily types defeq to that like Set A) are lowercase camel-cased

[Mario Carneiro]

I think using Set A in that example was not a good choice, because if we "see though" the abbreviation then it has type A -> Prop so it should be lowercase, and if we don't then it has type Set A which is not a universe so it should also be lowercase

[Mario Carneiro]

what I meant to say by that example is that the naming convention does not "see through" abbreviations

[Daniel Selsam]

Ah, thanks for clarifying. I understand now.

[Scott Morrison]

Slippery slope: if we were to capitalize things of type Set A since they are like types, wouldn't we also want to capitalize things of type Submodule R M, etc, since they are just as much like types?

[Daniel Selsam]

What about capitalizing things that syntactically return something capitalized besides Prop?

[Mario Carneiro]

that would include Nat.add

[Mario Carneiro]

Re: slippery slope, we could extend the rule (whatever it is) to things with a coe to sort

[Daniel Selsam]

Mario Carneiro said:

Daniel Selsam The rule is to capitalize things of type Sort u or Type u but not Prop or OtherType. Absent another exception that means that sets should be lowercase

I don't yet see a major problem with this. We can simplify the wording as only capitalize things that syntactically return Sort u or Type u.

[Mario Carneiro]

I don't have a well formed opinion on sets, submodules etc. Maybe lowercase is fine

[Daniel Selsam]

I think it would be a priori reasonable to use decidable Sets in programming, i.e. n \in validChars.

[Mario Carneiro]

I don't think that resolves the question though. Both capital and lowercase seem reasonable in that position

[Daniel Selsam]

It would be behaving like a datastructure though (which would normally be camelCase), similar to how isValidChar would be behaving like a Bool-valued function.

[Mario Carneiro]

One argument for the slippery slope version: if there is a coe to sort, then you can write n: validChars and with the lowercasing rule for props this makes n look like a proof of a proposition

[Mario Carneiro]

So to more formally state the slippery slope version: Only capitalize things that either syntactically return Sort u or Type u, or types that coerce to Sort u or Type u.

[Mac]

Mario Carneiro said:

Another solution to True/true that just occurred to me: we can have a notation true with a type-dependent elaborator that elaborates to True when the target type is Prop and Bool.true or its coercion otherwise. Lean 3 already makes it fairly transparent to use true for tt or vice versa, but the coercion that sneaks in bothers me and so I try to always use the right one. A type dependent elaborator would let me use true always with a good conscience

What is wrong with following?

universe u
class True (A : Type u) := true : A
class False (A : Type u) := false : A

export True (true)
export False (false)

instance : True Bool := ⟨Bool.true⟩
instance : False Bool := ⟨Bool.false⟩

instance : True Prop := ⟨Prop.true⟩
instance : False Prop := ⟨Prop.false⟩

(I am not sure whether Prop's should be a default instance, but the idea in general seems sound).

[Mario Carneiro]

The issue is that we want the result to be syntactically either True or Bool.true depending on the context. Since there are coercions in both directions you can still use either one in the wrong context and get something equivalent to the right result, but it is syntactically incorrect (if you use true : Prop you get true = true and if you use True : Bool you get decide True)

[Mac]

How does that relate to my class example?

[Mario Carneiro]

With an instance you would end up with the wrong answer in both cases, namely @True.true Prop instTrueProp and @True.true Bool instTrueBool instead of True and Bool.true respectively

[Mac]

Is that a problem?

[Mac]

They can be proved equivalent, right?

[Mac]

ex. example : true = Prop.true := rfl or example : true = Bool.true := rfl

[Mac]

Furthemore, this seems to fit with the way Lean generally handles shared syntax (ex. the type classes for Add, Mul, etc.)

[Mario Carneiro]

Yes, it causes problems for simp, rw and other tactics that look at the syntax of a term in order to decide what to do

[Mario Carneiro]

I don't think the way to solve the issue of two ways to write true is to make four ways to write true

[Mac]

Why isn't that also a sticking point for the math operators (and natural literals) then?

[Mac]

Sure you could make "true"/"false" custom syntax and do type-dependent elaboration as you said. But as Lean doesn't do that other syntax, but instead use type classes, it seems reasonable to use type classes here.

[Mario Carneiro]

This is getting off topic for this thread

[Mac]

Mario Carneiro said:

I don't think the way to solve the issue of two ways to write true is to make four ways to write true

No, now there is really one way -- everything would just use the true from the type class. Just like everything uses the hAdd from HAdd when doing addition.

[Mac]

However, I am not denying there may be issues with that, it just seems reasonable to remain consistent with how this kind of polymorphism is done elsewhere.

[Mario Carneiro]

Any solution to this issue will be in mathlib anyway, lean core doesn't have to care

[Mario Carneiro]

lean can just define True and Bool.true

[Mario Carneiro]

true isn't notation (in lean core) so it doesn't make sense to have a notation typeclass for it (in lean core)

[Mac]

isn't the theorem names rfc about Lean core, though? so this will effect core.

[Mario Carneiro]

This is not an rfc about typeclass true

[Mac]

I am simply suggesting that this would be one way to resolve the true/True and false/False problem that came up as a sticking point for option (3). This would unify them into a single true/false thus removing the clash.

[Mario Carneiro]

your proposal is a lot more than a name change though, it needs separate discussion and this isn't the place for it

[Mac]

k, if you say so

[Mario Carneiro]

regardless of the existence of alternate typeclasses, you would still need a name for Prop.true and Bool.true. We don't use Prop as a namespace elsewhere

[Mario Carneiro]

current frontrunner seems to be True and Bool.true

[Mac]

Personally, I do think that using Prop as a namespace would be a good idea and help mitigate a lot of these naming clashes.

[Mac]

As theorems that clash between Bool and Prop could go into their separate namespaces.

[Mac]

Mario Carneiro said:

current frontrunner seems to be True and Bool.true

Well, yeah, because that is currently how it is set up and thus it is easiest to keep it that way.

[Mario Carneiro]

Note that true and Bool.true aren't an option not because they clash directly, but because they clash when Bool.true is exported. That's why we're considering separate names like true/tt or True/true. Prop.true/Bool.true would similarly cause clashing exported names

[Mac]

I concur largely with what you said earlier, I think that since Prop "types" follow proof irrelevance it makes sense for them to be lower camelCase like objects instead of upper camelCase like types (and this is already some followed with things like isValidChar).

[Mac]

Mario Carneiro said:

Note that true and Bool.true aren't an option not because they clash directly, but because they clash when Bool.true is exported. That's why we're considering separate names like true/tt or True/true. Prop.true/Bool.true would similarly cause clashing exported names

Yes but if you had something like a type class to unify them you wouldn't need to export them.

[Mac]

Just like you don't need to export Nat.add or Int.add because Add unifies them.

[Mac]

In fact, if they used namespace, you could potentially solve the syntactic problem by having true : A and false : A be elaborated to A.true/ A.false (ex. Prop.true/Bool.true).

[Sebastian Ullrich]

I have to say I like the current naming convention with capitalizing propositions for teaching. Using the same naming convention really drives home the whole "propositions are just types", which, yes, students are quick to forget about again even if it's the very first and central thing you tell them. I'd like to hear whether @Jakob von Raumer and @Marc Huisinga agree.

[Sebastian Ullrich]

I agree that using IsValidChar in a conditional would probably look weird. On the other hand,

structure Char where
  val   : UInt32
  valid : val.isValidChar

also looks quite weird to me, with a camelcase ident right of :! I haven't really made up my mind about this yet.

[Gabriel Ebner]

Sebastian Ullrich said:

also looks quite weird to me, with a camelcase ident right of :!

It's also going to be lowercase if Char.isValidChar : Char → Bool is a Boolean. This is only consistent.

[Marc Huisinga]

Sebastian Ullrich said:

Using the same naming convention really drives home the whole "propositions are just types", which, yes, students are quick to forget about again even if it's the very first and central thing you tell them. I'd like to hear whether Jakob von Raumer and Marc Huisinga agree.

I'm not sure if students will really remember this any better if the naming convention mirrors it :sweat_smile:
One thing I've also noticed during the lab is that students sometimes confuse False with false and True with true. Not necessarily because they missunderstand the difference between Bool and Prop, but because they forget the exact name and write down the first thing that comes to their mind.

[Sebastian Ullrich]

Almost makes you wonder if we do need both true and True to begin with. We could have

def true.intro : true := rfl
def false.elim : false → α := fun h => nomatch h

and together with pretty-printing away = true usage would basically stay the same. For efficiency and indexing reasons we might want to instead use

inductive Bool.asProp : Bool → Prop where
  | true : asProp true

but that would really be an implementation detail.

[Kevin Buzzard]

Sebastian Ullrich said:

Almost makes you wonder if we do need both true and True to begin with.

Yeah I'd be behind that proposal. My students never use Bool, we could just scrap it completely.

[François G. Dorais]

@Sebastian Ullrich Or perhaps Bool.AsProp...

[Gabriel Ebner]

Sebastian Ullrich said:

Almost makes you wonder if we do need both [false and False] to begin with.

For False, it is convenient to have dot-notation, i.e. (not_lt_of_le h1 h2).elim which wouldn't work out-of-the-box with a coercion from Bool. But maybe there's a way to make dot-notation see through Bool.asProp.

[Daniel Fabian]

@Gabriel Ebner wouldn't (not_lt_of_le h1 h2).asProp.elim work?

[Gabriel Ebner]

No? With the proposal, not_lt_of_le h1 h2 would have the type Bool.asProp false (pretty-printed as false). Dot-notation would then look for a declaration called Bool.asProp.elim.

[Daniel Fabian]

ah, gotcha

[Daniel Fabian]

elim could potentially be a type class, but I guess that's completely besides the point.

[François G. Dorais]

Why would it look for Bool.elim? This currently works:

inductive Bool.asProp : Bool → Prop where
| true : asProp true

theorem T : 0 = 1 → Bool.asProp false := λ h => Nat.noConfusion h

#reduce (h : 0 = 1) → (T h).recOn (motive:=λ _ _ => _) Empty
-- 0 = 1 → Bool.asProp.rec Empty (_ : Nat.noConfusionType (Bool.asProp false) 0 1)

[Gabriel Ebner]

Ah sorry, it would look for Bool.asProp.elim of course. But that's still not helpful for false.elim (even if you manage to reuse the recursor) , since you need to provide lots of extra arguments to the recursor.

[François G. Dorais]

This works:

inductive Bool.asProp : Bool → Prop where
| true : asProp true

theorem T : 0 = 1 → Bool.asProp false := λ h => Nat.noConfusion h

def Bool.asProp.elim {C : Sort _} : false.asProp → C := λ h => nomatch h

example (h : 0 = 1) : true = false := (T h).elim

[Sebastian Ullrich]

Calling it elim is a bit weird when it's not applicable to all asProps. How about exfalso? Doesn't that make the proof script even more readable than before?

[Sebastian Ullrich]

Or elimFalse or...

[Gabriel Ebner]

exfalso's actually a good name. Although I'd still prefer dot-notation to see through the asProp.

[Sebastian Ullrich]

There was some discussion about a [parent] attribute that could be applied to structure fields for this, but it would need to be even more general in this case...

[François G. Dorais]

Speaking of names: the constructor Bool.asProp.true should be protected or perhaps renamed Bool.asProp.trivial.

[Patrick Massot]

Sebastian Ullrich said:

I have to say I like the current naming convention with capitalizing propositions for teaching. Using the same naming convention really drives home the whole "propositions are just types", which, yes, students are quick to forget about again even if it's the very first and central thing you tell them.

For me this is a really strong argument against this naming convention. I try very hard to completely hide the whole "propositions are just types" crazyness to my students.

[Marc Huisinga]

Patrick Massot said:

Sebastian Ullrich said:

I have to say I like the current naming convention with capitalizing propositions for teaching. Using the same naming convention really drives home the whole "propositions are just types", which, yes, students are quick to forget about again even if it's the very first and central thing you tell them.

For me this is a really strong argument against this naming convention. I try very hard to completely hide the whole "propositions are just types" crazyness to my students.

One example that came up in the course was that students proved properties about the natural numbers and then had to define monoids and instantiate Nat as a monoid.
We explained that propositions are types (in the sense that we can use the same language to work with them) and showed examples of propositions and regular structures which only contain data.
Given that information, we expected them to figure out that you can declare the monoid rules as fields of the structure as part of the exercise.
Is that crazy, or would you instead not mention "propositions as types" at all and always introduce all Lean features separately, once for propositions and once for types, even if they are used in very similar ways?
EDIT: I realize this is a bit off-topic :sweat_smile:

[Jeremy Avigad]

I'd like to cast a vote in favor of (at least trying out) the current proposal to reserve upper case for datatypes (and types like Set that are thought of as mathematical data). Teaching and constructive ideology aside, propositions aren't datatypes. Conflating them is confusing, and in practice it is often useful to be able to distinguish them easily.

As Patrick's remark indicates, mathematicians feel strongly about this. But it is also useful for computer scientists to distinguish between programming and verification, and to be able to tell at a glance whether they are dealing with a piece of code or a specification.

I don't know the best way to mediate between Prop and Bool. Sometimes x < y is a branching condition and sometimes it is used as a specification. But whatever we do to finesse that, I think it is helpful to be mindful of the distinction.

[Jeremy Avigad]

P.S. I have no problem with propositions as types -- it is useful as an analogy, and explaining commonalities in Lean syntax when writing code and proving theorems. All I am saying is that it is often helpful to distinguish them as well.

[Kevin Buzzard]

Am I right in thinking that propositions _aren't_ types in Isabelle/HOL?

"define monoids" would be something that people in my course would find easy, because I define lots of structures very early on -- mathematics is full of structures. My students have probably never seen the inductive keyword though.

[Mario Carneiro]

Am I right in thinking that propositions _aren't_ types in Isabelle/HOL?

That's correct. In ZFC or HOL based systems (Isabelle/HOL, HOL Light, Mizar, Metamath) propositions are in a separate class from data / objects in the domain of discourse and you can't conflate them. Only DTT based systems (Coq, Agda, Lean) have propositions as types.

[Mario Carneiro]

Marc Huisinga said:

One thing I've also noticed during the lab is that students sometimes confuse False with false and True with true. Not necessarily because they missunderstand the difference between Bool and Prop, but because they forget the exact name and write down the first thing that comes to their mind.

This is the audience I'm trying to address with the proposal for a type dependent elaborator for the notation true. It doesn't come with an unexpander so it will still be printed as True (maybe this is debatable), but it's easier to do the right thing when you can just always write true and lean just inserts the right one.

[Gabriel Ebner]

Mario Carneiro said:

In ZFC or HOL based systems (Isabelle/HOL, HOL Light, Mizar, Metamath) propositions are in a separate class from data / objects in the domain of discourse and you can't conflate them.

Which is not entirely true. In the HOL systems, there is only a distinction between terms and types. The Booleans are a type, and e.g. true has the type Boolean. Just like the natural numbers are a type, and 0 has the type natural number. And propositions are just terms of type Boolean. (In metamath these are indeed different categories though.)

[Gabriel Ebner]

Another category is proofs: these are completely separate in all non-DTT systems that I know of.

[Mario Carneiro]

ah, you are right. In HOL propositions are objects in the domain of discourse, but proofs are not

[Mario Carneiro]

Actually maybe I should say that propositions are like data but they have a different type (namely Boolean in HOL and wff in metamath). This is more surprising in metamath since there are only a handful of types, but it's approximately the same distinction

[Patrick Massot]

In my teaching using Lean students don't define define anything. They don't even state lemmas. It's all about proofs (what else?).

[Marc Huisinga]

Patrick Massot said:

In my teaching using Lean students don't define define anything. They don't even state lemmas. It's all about proofs (what else?).

But that's only half the fun! :grinning_face_with_smiling_eyes:

[Patrick Massot]

My course is really using Lean as a tool towards learning how to write correct proofs on paper.

[Sebastian Ullrich]

Jeremy Avigad said:

But it is also useful for computer scientists to distinguish between programming and verification, and to be able to tell at a glance whether they are dealing with a piece of code or a specification.

This is in fact nicely demonstrated at Char, where one really wants the information that the second field is erased and thus the entire structure is unboxed. So I suppose I just have to get used to it.

[Daniel Selsam]

Summary so far:

• Their seems to be consensus for the original (3), which is independent of the capitalization scheme for types/props.
• There seems to be consensus to (a) capitalize definitions that syntactically return Sort u or Type u and (b) not to capitalize definitions that syntactically return Prop. One of the main benefits of the latter is that we are already lower-casing many of these anyway as special-cases, since decidable Props are frequently used like Bools.
• There does not seem to be consensus yet whether to capitalize definitions that return other types, which includes both defs that are def-eq to something returning Prop (e.g. def mySet : Set Nat) and ones that are not (e.g. def MapToType α := α → Type; def foo : MapToType Nat). Mario proposed the "slippery slope" addendum: also capitalize defs that return types that coerce to Sort u or Type u. Another obvious candidate is the "semantic" approach of removing the "syntactic" qualifier from the original proposal. Note that these two proposal have the opposite behavior on the two examples above.
• There are a few ways to deal with true, the simplest being to just capitalize the Prop versions. I think other variants could probably be considered separately from this issue.

[Daniel Selsam]

Downside to slippery slope proposal: the presence of a coercion isn't as binary/definitive as either the syntactic or semantic checks. Somebody could add a CoeSort in some other file much later, or as a local instance, etc.

[Mario Carneiro]

Somebody could add a CoeSort in some other file much later, or as a local instance, etc.

I don't think these are very important considerations. The vast majority of the time whether something has a coe to sort or not is relatively integral to the type's expression and use. If CoeSort is added in a file much later, that's bad style, unless for whatever reason it is very difficult to set up the coercion in which case the whole file should be written with that in mind. If it's a local instance, then it doesn't count.

[Mario Carneiro]

Since we're talking about a naming convention here it's okay to have a solution for 90% of cases and leave the rest as judgment calls

[Daniel Selsam]

I agree this is unlikely to be an issue. I think I would still rather foo : MapToType Nat to be Foo though. How about slippery-slope + semantic, since they seem to be compatible. The rule would be caps if it semantically returns Sort u or Type u, or if it coe-to-sorts to something that does.

[Mario Carneiro]

The main issues I see with the semantic approach:

• Definitions can be arbitrarily stacked, so it can be unobvious and sometimes even surprising to discover that something, ultimately, boils down to a function to Type/Prop. This is well known as the "apply bug" in lean 3, where the apply tactic uses the number of pi types in the fully unfolded type of the applied lemma even though most of them are hidden to the user (and in some cases even explicitly marked as opaque using @[irreducible]). The purpose of definitions is to encapsulate complexity and we shouldn't be peeking behind the curtain.
• Besides this, it can actually just be difficult to determine "at a glance" whether a type is such a definition, which means that people will be tempted to use a lower cost approximation to the naming convention, leading to inconsistency.
• For abbreviations, there is a stronger argument for unfolding since the user is explicitly indicating that it should be unfolded. However that's a directive to lean, not to readers, and I would still be inclined to default to not unfolding in this case with exceptions added on a case-by-case basis.

[Daniel Selsam]

Mario Carneiro said:

• Definitions can be arbitrarily stacked, so it can be unobvious and sometimes even surprising to discover that something, ultimately, boils down to a function to Type/Prop.

Can you please clarify why this wouldn't be compositional? Why couldn't you just look at the capitalization of the syntactic return type?

def Foo0 (α : Type) : Type 4 := α → Type 3
def Foo1 : Foo0 Nat := fun _ => Type 2
def Foo2 : Foo1 0   := Type 1
def Foo3 : Foo2     := Type

[Mario Carneiro]

Foo2 is capitalized the same as Nat but def foo3 : Nat and def Foo3 : Foo2 have different capitalization

[Mario Carneiro]

To determine how Foo3 needs to be capitalized you have to look at the definition (value) of Foo2 and unfold everything there (your example is just Type 1 so no additional unfolding is necessary)

[Mario Carneiro]

A bad case would be something like this:

def Foo0 (α : Type) : Type 1 := α → Type
def Foo1 : Type 1 := Foo0 Nat
def Foo2 : Type 2 := Foo1 -> Foo1
def Bar : Foo2 := id

to determine that Bar should be capitalized you need to look at the definition of Foo0, Foo1 and Foo2, and none of the capitalization there helps

[Daniel Selsam]

Whoops, I confused myself. Thanks for clarifying. In that case I agree with the syntax + slippery-slope proposal. I will summarize it on the GitHub issue.

[Mac]

Question: If we are proposing to capitalize any identifier that is syntactically in Sort u or Type u, wouldn't it make sense for auto bound implicit arguments to auto bind single upper case letters as Sort u/Type u rather than single lower case letters (as having a lower case identifier syntactically in Sort u/Type u violates this style guide)?

[Sebastian Ullrich]

This RFC is about naming declarations. I haven't seen any proposals for changing our parameter naming scheme, which is to always use lowercase names, mostly Greek ones for type parameters.

[Sebastien Gouezel]

It's not exactly what we do in mathlib, where our style guide contains: "α, β, γ, ... for generic types. Types with a mathematical content are expressed with the usual mathematical notation, often with an upper case letter (G for a group, R for a ring, K or 𝕜 for a field, E for a vector space, ...)".

But it's arguably a mathlib thing, so none of the concern of core.

[Mac]

It just seems a little odd to me to auto bind lower case ASCII letters as Type u/Sort u when every other instance of (syntactic) Type u/Sort u is going to be upper case (or a greek letter / unicode identifier).

[Mac]

It feels inconsistent and symmetry breaking.

[Gabriel Ebner]

Sebastien Gouezel said:

But it's arguably a mathlib thing, so none of the concern of core.

It is, insofar as isValidAutoBoundImplicitName cannot be overriden and rejects K as a valid name.

[Mario Carneiro]

Mac said:

It just seems a little odd to me to auto bind lower case ASCII letters as Type u/Sort u when every other instance of (syntactic) Type u/Sort u is going to be upper case (or a greek letter / unicode identifier).

FWIW Haskell / ML also have this split: Type parameters are lowercase letters but types and type constructors are uppercase camel-case, as in Seq a or 'a Seq.t

[Mac]

Mario Carneiro said:

FWIW Haskell / ML also have this split: Type parameters are lowercase letters but types and type constructors are uppercase camel-case, as in Seq a or 'a Seq.t

Yes, but, in Haskell, there is a split between the type and term namespaces. Type and term variables cannot clash or overshadow one another, making such usage more natural. As a result, one can (and many times does) have type specifications like k :: k (ala k : k in Lean), which is not possible in a dependently typed language like Lean.

[Mac]

In fact, Haskell makes heavy use of this split in its DataKinds extension, where every term constructor Foo (in the term namespace) gets an automatically promoted type constructor also named Foo (in the type namespace).

[François G. Dorais]

Sebastian Ullrich said:

For efficiency and indexing reasons we might want to instead use

inductive Bool.asProp : Bool → Prop where
  | true : asProp true

but that would really be an implementation detail.

Is there a reason why it is not currently implemented this way? My impression is that this coercion would be easier to use than = true, in general.

[Mario Carneiro]

We have a lot of tools for dealing with equality, and this inductive type is the same as what you would get by inlining the definition of Eq true as an inductive type, so I'm not sure there is much to be gained except maybe some visual brevity (which we can also address by using unexpanders)

[Mario Carneiro]

in particular, the main ways to interact with this would be to prove it when it's true via ⟨⟩ and eliminate it when it's false via nomatch h and that would work with either representation (and Eq also has another compact spelling for the first case, rfl)