Dot notation, capitalization, and naming conventions

Stream: new members

[Eric Rogstad]

Hi All, I've got a question relating to a personal project. Hopefully this is the right place to ask, but please direct me elsewhere if not.

I'm developing a simple game involving Boolean formulas and satisfiability, and I'm trying to use Lean to prove certain properties about the rules of the game. I'd like to follow standard Lean style (using this guide: https://leanprover-community.github.io/contribute/naming.html), but I'm not sure if I'm doing it right.

For a definition like this, is lowerCamelCase correct (applying rules 3 and 4 from the guide)?

/--
Terminal formula: satisfiability is trivially determined.

A formula is terminal when the game ends - either all clauses are satisfied
(empty formula means Affirmative wins) or an empty clause exists (Negative wins).
-/
def Formula.isTerminal {Var : Type} (formula : Formula Var) : Bool :=
  formula.isEmpty || formula.hasEmptyClause

And is UpperCamelCase correct here because it is a Prop (rule 2), or should it be snake_case because it's a "term of type Prop" (applying rule 1)?

/--
Relation defining when one formula has strictly fewer literals than another.

This serves as our termination measure: every valid game operation on a nonterminal
formula produces a formula with a lower literal count, and natural number ordering
is well-founded.
-/
def HasLowerLiteralCount {Var : Type} : Formula Var → Formula Var → Prop :=
  InvImage (· < ·) literalCount

[Aaron Liu]

These two seem correct

[Robin Arnez]

Yeah these are right

[Robin Arnez]

snake_case is if you have an h : p : Prop

[Aaron Liu]

Eric Rogstad said:

And is UpperCamelCase correct here because it is a Prop (rule 2), or should it be snake_case because it's a "term of type Prop" (applying rule 1)?

snake_case applies to "terms of terms of type Prop", so we get FermatLastTheorem : Prop and proof_of_fermat_last_theorem : FermatLastTheorem.

[Eric Rogstad]

Hmm, so my HasLowerLiteralCount is actually a function that produces a prop though, right?

[Eric Rogstad]

But then does that actually mean that Rule 3 applies:

Functions are named the same way as their return values (e.g. a function of type A → B → C is named as though it is a term of type C).

... and then since the return type is Prop, then I'd go to Rule 2:

Props and Types (or Sort) (inductive types, structures, classes) are in UpperCamelCase. There are some rare exceptions: some fields of structures are currently wrongly lower-cased (see the example for the class LT below).

... which would tell me to use UpperCamelCase?

[Eric Rogstad]

Thanks! Btw, meta question, which perhaps you've implicitly answered, but is this the right place to ask these kinds of newbie questions?

[Eric Rogstad]

Oh, another object level question — if Formula.isTerminal had returned a Prop rather than a Bool, would that mean it should be Formula.IsTerminal instead? And if so, is it weird to mix dot notation with UpperCamelCase, or is that normal?

[Aaron Liu]

Dot notation with upper camel case is normal, for example in mathlib we have docs#Nat.Prime, docs#Function.LeftInverse, docs#Set.Subsingleton